The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Li-Yang Tan 
<lytan AT artsci.wustl.edu>:

Hello,

> Hello,
>
> I have a simple question regarding the intro(s) tactic.  Suppose I am
> trying to prove the following implication,
>
> P : Prop
> Q : Prop
> ----------------------------------
> (P /\ (Q /\ R)) -> ((P /\ Q) /\ R)
>
> I can pull to antecedent of the implication into my list of
> hypotheses/assumptions by doing "intros [H1 [H2 H3]]".  This is very
> nice, since it saves me from having to do: "intro; elim H; intros; elim
> H0; intros."  I believe there is a similar trick for disjunctions, so if
> the antecedent of my implication is say (P /\ (Q \/ R)), I can simply do
> "intros [H1 [H2 | H3]]."
>
> I am curious as to whether there is something similar if the antecedent
> has a list of nested existential quantifiers.
>
> For example, consider the following:
>
> Theorem Fermat :
>     (exists x, exists y, exists z, exists n,
>        (n > 2) /\ (x^n + y^n  = z^n)) -> False.
>
> Is there any way I can introduce x, y, z, and n into my assumptions
> *without* having to do the following?
>
> intro.
> elim H; intros.
> elim H0; intros.
> elim H1; intros.
> elim H2; intros.


Hi,

 You can do the following :

 intros (x,(y,(z,(n,(H,e))))).

1 subgoal

  x : Z
  y : Z
  z : Z
  n : Z
  H : n > 2
  e : x ^ n + y ^ n = z ^ n
  ============================
   False

  The rest of the proof is left as an exercise.

Best regards,


Pierre

> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.