Mercurial > cpdt > repo

comparison src/StackMachine.v @ 22:91e247c68ee8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Template generation
author Adam Chlipala <adamc@hcoop.net>
date Fri, 05 Sep 2008 16:46:32 -0400
parents c0cbf324ec7d
children 26ad686e68f2
comparison
equal deleted inserted replaced
21:00366a62bd00 22:91e247c68ee8
196 196
197 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). 197 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
198 (* begin hide *) 198 (* begin hide *)
199 Abort. 199 Abort.
200 (* end hide *) 200 (* end hide *)
201 (* begin thide *)
201 202
202 (** Though a pencil-and-paper proof might clock out at this point, writing "by a routine induction on [e]," it turns out not to make sense to attack this proof directly. We need to use the standard trick of %\textit{%#<i>#strengthening the induction hypothesis#</i>#%}%. We do that by proving an auxiliary lemma: 203 (** Though a pencil-and-paper proof might clock out at this point, writing "by a routine induction on [e]," it turns out not to make sense to attack this proof directly. We need to use the standard trick of %\textit{%#<i>#strengthening the induction hypothesis#</i>#%}%. We do that by proving an auxiliary lemma:
203 *) 204 *)
204 205
205 Lemma compileCorrect' : forall e p s, progDenote (compile e ++ p) s = progDenote p (expDenote e :: s). 206 Lemma compileCorrect' : forall e p s, progDenote (compile e ++ p) s = progDenote p (expDenote e :: s).
509 510
510 We are almost done. The lefthand and righthand sides can be seen to match by simple symbolic evaluation. That means we are in luck, because Coq identifies any pair of terms as equal whenever they normalize to the same result by symbolic evaluation. By the definition of [progDenote], that is the case here, but we do not need to worry about such details. A simple invocation of [reflexivity] does the normalization and checks that the two results are syntactically equal. *) 511 We are almost done. The lefthand and righthand sides can be seen to match by simple symbolic evaluation. That means we are in luck, because Coq identifies any pair of terms as equal whenever they normalize to the same result by symbolic evaluation. By the definition of [progDenote], that is the case here, but we do not need to worry about such details. A simple invocation of [reflexivity] does the normalization and checks that the two results are syntactically equal. *)
511 512
512 reflexivity. 513 reflexivity.
513 Qed. 514 Qed.
515 (* end thide *)
514 516
515 517
516 (** * Typed Expressions *) 518 (** * Typed Expressions *)
517 519
518 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *) 520 (** In this section, we will build on the initial example by adding additional expression forms that depend on static typing of terms for safety. *)
791 793
792 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 794 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
793 (* begin hide *) 795 (* begin hide *)
794 Abort. 796 Abort.
795 (* end hide *) 797 (* end hide *)
798 (* begin thide *)
796 799
797 (** Again, we need to strengthen the theorem statement so that the induction will go through. This time, I will develop an alternative approach to this kind of proof, stating the key lemma as: *) 800 (** Again, we need to strengthen the theorem statement so that the induction will go through. This time, I will develop an alternative approach to this kind of proof, stating the key lemma as: *)
798 801
799 Lemma tcompileCorrect' : forall t (e : texp t) 802 Lemma tcompileCorrect' : forall t (e : texp t)
800 ts (s : vstack ts), 803 ts (s : vstack ts),
849 Hint Rewrite tcompileCorrect' : cpdt. 852 Hint Rewrite tcompileCorrect' : cpdt.
850 853
851 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 854 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
852 crush. 855 crush.
853 Qed. 856 Qed.
857 (* end thide *)