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