Mercurial > cpdt > repo
comparison src/StackMachine.v @ 22:91e247c68ee8
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 *) |