Skip to Content.
Sympa Menu

coq-club - Re: guarded fixpoints

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: guarded fixpoints


chronological Thread 
  • From: Pascal Brisset <pascal.brisset AT cnet.francetelecom.fr>
  • To: Frederic Blanqui <Frederic.Blanqui AT lri.fr>
  • Cc: Dimitri Hendriks <Dimitri.Hendriks AT phil.uu.nl>, coq-club AT pauillac.inria.fr
  • Subject: Re: guarded fixpoints
  • Date: Fri, 19 Nov 1999 18:04:37 +0100 (MET)

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 -






Archive powered by MhonArc 2.6.16.

Top of Page