The Coq mailing list

[Pascal Brisset <pascal.brisset AT cnet.francetelecom.fr>]

Frederic Blanqui writes:
 > Lemma good_term_ind
 >      : (P:(term->Prop))
 >         (P (fun (nil term)))
 >         ->((t:term; l:(list term))(P (fun l))->(P (fun (cons t l))))
 >         ->(t:term)(P t).

Here is a stronger elimination:

| Lemma better_term_ind
|      : (P:(term->Prop))
|         (P (fun (nil term)))
|         ->((t:term; l:(list term))(P t)->(P (fun l))->(P (fun (cons t l))))
|         ->(t:term)(P t).
|   Intros P P0 rec. Fix 1. Destruct t; Clear t. Induction l; Clear l.
|     Assumption.
|     Intros t l H. Apply rec.
|       Apply better_term_ind; Auto.
|       Assumption.
| Qed.

I believe you would need that in order to prove, for example:

| Fixpoint ident [t:term] : term := let (l) = t in (fun (map ident l)).
| Lemma Ident : (t:term) (ident t)=t.

and like you, I would like to have it generated automatically.

- Pascal Brisset 
<pascal.brisset AT cnet.francetelecom.fr>
 +33296051928 -
- France Telecom CNET DTL/MSV | 2 av Pierre Marzin | F-22307 Lannion -