The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Coq 8.4 (pl6) behaves very, very poorly when dealing with functions which are evars.  Is there any systematic to deal with evars which are functions?

In particular, I am trying dealing with something like the following (except much more complicated, where I do many refinements to split up evars and do rewriting under various binders, etc, before trying to instantiate the evar):

Goal exists f : nat -> nat, ((forall x, f x = x) -> (forall y, f y = y)) -> (forall z, f z = z).
Proof.
  clear; eexists; intros H y.
  refine (_ : (fun w => _) y = _); cbv beta in *.
  Fail revert y. (* The command has indeed failed with message:
=> Error: Refiner was given an argument
    "(?16420:forall y : nat, ?3711 = y) y" of type
   "?3711 = y" instead of "?3711 = y". *)
  match goal with |- ?lhs = _ => set (LHS := lhs) in * end.
  revert y; subst LHS.
  refine (H _); clear H.
  intro x.
  Fail reflexivity. (* Toplevel input, characters 0-11:
Error: Impossible to unify "?3711" with "x".
                     *)
  Fail instantiate (1 := x). (* Error: Instance is not well-typed in the environment of ?3711 *)
  Fail instantiate (1 := z). (* Error: Instance is not well-typed in the environment of ?3711 *)
  instantiate (1 := y).
  Fail reflexivity. (* => Error: Impossible to unify "x" with "_UNBOUND_REL_2". *)
  Fail abstract reflexivity. (* => Error: Impossible to unify "x" with "_UNBOUND_REL_1". *)
  Undo.
  instantiate (1 := w).
  Fail reflexivity. (* Error: Impossible to unify "x" with "_UNBOUND_REL_1". *)
  abstract reflexivity. (* success?! *)
Qed.

Is there any way to automatically discover the appropriate name "w"?  The best I can think of is to walk the structure of the term, unifying it bit by bit, and then try [try (instantiate (1 := v); abstract reflexivity)] for each name v that I introduced in binders anywhere in the proof.  This seems fragile and poor, so I am looking for a better way to do it, that works in Coq 8.4.

Thanks,

Jason