Coq：帮助形式化一个非正式的证明

Question

Theorem ev_ev__ev_full : forall n m,
  even (n+m) <-> (even n <-> even m).
Proof.
  intros n m. split.
  - intros H. split.
    + intros H1. apply (ev_ev__ev n m H H1).
    + intros H1. rewrite plus_comm in H. apply (ev_ev__ev m n H H1).
  - intros H.

输出：

  n, m : nat
  H : even n <-> even m
  ============================
  even (n + m)

现在n可以是偶数也可以不是偶数。

如果n是偶数，m也是偶数。那么由ev_sum定理(n+m)也是偶数。
如果 n 不是偶数，它的形式是 (n' + 1)，其中 n' 是偶数。 m 也不是偶数，并且具有 (m' + 1) 的形式，其中 m' 是偶数。所以他们的总和等于：

n + m = n' + 1 + m' + 1 => n + m = (n' + m') + 2.

偶数 ((n' + m') + 2)。在 apply ev_SS 之后我们得到偶数 (n' + m')。由于我们知道 n' 是偶数且 m' 是偶数，我们 apply ev_sum。这证明了定理。

如何在 coq 中编写这个非正式证明？

Answer 1

从这些引理开始：

Theorem even_S (n : nat) : (~even n <-> even (S n)) /\ (even n <-> ~even (S n)). Admitted.
Theorem contra {A B : Prop} (prf : A -> B) : ~B -> ~A. Admitted.

even_S 是通过归纳法证明的，我认为这是定理的例子之一，使结论比您预期的更强大可以更容易地证明（删除 /\ 的任一侧使剩下的一方困难）。 contra 是一个 tauto 逻辑。

知道 even_S，even n 的可判定性直接从对 n 的归纳得出。

Theorem even_dec (n : nat) : {even n} + {~even n}. Admitted.

这是一个决策程序：even_dec n 告诉您 n 是否是 even，取决于它 returns 是左选项还是右选项。 { _ } + { _ } 是 sumbool 的表示法。它基本上就像一个 bool（它在 Set 中，因此可以在计算相关的上下文中被破坏）除了它还见证了两个给定的 Prop 之一，具体取决于替代方案。在你的证明中，第一步是分支属性:

    destruct (even_dec n) as [prf_n | prf_n].

如果even n，证明是微不足道的。

    + admit.

否则，反向蕴涵的逆反告诉我们~even m。我们还可以消除 nots:

    + pose proof (contra (proj2 H) prf_n) as prf_m.
      apply even_S in prf_n.
      apply even_S in prf_m.

证明的其余部分（断言 n = S n'、m = S m'、even n'、even m' 因此 even (n + m)）紧随其后的是一些工作（与inversion).

      admit.

（我自己填写了 admit 并且这条路径确实成功地导致了证明，但只是泄露所有答案并不好玩 :)。 )

Coq：帮助形式化一个非正式的证明

Coq: help to formalize an informal proof

coq

logical-foundations