2

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

have Lemma using Lemma1, Lemma2 by auto.

我知道该exact声明并想知道是否是这样...但是我也希望像在 Isar 中一样拥有该声明的证据，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

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

有关的：

4

2 回答 2

6

您可以在证明中间写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

于 2021-12-12T16:55:42.023 回答
6

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

于 2021-12-12T18:30:09.597 回答