The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

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