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.