为什么在证明基本情况后，Coq remove/clear 我在证明中断言的引理？

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 删除我的本地引理并将它们永远保留在该证明的本地上下文中？最好在 Proof. body 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

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

为什么在证明基本情况后，Coq remove/clear 我在证明中断言的引理？

Why does Coq remove/clear my asserted lemmas in my proof after the base case is proved?

coq

coq-tactic