Certified Programming with Dependent Types: src/StackMachine.v comparison

comparison src/StackMachine.v @ 277:a57e75752c80

PC comments for Chapter 2

author	Adam Chlipala <adam@chlipala.net>
date	Tue, 21 Sep 2010 09:50:33 -0400
parents	a636eda02176
children	e7ed2fddd29a

comparison

equal deleted inserted replaced

-:6c6786a815dd
+:a57e75752c80
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)
 (* begin hide *)
-Require Import List.
+Require Import Arith Bool List.
 Require Import Tactics.
 Set Implicit Arguments.
 (* end hide *)
 (** %\chapter{Some Quick Examples}% *)
 (** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq version 8.2pl1, though parts may work with other versions.
-As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines [Require Import List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source, and be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book.  In either case, you will need to run %\texttt{%#<tt>#make#</tt>#%}% in the root directory of the source distribution for the book before getting started.  If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.
+As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines [Require Import Arith Bool List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source, and be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book.  In either case, you will need to run %\texttt{%#<tt>#make#</tt>#%}% in the root directory of the source distribution for the book before getting started.  If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.
 There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% program.  The best way to add settings that will be shared by many source files is to add a custom variable setting to your %\texttt{%#<tt>#.emacs#</tt>#%}% file, like this:
 %\begin{verbatim}%#<pre>#(custom-set-variables
 ...
 '(coq-prog-args '("-I" "/path/to/cpdt/src"))
 | Const : nat -> exp
 | Binop : binop -> exp -> exp -> exp.
 (** Now we define the type of arithmetic expressions.  We write that a constant may be built from one argument, a natural number; and a binary operation may be built from a choice of operator and two operand expressions.
-A note for readers following along in the PDF version: coqdoc supports pretty-printing of tokens in LaTeX or HTML.  Where you see a right arrow character, the source contains the ASCII text %\texttt{%#<tt>#->#</tt>#%}%.  Other examples of this substitution appearing in this chapter are a double right arrow for %\texttt{%#<tt>#=>#</tt>#%}% and the inverted 'A' symbol for %\texttt{%#<tt>#forall#</tt>#%}%.  When in doubt about the ASCII version of a symbol, you can consult the chapter source code.
+A note for readers following along in the PDF version: coqdoc supports pretty-printing of tokens in LaTeX or HTML.  Where you see a right arrow character, the source contains the ASCII text %\texttt{%#<tt>#->#</tt>#%}%.  Other examples of this substitution appearing in this chapter are a double right arrow for %\texttt{%#<tt>#=>#</tt>#%}%, the inverted 'A' symbol for %\texttt{%#<tt>#forall#</tt>#%}%, and the Cartesian product 'X' for %\texttt{%#<tt>#*#</tt>#%}%.  When in doubt about the ASCII version of a symbol, you can consult the chapter source code.
 %\medskip%
 Now we are ready to say what these programs mean.  We will do this by writing an interpreter that can be thought of as a trivial operational or denotational semantics.  (If you are not familiar with these semantic techniques, no need to worry; we will stick to "common sense" constructions.) *)
 progDenote ((compile e2 ++ compile e1 ++ IBinop b :: nil) ++ p) s =
 progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
 ]]
-What we need is the associative law of list concatenation, available as a theorem [app_ass] in the standard library. *)
+What we need is the associative law of list concatenation, which is available as a theorem [app_ass] in the standard library. *)
 Check app_ass.
 (** [[
 app_ass
 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
+]]
+If we did not already know the name of the theorem, we could use the [SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *)
+SearchRewrite ((_ ++ _) ++ _).
+(** [[
+app_ass: forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
+ass_app: forall (A : Type) (l m n : list A), l ++ m ++ n = (l ++ m) ++ n
 ]]
 We use it to perform a rewrite: *)
 (** We define a trivial language of types to classify our expressions: *)
 Inductive type : Set := Nat | Bool.
-(** Now we define an expanded set of binary operators. *)
+(** Like most programming languages, Coq uses case-sensitive variable names, so that our user-defined type [type] is distinct from the [Type] keyword that we have already seen appear in the statement of a polymorphic theorem (and that we will meet in more detail later), and our constructor names [Nat] and [Bool] are distinct from the types [nat] and [bool] in the standard library.
+Now we define an expanded set of binary operators. *)
 Inductive tbinop : type -> type -> type -> Set :=
 | TPlus : tbinop Nat Nat Nat
 | TTimes : tbinop Nat Nat Nat
 | TEq : forall t, tbinop t t Bool
 | Bool => bool
 end.
 (** It can take a few moments to come to terms with the fact that [Set], the type of types of programs, is itself a first-class type, and that we can write functions that return [Set]s.  Past that wrinkle, the definition of [typeDenote] is trivial, relying on the [nat] and [bool] types from the Coq standard library.
-We need to define a few auxiliary functions, implementing our boolean binary operators that do not appear with the right types in the standard library.  They are entirely standard and ML-like, with the one caveat being that the Coq [nat] type uses a unary representation, where [O] is zero and [S n] is the successor of [n].
+We need to define one auxiliary function, implementing a boolean binary "less-than" operator, which only appears in the standard library with a type fancier than what we are prepared to deal with here.  The code is entirely standard and ML-like, with the one caveat being that the Coq [nat] type uses a unary representation, where [O] is zero and [S n] is the successor of [n].
 *)
-Definition eq_bool (b1 b2 : bool) : bool :=
-match b1, b2 with
-| true, true => true
-| false, false => true
-| _, _ => false
-end.
-Fixpoint eq_nat (n1 n2 : nat) : bool :=
-match n1, n2 with
-| O, O => true
-| S n1', S n2' => eq_nat n1' n2'
-| _, _ => false
-end.
 Fixpoint lt (n1 n2 : nat) : bool :=
 match n1, n2 with
 | O, S _ => true
 | S n1', S n2' => lt n1' n2'
 | _, _ => false
 end.
-(** Now we can interpret binary operators: *)
+(** Now we can interpret binary operators, relying on standard-library equality test functions [eqb] and [beq_nat] for booleans and naturals, respectively: *)
 Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
 : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
 match b in (tbinop arg1 arg2 res)
 return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with
 | TPlus => plus
 | TTimes => mult
-| TEq Nat => eq_nat
+| TEq Nat => beq_nat
-| TEq Bool => eq_bool
+| TEq Bool => eqb
 | TLt => lt
 end.
 (** This function has just a few differences from the denotation functions we saw earlier.  First, [tbinop] is an indexed type, so its indices become additional arguments to [tbinopDenote].  Second, we need to perform a genuine %\textit{%#<i>#dependent pattern match#</i>#%}% to come up with a definition of this function that type-checks.  In each branch of the [match], we need to use branch-specific information about the indices to [tbinop].  General type inference that takes such information into account is undecidable, so it is often necessary to write annotations, like we see above on the line with [match].
 Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
 : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
 match b with
 | TPlus => plus
 | TTimes => mult
-| TEq Nat => eq_nat
+| TEq Nat => beq_nat
-| TEq Bool => eq_bool
+| TEq Bool => eqb
 | TLt => lt
 end.
 (**
 The same tricks suffice to define an expression denotation function in an unsurprising way:

Mercurial > cpdt > repo

comparison src/StackMachine.v @ 277:a57e75752c80