coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 -
- guarded fixpoints, Dimitri Hendriks
- Re: guarded fixpoints, Christine Paulin
- Re: guarded fixpoints,
Frederic Blanqui
- Re: guarded fixpoints, Pascal Brisset
Archive powered by MhonArc 2.6.16.