我想在 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 不再支持它。
最佳答案
你可以写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
关于coq - 如何在 Coq 中编写中间证明语句 - 类似于在 Isar 中如何有 `have Statement using Lemma1, Lemma2 by auto` 但在 Coq 中?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/70324745/