The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/13/2015 09:44 AM, Soegtrop, Michael wrote:

Dear Coq users,

trying to write my own "Chlipala style" crush tactic, I came across the effect that eapply creates evars which don't have an existential hypothesis:

	Require Import Bool.
	Require Import Vector.

	Class BooleanEqualityT (T : Type) : Type :=
	{
	    eqb       : T -> T -> bool ;
	    eqb_axiom : forall x y, reflect (x = y) (eqb x y)
	}.

	Instance BooleanEquality_vector {T : Type} {Beq : BooleanEqualityT T} (n : nat) : BooleanEqualityT (Vector.t T n).
	  eapply Build_BooleanEqualityT.

Results in:

	1 subgoal
	T : Type
	Beq : BooleanEqualityT T
	n : nat
	______________________________________(1/1)
	forall x y : t T n, reflect (x = y) (?eqb x y)

The strange thing is that the evar ?eqb doesn't appear as existential in the hypothesis. This makes it difficult to detect the evar in automation and to set it.

I am unclear as to what kind of appearance you were expecting.  For example, if you at this point do [set (eqb:=?eqb)], that will generate a local definition that will show up in the hypotheses:

1 subgoal
T : Type
Beq : BooleanEqualityT T
n : nat
eqb := ?eqb : t T n -> t T n -> bool
______________________________________(1/1)
forall x y : t T n, reflect (x = y) (eqb x y)

So the question is: how can I detect in automation that I have such an evar and get its type?

If you want a tactic that can detect occurrences of free evars in the conclusion and generate such local definition hypotheses from them, that is fairly easy to do:

  Ltac gen_evar_local_defs :=
      repeat match goal with |- context[?V] => is_evar V; set V end.

It is possible to do something like this for evars under binders as well.

Or, is there something else you want to occur?

-- Jonathan