coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
- To: Pierre Casteran <casteran AT labri.fr>
- Cc: Aurore Collomb <aurorecollomb AT chez.com>, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Error w_Unify.
- Date: Tue, 13 Jan 2004 12:24:13 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Mon, 12 Jan 2004 17:16:09 +0100
Pierre Casteran
<casteran AT labri.fr>
wrote:
> Parameter P P' Q : nat* nat -> Prop.
>
>
> Axiom R : forall a b, P (a, b) -> P' (a, b).
>
> Goal (exists c1, (exists c2, P (c1, c2) /\ Q (c1, c2))) ->
> (exists c3, (exists c4, P' (c3, c4) /\ Q (c3, c4))).
> Proof.
> intro H; case H; intros x Hx.
> case Hx; intros y Hy.
> exists x; exists y.
> generalize R; intuition.
> Qed
Bien que les tactiques fabriquant des noms d'hypothèse soient honnis de
certain (à juste titre), je signale que
decompose [ex] H.
fait la mm chose que
case H; intros x Hx. case Hx; intros y Hy.
(sauf que y s'appelle x0, Hx s'appelle H0 et Hy s'appelle H2 allez savoir
pourquoi...).
Pierre
- [Coq-Club] Error w_Unify., Aurore Collomb
- Re: [Coq-Club] Error w_Unify., Benjamin Werner
- Re: [Coq-Club] Error w_Unify.,
Pierre Casteran
- Re: [Coq-Club] Error w_Unify., Pierre Courtieu
- Re: [Coq-Club] Error w_Unify., Hugo Herbelin
- Re: [Coq-Club] Error w_Unify.,
Carlos.SIMPSON
- Re: [Coq-Club] Error w_Unify., Pierre Courtieu
- Re: [Coq-Club] Error w_Unify., Benjamin Gregoire
- Re: [Coq-Club] Error w_Unify., Pierre Courtieu
Archive powered by MhonArc 2.6.16.