The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

I do not think this answers the question, because it gives you a goal
with an existential variable instead of a goal in existential form.

In the script below this hidden because the goal is trivial and solved
by reflexivity. Or do you know a way to go back from an existential
variable to an existential goal ?

Benjamin


Le 31 janv. 07 à 11:33, Pierre Casteran a écrit :

> Hi,
>
> Another way is using existential variables:
>
>
> Goal exists x:nat, exists y : nat, y*y = x.
> eapply ex_intro.
> exists 3.
> simpl.
> reflexivity.
> Qed.
>
> Pierre
>
>
>
>
>
>
>
> Benjamin Werner wrote:
>
> > Hi,
> >
> > It seems the simplest is to first prove the ad-hoc
> > lemma :
> >
> >
> > Lemma ex_perm : forall A B : Type, forall P : A -> B -> Prop,
> > (exists x:A, exists y:B, P x y) ->
> >   (exists y:B, exists x : A, P x y).
> > Proof.
> > intros A B P [x [y p]]; exists y; exists x; trivial.
> > Qed.
> >
> > (* test on a stupid example *)
> >
> > Goal exists x:nat, exists y : nat, x=y.
> > apply ex_perm; exists 3.
> >
> >
> > I hope it works also when the right-hand part is less
> > simple.
> >
> > Cheers,
> >
> >
> > Benjamin
> >
> >
> >
> > Le 31 janv. 07 à 10:39, Keiko Nakata a écrit :
> >
> > > Hello,
> > >
> > > How can I instantiate an inner existential?
> > >
> > > Suppose P and Q are of Prop and I have a subgoal :
> > >
> > > exists i : Z, (P /\ (exists j : Z, Q))
> > >
> > > I know that j does not depend on i and want to instantiate j first
> > > with, say an integer 3, so as to make the subgoal look simpler.
> > >
> > > It would be nicer if I can also instantiate j first with an object
> > > which depends on i (e.g., i+3).
> > >
> > > With best regards,
> > > Keiko
> > >
> > >
> > >
> > > --------------------------------------------------------
> > > 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
> >
> >
> > --------------------------------------------------------
> > 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
>
>
> --------------------------------------------------------
> 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