Mercurial > cpdt > repo
comparison src/StackMachine.v @ 394:cc8d0503619f
Citations for continuations and unification
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 22 Apr 2012 15:51:03 -0400 |
| parents | d1276004eec9 |
| children | 05efde66559d |
comparison
equal
deleted
inserted
replaced
| 393:d40b05266306 | 394:cc8d0503619f |
|---|---|
| 812 (** Again, we need to strengthen the theorem statement so that the induction will go through. This time, to provide an excuse to demonstrate different tactics, I will develop an alternative approach to this kind of proof, stating the key lemma as: *) | 812 (** Again, we need to strengthen the theorem statement so that the induction will go through. This time, to provide an excuse to demonstrate different tactics, I will develop an alternative approach to this kind of proof, stating the key lemma as: *) |
| 813 | 813 |
| 814 Lemma tcompile_correct' : forall t (e : texp t) ts (s : vstack ts), | 814 Lemma tcompile_correct' : forall t (e : texp t) ts (s : vstack ts), |
| 815 tprogDenote (tcompile e ts) s = (texpDenote e, s). | 815 tprogDenote (tcompile e ts) s = (texpDenote e, s). |
| 816 | 816 |
| 817 (** While lemma [compile_correct'] quantified over a program that is the %``%#"#continuation#"#%''% for the expression we are considering, here we avoid drawing in any extra syntactic elements. In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it. Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it. | 817 (** While lemma [compile_correct'] quantified over a program that is the %``%#"#continuation#"#%''~\cite{continuations}% for the expression we are considering, here we avoid drawing in any extra syntactic elements. In addition to the source expression and its type, we also quantify over an initial stack type and a stack compatible with it. Running the compilation of the program starting from that stack, we should arrive at a stack that differs only in having the program's denotation pushed onto it. |
| 818 | 818 |
| 819 Let us try to prove this theorem in the same way that we settled on in the last section. *) | 819 Let us try to prove this theorem in the same way that we settled on in the last section. *) |
| 820 | 820 |
| 821 induction e; crush. | 821 induction e; crush. |
| 822 | 822 |