coq - 如何在 Coq 中编写中间证明语句 - 类似于在 Isar 中如何有 `have Statement using Lemma1, Lemma2 by auto` 但在 Coq 中？

Question

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

have Lemma using Lemma1, Lemma2 by auto.

我知道 exact 语句，想知道是否就是这样......但我也想像在 Isar 中一样获得该语句的证明，我们有 have by auto 或 使用证明。 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

但我不确定它是如何工作的，而且效果不是很好。

---

我也对 Coq 中的 shows 感兴趣，例如

shows T using lemmas by hammer.

---

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

---

Isabelle 似乎擅长的是在给定证明和一系列假设的情况下宣布陈述为真。因此，例如有名称: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/tactics.html#coq:tacn.assert