Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Error w_Unify.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Error w_Unify.


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page