Coq 定理证明：peano 算术中的简单分数律

Question

我正在学习 coq，并试图证明 peano 算术中的等式。

我陷入了一个简单的分数定律。

我们从小学就知道 (n + m) / 2 = n / 2 + m / 2。 在 peano 算术中，这仅在 n 和 m 为偶数时才成立（因为除法会产生正确的结果）。

Compute (3 / 2) + (5 / 2). (*3*)
Compute (3 + 5) / 2. (*4*)

所以我们定义：

Theorem fraction_addition: forall n m: nat , 
    even n -> even m ->  Nat.div2 n + Nat.div2 m = Nat.div2 (n + m).

据我了解，这是一个正确且可证明的定理。 我尝试了一个归纳证明，例如

intros n m en em.
induction n.
- reflexivity.
- ???

这让我陷入了这样的境地

en = even (S n) 和IHn : even n -> Nat.div2 n + Nat.div2 m = Nat.div2 (n + m)，所以我找不到应用归纳假设的方法。

经过对标准库和文档的长期研究，我没有找到答案。

Answer 1

在这种情况下，你需要加强你的归纳假设。 一种方法是证明这样的归纳原理：

From Coq Require Import Arith Even.
Lemma nat_ind2 (P : nat -> Prop) :
  P 0 ->
  P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
now intros P0 P1 IH n; enough (H : P n /\ P (S n)); [|induction n]; intuition.
Qed.

nat_ind2可以这样使用：

Theorem fraction_addition n m :
  even n -> even m ->
  Nat.div2 n + Nat.div2 m = Nat.div2 (n + m).
Proof.
  induction n using nat_ind2.
  (* here goes the rest of the proof *)
Qed.

Answer 2

如果你可以使用标准库，你也可以不用归纳证明你的定理。

如果您在假设中使用Even m（表示exists n, m = 2*m），那么您可以使用标准库中的引理进行简单的代数重写。

Require Import PeanoNat.
Import Nat.

Goal forall n m, Even n -> Even m -> n / 2 + m / 2 = (n+m)/2.
  inversion 1; inversion 1.
  subst.
  rewrite <- mul_add_distr_l.
  rewrite ?(mul_comm 2).
  rewrite ?div_mul; auto.
Qed.

问号只是表示“尽可能多地（零次或多次）重写”。

inversion 1 对目标中的第一个归纳假设进行反演，在这种情况下首先是 Even n，然后是 Even m。它在上下文中为我们提供了n = 2 * x 和m = 2 * x0，然后我们将其替换。

还要注意even_spec: forall n : nat, even n = true <-> Even n，所以如果您愿意，可以使用even，只需先用even_spec 重写...