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: Fri, 15 Mar 2013 09:45:20 -0400

On 03/14/2013 04:51 PM, Jason Gross wrote:
Oops. Sorry, I forgot to clean up my code from a previous version of what I tried. I meant to paste

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;
assert (e = @Build_NT (CO e) (HO e))
end.
apply f_equal2.

What I want to do is be able to say that [e] should start with [@Build_NT].

In this case, the assertion is proved easily if you add after [assert]:
by (destruct e; reflexivity)

Here's an example that works the way I want it to:

Goal forall f : nat -> nat -> nat, exists x : nat, x = x.
clear.
intro f.
esplit.
match goal with
| [ |- appcontext[?e] ] => is_evar e;
evar (n : nat);
evar (n' : nat);
assert (e = @f n n') by (apply f_equal2; subst; reflexivity)
end.

(note that [n] and [n'] are dummy evars, which get instantiated by [reflexivity], but aren't used there-after.)
I think the problem I'm having has to do with dependent typing.

This looks like exactly the problem I was describing earlier in the thread, and the solution I proposed works:

match goal with
| [ |- appcontext[?e] ] => is_evar e;
evar (n : nat);
evar (n' : nat);
let n0 := eval unfold n in n in
let n'0 := eval unfold n' in n' in
clear n n'; assert (e = f n0 n'0) by (apply f_equal2; reflexivity)
end.




Archive powered by MHonArc 2.6.18.

Top of Page