How can I specify the value of evariable

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring

11 stars 6 forks source link

How can I specify the value of evariable #118

Open jaewooklee93 opened 9 years ago

jaewooklee93 commented 9 years ago

Using eapply tactics, I made this situation. However, eauto or eassumption doesn't clear the goal. How can I tell Coq that ?59=st''?

H0 : c2 / st' || st''
______________________________________(1/4)
c2 / st' || ?59

jeehoonkang commented 9 years ago

instantiate (1 := st'').

jeehoonkang commented 9 years ago

However, it is strange that eauto cannot solve the goal.
Command Set Printing All. idtac. and see if what appears. If H0 and the goal is identical modulo the evariable, it is really strange..

jaewooklee93 commented 9 years ago

Thank you for your really quick response!

But that command instantiate (1 := st''). gave the following error

Error: Instance is not well-typed in the environment of ?59

H : c1 / st || st'
st'' : state
H0 : c2 / st' || st''
______________________________________(1/5)
c1 / st || ?5655
______________________________________(2/5)
c2 / ?5655 || ?59

First goal was solved by eauto. but it was not working for the second goal.

jeehoonkang commented 9 years ago

That is because the evariable is introduced before st'' is introduced. You have to make sure that the context contains st'' at the time that the evariable is (somehow) introduced.

Jeehoon

jaewooklee93 commented 9 years ago

Hmmm....... Okay, I can solve the goal with exchanging the introducing order of st'' and ?59. But that rule seems quite restrictive. Is it a natural feature of e-tactics? Maybe there is a good reason to make rule in that way, but for me, that restriction is not really intuitive at first glance.

jeehoonkang commented 9 years ago

@jaewooklee93 I agree with you in that the rule is a little bit counter-intuitive. But it has a good reason...

A proof script is, when somehow compiled, transformed into a proof term.
A goal represents a missing part of the proof term. The context of the goal represents bound variables of the proof term to make.
When an evariable is introduced, the evariable is really a placeholder for a sub-term; and the sub-term should be constructed from the bound variables, i.e., the context. Thus the instantiation of an evariable should be a term of the context at the time that the evariable is introduced.