[SOLVED] Coq theorem proving: Simple fraction law in peano arithmetic

Coq theorem proving: Simple fraction law in peano arithmetic

I am learning coq and am trying to prove equalities in peano arithmetic.

I got stuck on a simple fraction law.

We know that (n + m) / 2 = n / 2 + m / 2 from primary school. In peano arithmetic this does only hold if n and m are even (because then division produces correct results).

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

So we define:

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

From my understanding this is a correct and provable theorem. I tried an inductive proof, e.g.

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

Which gets me into the situation that

en = even (S n) and IHn : even n -> Nat.div2 n + Nat.div2 m = Nat.div2 (n + m), so i don't find a way to apply the induction hypothesis.

After long research of the standard library and documentation, i don't find an answer.

Solution

You need to strengthen your induction hypothesis in cases like this. One way of doing this is by proving an induction principle like this one:

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 can be used as follows:

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.