The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

On Sun, Dec 12, 2010 at 07:18:09PM +0100, Martijn Vermaat wrote:

> I think the most obvious way is by first proving the following fact:
>   Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).

Yeah! It works!

I have my proof without "+", auto, nor importing modules.
I learned many things. Thanks a lot!

  Fixpoint sum (a b : nat) : nat :=
    match b with
    | 0 => a
    | S b1 => sum (S a) b1
    end.

  Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).
  Proof.
    intros a b; generalize a; generalize b; clear; induction b.
    reflexivity.
    intro a; simpl; rewrite <- (IHb (S a)); simpl; reflexivity.
  Qed.

  Lemma sum_zero : forall a : nat, sum 0 a = a.
  Proof.
    induction a.
    reflexivity.
    assert (H : (sum 0 (S a) = S (sum 0 a))) by apply sum_S.
    rewrite H; f_equal; assumption.
  Qed.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/