The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

You can also use the same syntax as for conjunctions and disjunctions:

intros [x [y [z [n [A B]]]]].

-Andrew


On Sun, 13 Nov 2005, Pierre Casteran wrote:

> 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.
> --------------------------------------------------------
> 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
>