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.

问号就是"rewrite as many (zero or more) times as possible".

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重写...

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

Coq theorem proving: Simple fraction law in peano arithmetic

theorem-proving

coq

peano-numbers