The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

Hi Daniel,

You could actually prove directly that your sum function is always
equal to 'plus' on natural numbers. From this, you'll have no problem
proving your lemma.

Require Import Arith_base.

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

Lemma sum_plus : forall b a : nat, sum a b = a + b.
Proof.
induction b.

(* Base case *)
auto.

(* Induction step *)
intro a.
simpl.
rewrite (IHb (S a)).
rewrite plus_Snm_nSm; reflexivity.
Qed.

I'm not that well versed in Coq to discuss a minimum condition for the
proof you wanted to do, but it seems to me that a stronger induction
hypothesis might be required, and you can obtain it as above.

Best regards,
Petar

On 12 December 2010 18:17, Daniel de Rauglaudre
<daniel.de_rauglaudre AT inria.fr>
 wrote:
> 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/
>