为什么在证明基本情况后，Coq 会删除/清除我的证明中断言的引理？

Question

我想在证明的顶部断言一些引理，并将它们重新用于每个未来的目标。我做到了：

  Theorem add_comm_eauto_using:
    forall n m: nat,
      n + m = m + n.
    Proof.
      intros. induction n.
      assert (H: forall n, n + 0 = n) by eauto using n_plus_zero_eq_n.
      assert (H': forall n m, S (n + m) = n + S m) by eauto using Sn_plus_m_eq_n_plus_Sm.
      - eauto with *.

但在我证明了基本情况之后，假设就从当地环境中消失了！

为什么会发生这种情况以及如何阻止 coq 删除我的本地引理并将它们永远保留在这个证明中的本地上下文中？最好在证明中。身体 Qed。 身体。

---

脚本：

  Theorem n_plus_zero_eq_n:
  forall n:nat,
    n + 0 = n.
  Proof.
    intros.
    induction n as [| n' IH].
    - simpl. reflexivity.
    - simpl. rewrite -> IH. reflexivity.
  Qed.

  Theorem Sn_plus_m_eq_n_plus_Sm:
  forall n m : nat,
    S (n + m) = n + (S m).
  Proof.
    intros n m.
    induction n as [| n' IH].
    - auto.
    - simpl. rewrite <- IH. reflexivity.  
  Qed.

  Theorem add_comm :
  forall n m : nat,
    n + m = m + n.
  Proof.
    intros.
    induction n as [| n' IH].
    - simpl. rewrite -> n_plus_zero_eq_n. reflexivity.
    - simpl. rewrite -> IH. rewrite -> Sn_plus_m_eq_n_plus_Sm. reflexivity. 
  Qed.

  (* auto using proof *)
  Theorem add_comm_eauto_using_auto_with_start:
  forall n m: nat,
    n + m = m + n.
  Proof.
    intros. induction n.
    Print Hint.
      - auto with *.
      - auto with *. 
    Qed.

  Theorem add_comm_eauto_using:
    forall n m: nat,
      n + m = m + n.
    Proof.
      intros. induction n.
      assert (H: forall n, n + 0 = n) by eauto using n_plus_zero_eq_n.
      assert (H': forall n m, S (n + m) = n + S m) by eauto using Sn_plus_m_eq_n_plus_Sm.
      - eauto with *.
      - eauto using IHn, H, H'. 

Answer 1

您在作为基本情况的证明部分中定义引理；因此，当此步骤完成时，它们将被丢弃。如果将它们放在归纳n之前，则在两种情况下都可以访问它们。