为什么在基本情况被证明之后，Coq删除/清除我的证明中的断言引理？ [英] Why does Coq remove/clear my asserted lemmas in my proof after the base case is proved?

问题描述

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

  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'. 

推荐答案

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

这篇关于为什么在基本情况被证明之后，Coq删除/清除我的证明中的断言引理？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！