The Coq mailing list

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

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