Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Partial Evar instantiation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Partial Evar instantiation


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: Jason Gross <jasongross9 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Partial Evar instantiation
  • Date: Thu, 14 Mar 2013 16:36:35 -0400

Maybe the problem has to do with choosing an evar instantiation that refers to new local variables created since the birth of that evar? I'm a bit confused by the code below, which defines [t] and [t'] but doesn't seem to refer to them. If they were used somehow to instantiate [e], then you would have an instance of the problem I suggested, in which you'd want to do something like [let t0 := eval unfold t in t ...] and refer to [t0] instead of [t].

On 03/14/2013 04:31 PM, Jason Gross wrote:
Is there a systematic way to partially instantiate an evar? That is, if I have an evar [e] and I want to instantiate [e] as [f _ _] for a known [f] (and get the two holes as new evars), is there a way to do that?

I feel like I should be able to do it with something like the following, but I haven't managed to make it work.

Record NT := Build_NT { CO :> forall x : nat, x = x;
HO : CO = CO }.
Goal exists x : NT, x = x.
clear.
esplit.
match goal with
| [ |- appcontext[?e] ] => is_evar e;
let T := fresh in let t := fresh in evar (T : Type); evar (t : T); subst T;
let T' := fresh in let t' := fresh in evar (T' : Type); evar (t' : T'); subst T';
assert (e = @Build_NT (CO e) (HO e))
end.
apply f_equal2.

Thanks,
Jason




Archive powered by MHonArc 2.6.18.

Top of Page