The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  May I suggest "intro H; induction H as (x,(y,Hy))" as an extra
alternative (or even its contraction "induction 1 as (x,(y,Hy))"
... but the meaning of "1" is a bit esoteric here).

------------------------------------
Parameter P P' Q : nat* nat -> Prop.

Goal (exists c1, (exists c2,  P (c1, c2) /\ Q (c1, c2))) ->
       (exists c3, (exists c4,  P' (c3, c4) /\ Q (c3, c4))).
Proof.
induction 1 as (x,(y,Hy)).
exists x; exists y.
...
------------------------------------

  Hugo

Pierre Courtieu:
> Pierre Casteran:
> > 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'hypothM-hse 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...).