如何在 Coq 中编写中间证明语句 - 类似于 Isar 中的“使用 Lemma1、Lemma2 by auto 有语句”，但在 Coq 中？

Question

我想在 Coq 证明脚本中编写中间引理，例如，在 SCRIPTProof. SCRIPT Qed.本身中 - 类似于在 Isar 中的做法。在 Coq 中如何做到这一点？例如：

have Lemma using Lemma1, Lemma2 by auto.

我知道这个exact陈述，想知道是否就是这样……但我也想得到这个陈述的证据，就像在伊萨尔我们有have by auto或using Proof. LEMMA_PROOF Qed.

为了使其具体化，我试图做这些非常简单的证明：

Module small_example.

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

  Theorem plus_n_Sm :
    forall n m : nat,
      S (n + m) = n + (S m).
  Proof.
    intros n m.
    induction n as [| n' IH].
    - simpl. reflexivity.
    - 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 -> add_easy_induct_1. reflexivity.
    - simpl. rewrite -> IH. simpl. rewrite <- plus_n_Sm. reflexivity.
  Qed.

End small_example

但我不知道如何实现，而且效果也不是很好。

---

shows我也对Coq感兴趣，例如

shows T using lemmas by hammer.

---

当前的答案很好地表明了 Coq 中存在 have 和 by 语句。然而，关键缺少的是 1）shows 语句和 2）using 语句。我希望看到与 Coq 证明中类似的构造——尤其是与 Shows 和 Have 一起使用的 using 构造。

---

伊莎贝尔似乎擅长的是在给出证明和一系列假设的情况下宣布陈述为真。例如，名称为：L，使用 metis 的 l1。会创建引理 L 作为一个新事实，给它命名 name 但使用策略 metis 证明它，但关键取决于事实 l1 作为该陈述成功所给出的东西。所以我希望能够声明事物并通过 Coq 中的策略/ATP 检查。

---

有关的：

• 我知道 Czar ( https://coq.discourse.group/t/what-is-the-difference- Between-ssreflect-and-czar/824 )，但 Coq afaik 不再支持它。

Answer 1

您可以在证明过程中编写assert <lem>证明中间结果的方法。<lem>其他变体是assert <lem> by <tactic>立即证明<lem>使用<tactic>，或assert (<lemname> : <lem>)为引理命名。例子：

Theorem add_comm :
  forall n m : nat,
    n + m = m + n.
Proof.
  intros.
  induction n as [| n' IH].
  - simpl.
    assert (add_easy_induct_1 : forall n, n + 0 = n) by (induction n; auto).
    rewrite -> add_easy_induct_1. reflexivity.
  - simpl.
    assert (plus_n_Sm : forall n m, S (n + m) = n + S m) by (induction n; auto).
    rewrite -> IH. simpl. rewrite <- plus_n_Sm. reflexivity.
Qed.

文档assert： https: //coq.inria.fr/distrib/current/refman/proof-engine/tropics.html#coq :tacn.assert

Answer 2

您可以使用Coq 策略语言have:中的构造ssreflect，具有与您想要的几乎相同的语义，再加上一些与如何立即使用此引理（例如，用于重写）相关的附加功能，而不是给出一个姓名。

具体代码示例请参见/sf/answers/4999976761/