The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

 

thanks, this helps! Maybe I am mixing up some things here, but I thought that for most evars I have seen so far, some hypothesis gave the type of the evar. In general I would like to have a way to match on all free evars (not only those occurring in the goal) and their type. Your Ltac script is easily extended to this, but I wonder how efficient it is, when applied repeatedly in some automation script.

 

Maybe it is better to avoid creation of evars in automation in the first place. I am experimenting a bit and see what works well and what results in problems.

 

Best regards,

 

Michael

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Jonathan Leivent
Sent: Friday, February 13, 2015 4:49 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to handle "invisible" evars created by eapply?

 

 

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