Mercurial > cpdt > repo
comparison src/StackMachine.v @ 210:b149a07b9b5b
Most old Sestoft suggestions processed
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 09 Nov 2009 13:18:46 -0500 |
| parents | a7be5d9a2fd4 |
| children | 191a66cd7cb5 |
comparison
equal
deleted
inserted
replaced
| 209:90af611e2993 | 210:b149a07b9b5b |
|---|---|
| 484 induction e; crush. | 484 induction e; crush. |
| 485 Qed. | 485 Qed. |
| 486 | 486 |
| 487 (** 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. | 487 (** 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. |
| 488 | 488 |
| 489 The [crush] tactic comes from the library associated with this book and is not part of the Coq standard library. The book's library contains a number of other tactics that are especially helpful in highly-automated proofs. | |
| 490 | |
| 489 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. *) | 491 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. *) |
| 490 | 492 |
| 491 Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). | 493 Theorem compile_correct : forall e, progDenote (compile e) nil = Some (expDenote e :: nil). |
| 492 intros. | 494 intros. |
| 493 (** [[ | 495 (** [[ |
| 698 match ts with | 700 match ts with |
| 699 | nil => unit | 701 | nil => unit |
| 700 | t :: ts' => typeDenote t * vstack ts' | 702 | t :: ts' => typeDenote t * vstack ts' |
| 701 end%type. | 703 end%type. |
| 702 | 704 |
| 703 (** This is another [Set]-valued function. This time it is recursive, which is perfectly valid, since [Set] is not treated specially in determining which functions may be written. We say that the value stack of an empty stack type is any value of type [unit], which has just a single value, [tt]. A nonempty stack type leads to a value stack that is a pair, whose first element has the proper type and whose second element follows the representation for the remainder of the stack type. | 705 (** This is another [Set]-valued function. This time it is recursive, which is perfectly valid, since [Set] is not treated specially in determining which functions may be written. We say that the value stack of an empty stack type is any value of type [unit], which has just a single value, [tt]. A nonempty stack type leads to a value stack that is a pair, whose first element has the proper type and whose second element follows the representation for the remainder of the stack type. We write [%type] so that Coq knows to interpret [*] as Cartesian product rather than multiplication. |
| 704 | 706 |
| 705 This idea of programming with types can take a while to internalize, but it enables a very simple definition of instruction denotation. Our definition is like what you might expect from a Lisp-like version of ML that ignored type information. Nonetheless, the fact that [tinstrDenote] passes the type-checker guarantees that our stack machine programs can never go wrong. *) | 707 This idea of programming with types can take a while to internalize, but it enables a very simple definition of instruction denotation. Our definition is like what you might expect from a Lisp-like version of ML that ignored type information. Nonetheless, the fact that [tinstrDenote] passes the type-checker guarantees that our stack machine programs can never go wrong. *) |
| 706 | 708 |
| 707 Definition tinstrDenote ts ts' (i : tinstr ts ts') : vstack ts -> vstack ts' := | 709 Definition tinstrDenote ts ts' (i : tinstr ts ts') : vstack ts -> vstack ts' := |
| 708 match i with | 710 match i with |