0 
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 中编写这个非正式的证明？

4

1 回答 1

2

从这些引理开始：

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，取决于它返回左选项还是右选项。{ _ } + { _ }是 的符号sumbool。它基本上就像 a bool（它在Set其中，因此可以在计算相关的上下文中被破坏），除了它还见证了两个给定Prop的 s 之一，具体取决于替代方案。在您的证明中，第一步是在此属性上进行分支：

    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.

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

于 2020-07-28T23:27:59.420 回答