The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The error means that the variable [x0] was introduced after you constructed the existential [?9649].  Here's a simpler example of the error:

Lemma silly : exists x : nat, forall y, y = x.

  eexists.

  intro y.

  instantiate (1 := y).

Note that this theorem is false (there's no natural number equal to all other natural numbers), but permitting this instantiation would let you prove it.

Another way to look at this is via [Show Proof].  If I [Show Proof.] right after your [inversion H], I get

(fun (P : nat -> nat -> Prop) (H : forall x : nat, exists v : nat, P x v) =>

 ex_intro (fun f : nat -> nat => forall x : nat, P x (f x)) 

   ?314

   (fun x : nat =>

    (fun H0 : exists v : nat, P x v =>

     (fun H1 : P x (?314 x) => H1)

       match H0 with

       | ex_intro x0 H1 => (fun H2 : P x x0 => ?323) H1

       end) (H x)))

Presumably, you were trying to instantiate [?314] with [x0].  But [x0] doesn't exist until the [match], and so you can't "lift" it up outside of the match.

-Jason

On Wed, Jan 16, 2013 at 2:41 AM, Vincent BENAYOUN <benayoun.vincent AT gmail.com> wrote:

Hi all,

I don't understand clearly why I cannot prove the following Lemma, which seems to be a kind of "axiom of dependent choice".

I will be glad if somebody can enlighten me, why I cannot instantiate the existential variable with x0.

I get the following type error :

Toplevel input, characters 16-18:

Error: Instance is not well-typed in the environment of ?9649

Lemma exists_fun :

  forall (P:nat->nat->Prop),

    (forall (x:nat), exists (v:nat), P x v)

    -> exists (f:nat->nat), forall (x:nat), P x (f x).

Proof.

  intros P H.

  refine(ex_intro (fun (f:nat->nat) => forall x : nat, P x (f x)) (fun x => _) _).

  intros x.

  specialize (H x).

  inversion H.

  instantiate (1:=x0).

Thanks in advance,

Vincent