coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Partial Evar instantiation, Jason Gross, 03/14/2013
- Re: [Coq-Club] Partial Evar instantiation, Adam Chlipala, 03/14/2013
- Re: [Coq-Club] Partial Evar instantiation, Jason Gross, 03/14/2013
- Re: [Coq-Club] Partial Evar instantiation, Adam Chlipala, 03/15/2013
- Re: [Coq-Club] Partial Evar instantiation, Jason Gross, 03/15/2013
- Re: [Coq-Club] Partial Evar instantiation, Adam Chlipala, 03/15/2013
- Re: [Coq-Club] Partial Evar instantiation, Jason Gross, 03/14/2013
- Re: [Coq-Club] Partial Evar instantiation, Adam Chlipala, 03/14/2013
Archive powered by MHonArc 2.6.18.