The Coq mailing list

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

Hi everybody,

I am a beginner in Coq and I am blocked in that proof:

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

  Lemma sum_zero : forall a : nat, sum 0 a = a.

This 'sum' could be a definition of the 'plus' on natural numbers.
It seems to be true but I have no idea how to complete my proof.
I managed this:

  intro a; elim a; [ simpl; reflexivity | clear a; intros n H ].

I could add 'simpl', but I see no way to continue.

Perhaps recursion on 'a' is not the solution, but I don't see other
ways.

Well, actually, I am not sure I can proof it 'by hand' without using
other definitions of addition and subtraction, this may be the problem.
I would like to know what is *minimum* to complete such a proof.

Any hints?

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