The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Guillaume and Justus,

Thank you all for your help.

Justus, swapping the variables under the existential quantifier did the trick.

Best,
Lucian

On Tue, Dec 4, 2012 at 5:40 PM, Justus Matthiesen <justus.matthiesen AT cl.cam.ac.uk> wrote:

> A stripped down example of what I am trying to prove is :
>
> c1 : C
> b1 : B
> ----------------------------------
> exists (c : C) (b : B), P c b
>
> I would like to provide the witness b1 for b at this stage and provide a
> witness for c, different than c1, at a later moment. I tried "eexists;
> exists b1", but Coq didn't allow me to instantiate the existential variable
> created by eexists for c with anything else other than c1, which I don't
> want.

I'm sure there's better ways but my first idea would be to just prove that you
are allowed to swap the quantifiers:

Lemma swap_exists {A B} {P : A -> B -> Prop} :
  (exists (b : B) (a : A), P a b) -> exists (a : A) (b : B), P a b.
Proof.
  firstorder.
Qed.


Justus