1

我正在学习 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)，所以我找不到应用归纳假设的方法。

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

4

2 回答 2

3

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

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.
于 2019-11-30T21:18:26.460 回答
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对目标中的第一个归纳假设进行反演，在本例中为 firstEven n然后Even m. 它给了我们n = 2 * x和m = 2 * x0在上下文中，然后我们替换它。

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

于 2019-12-01T11:21:43.407 回答