Mercurial > cpdt > repo

comparison src/StackMachine.v @ 26:65314ca099ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Inductive Types
author Adam Chlipala <adamc@hcoop.net>
date Mon, 08 Sep 2008 14:19:50 -0400
parents 26ad686e68f2
children 4887ddb1ad23
comparison
equal deleted inserted replaced
25:26ad686e68f2 26:65314ca099ed
203 203
204 (** ** Translation Correctness *) 204 (** ** Translation Correctness *)
205 205
206 (** We are ready to prove that our compiler is implemented correctly. We can use a new vernacular command [Theorem] to start a correctness proof, in terms of the semantics we defined earlier: *) 206 (** We are ready to prove that our compiler is implemented correctly. We can use a new vernacular command [Theorem] to start a correctness proof, in terms of the semantics we defined earlier: *)
207 207
208 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). 208 Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
209 (* begin hide *) 209 (* begin hide *)
210 Abort. 210 Abort.
211 (* end hide *) 211 (* end hide *)
212 (* begin thide *) 212 (* begin thide *)
213 213
214 (** 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: 214 (** 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:
215 *) 215 *)
216 216
217 Lemma compileCorrect' : forall e p s, progDenote (compile e ++ p) s = progDenote p (expDenote e :: s). 217 Lemma compile_correct' : forall e p s, progDenote (compile e ++ p) s = progDenote p (expDenote e :: s).
218 218
219 (** After the period in the [Lemma] command, we are in %\textit{%#<i>#the interactive proof-editing mode#</i>#%}%. We find ourselves staring at this ominous screen of text: 219 (** After the period in the [Lemma] command, we are in %\textit{%#<i>#the interactive proof-editing mode#</i>#%}%. We find ourselves staring at this ominous screen of text:
220 220
221 [[ 221 [[
222 1 subgoal 222 1 subgoal
466 And there lies our first proof. Already, even for simple theorems like this, the final proof script is unstructured and not very enlightening to readers. If we extend this approach to more serious theorems, we arrive at the unreadable proof scripts that are the favorite complaints of opponents of tactic-based proving. Fortunately, Coq has rich support for scripted automation, and we can take advantage of such a scripted tactic (defined elsewhere) to make short work of this lemma. We abort the old proof attempt and start again. 466 And there lies our first proof. Already, even for simple theorems like this, the final proof script is unstructured and not very enlightening to readers. If we extend this approach to more serious theorems, we arrive at the unreadable proof scripts that are the favorite complaints of opponents of tactic-based proving. Fortunately, Coq has rich support for scripted automation, and we can take advantage of such a scripted tactic (defined elsewhere) to make short work of this lemma. We abort the old proof attempt and start again.
467 *) 467 *)
468 468
469 Abort. 469 Abort.
470 470
471 Lemma compileCorrect' : forall e s p, progDenote (compile e ++ p) s = 471 Lemma compile_correct' : forall e s p, progDenote (compile e ++ p) s =
472 progDenote p (expDenote e :: s). 472 progDenote p (expDenote e :: s).
473 induction e; crush. 473 induction e; crush.
474 Qed. 474 Qed.
475 475
476 (** We need only to state the basic inductive proof scheme and call a tactic that automates the tedious reasoning in between. In contrast to the period tactic terminator from our last proof, the semicolon tactic separator supports structured, compositional proofs. The tactic [t1; t2] has the effect of running [t1] and then running [t2] on each remaining subgoal. The semicolon is one of the most fundamental building blocks of effective proof automation. The period terminator is very useful for exploratory proving, where you need to see intermediate proof states, but final proofs of any serious complexity should have just one period, terminating a single compound tactic that probably uses semicolons. 476 (** We need only to state the basic inductive proof scheme and call a tactic that automates the tedious reasoning in between. In contrast to the period tactic terminator from our last proof, the semicolon tactic separator supports structured, compositional proofs. The tactic [t1; t2] has the effect of running [t1] and then running [t2] on each remaining subgoal. The semicolon is one of the most fundamental building blocks of effective proof automation. The period terminator is very useful for exploratory proving, where you need to see intermediate proof states, but final proofs of any serious complexity should have just one period, terminating a single compound tactic that probably uses semicolons.
477 477
478 The proof of our main theorem is now easy. We prove it with four period-terminated tactics, though separating them with semicolons would work as well; the version here is easier to step through. *) 478 The proof of our main theorem is now easy. We prove it with four period-terminated tactics, though separating them with semicolons would work as well; the version here is easier to step through. *)
479 479
480 Theorem compileCorrect : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). 480 Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil).
481 intros. 481 intros.
482 482
483 (** [[ 483 (** [[
484 484
485 e : exp 485 e : exp
486 ============================ 486 ============================
487 progDenote (compile e) nil = Some (expDenote e :: nil) 487 progDenote (compile e) nil = Some (expDenote e :: nil)
488 ]] 488 ]]
489 489
490 At this point, we want to massage the lefthand side to match the statement of [compileCorrect']. A theorem from the standard library is useful: *) 490 At this point, we want to massage the lefthand side to match the statement of [compile_correct']. A theorem from the standard library is useful: *)
491 491
492 Check app_nil_end. 492 Check app_nil_end.
493 493
494 (** [[ 494 (** [[
495 495
508 progDenote (compile e ++ nil) nil = Some (expDenote e :: nil) 508 progDenote (compile e ++ nil) nil = Some (expDenote e :: nil)
509 ]] 509 ]]
510 510
511 Now we can apply the lemma. *) 511 Now we can apply the lemma. *)
512 512
513 rewrite compileCorrect'. 513 rewrite compile_correct'.
514 514
515 (** [[ 515 (** [[
516 516
517 e : exp 517 e : exp
518 ============================ 518 ============================
800 800
801 (** ** Translation Correctness *) 801 (** ** Translation Correctness *)
802 802
803 (** We can state a correctness theorem similar to the last one. *) 803 (** We can state a correctness theorem similar to the last one. *)
804 804
805 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 805 Theorem tcompile_correct : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
806 (* begin hide *) 806 (* begin hide *)
807 Abort. 807 Abort.
808 (* end hide *) 808 (* end hide *)
809 (* begin thide *) 809 (* begin thide *)
810 810
811 (** 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: *) 811 (** 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: *)
812 812
813 Lemma tcompileCorrect' : forall t (e : texp t) 813 Lemma tcompile_correct' : forall t (e : texp t)
814 ts (s : vstack ts), 814 ts (s : vstack ts),
815 tprogDenote (tcompile e ts) s 815 tprogDenote (tcompile e ts) s
816 = (texpDenote e, s). 816 = (texpDenote e, s).
817 817
818 (** While lemma [compileCorrect'] 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. 818 (** 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.
819 819
820 Let us try to prove this theorem in the same way that we settled on in the last section. *) 820 Let us try to prove this theorem in the same way that we settled on in the last section. *)
821 821
822 induction e; crush. 822 induction e; crush.
823 823
834 834
835 We need an analogue to the [app_ass] theorem that we used to rewrite the goal in the last section. We can abort this proof and prove such a lemma about [tconcat]. 835 We need an analogue to the [app_ass] theorem that we used to rewrite the goal in the last section. We can abort this proof and prove such a lemma about [tconcat].
836 *) 836 *)
837 Abort. 837 Abort.
838 838
839 Lemma tconcatCorrect : forall ts ts' ts'' (p : tprog ts ts') (p' : tprog ts' ts'') 839 Lemma tconcat_correct : forall ts ts' ts'' (p : tprog ts ts') (p' : tprog ts' ts'')
840 (s : vstack ts), 840 (s : vstack ts),
841 tprogDenote (tconcat p p') s 841 tprogDenote (tconcat p p') s
842 = tprogDenote p' (tprogDenote p s). 842 = tprogDenote p' (tprogDenote p s).
843 induction p; crush. 843 induction p; crush.
844 Qed. 844 Qed.
845 845
846 (** This one goes through completely automatically. 846 (** This one goes through completely automatically.
847 847
848 Some code behind the scenes registers [app_ass] for use by [crush]. We must register [tconcatCorrect] similarly to get the same effect: *) 848 Some code behind the scenes registers [app_ass] for use by [crush]. We must register [tconcat_correct] similarly to get the same effect: *)
849 849
850 Hint Rewrite tconcatCorrect : cpdt. 850 Hint Rewrite tconcat_correct : cpdt.
851 851
852 (** We ask that the lemma be used for left-to-right rewriting, and we ask for the hint to be added to the hint database called [cpdt], which is the database used by [crush]. Now we are ready to return to [tcompileCorrect'], proving it automatically this time. *) 852 (** We ask that the lemma be used for left-to-right rewriting, and we ask for the hint to be added to the hint database called [cpdt], which is the database used by [crush]. Now we are ready to return to [tcompile_correct'], proving it automatically this time. *)
853 853
854 Lemma tcompileCorrect' : forall t (e : texp t) 854 Lemma tcompile_correct' : forall t (e : texp t)
855 ts (s : vstack ts), 855 ts (s : vstack ts),
856 tprogDenote (tcompile e ts) s 856 tprogDenote (tcompile e ts) s
857 = (texpDenote e, s). 857 = (texpDenote e, s).
858 induction e; crush. 858 induction e; crush.
859 Qed. 859 Qed.
860 860
861 (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *) 861 (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *)
862 862
863 Hint Rewrite tcompileCorrect' : cpdt. 863 Hint Rewrite tcompile_correct' : cpdt.
864 864
865 Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 865 Theorem tcompile_correct : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
866 crush. 866 crush.
867 Qed. 867 Qed.
868 (* end thide *) 868 (* end thide *)