The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hi Daniel,

It is also a good opportunity to interpret this as a concrete
application of Curry-Howard.  Making the induction over a quantified
formula is more than a trick, it is directly related to the kind of
(higher-order primitive) recursion used in the definition of sum -- a
pedantic way of presenting tail-recursion.

Conversely, you can make a very short "tail-recursive proof" of sum_S
as follows:

Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).                  
Proof.
fix 2 (* better practice: use "refine", but I'm lazy *).
  intros a [| b']; simpl.
    reflexivity.
    rewrite <- (sum_S (S a) b'). reflexivity.
Qed.

Cheers,
JF

On Mon, Dec 13, 2010 at 02:01:08AM +0100, Daniel de Rauglaudre wrote:
> 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/
> 
> 

-- 
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458