From 5e842c66f71987d7386e99c910a33f86e4caebee Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 6 Feb 2016 18:24:06 -0500
Subject: [PATCH 1/2] Start Interpreters code

---
 Frap.v         |  15 ++--
 Interpreters.v | 218 +++++++++++++++++++++++++++++++++++++++++++++++++
 _CoqProject    |   1 +
 3 files changed, 229 insertions(+), 5 deletions(-)
 create mode 100644 Interpreters.v

diff --git a/Frap.v b/Frap.v
index 02fdddc..0ea8cf2 100644
--- a/Frap.v
+++ b/Frap.v
@@ -3,6 +3,7 @@ Export String Arith Sets Relations Map Var Invariant.
 Require Import List.
 Export List ListNotations.
 Open Scope string_scope.
+Open Scope list_scope.
 
 Ltac inductN n :=
   match goal with
@@ -63,10 +64,14 @@ Ltac linear_arithmetic := intros;
 Ltac equality := congruence.
 
 Ltac cases E :=
-  (is_var E; destruct E)
-  || match type of E with
-     | {_} + {_} => destruct E
-     | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
-     end.
+  ((is_var E; destruct E)
+   || match type of E with
+      | {_} + {_} => destruct E
+      | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
+      end);
+  repeat match goal with
+         | [ H : _ = left _ |- _ ] => clear H
+         | [ H : _ = right _ |- _ ] => clear H
+         end.
 
 Global Opaque max min.
diff --git a/Interpreters.v b/Interpreters.v
new file mode 100644
index 0000000..a28d906
--- /dev/null
+++ b/Interpreters.v
@@ -0,0 +1,218 @@
+(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
+  * Chapter 3: Semantics via Interpreters
+  * Author: Adam Chlipala
+  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
+
+Require Import Frap.
+
+
+(* We begin with a return to our arithmetic language from the last chapter. *)
+Inductive arith : Set :=
+| Const (n : nat)
+| Var (x : var)
+| Plus (e1 e2 : arith)
+| Times (e1 e2 : arith).
+
+Example ex1 := Const 42.
+Example ex2 := Plus (Const 1) (Times (Var "x") (Const 3)).
+
+(* The above definition only explains what programs *look like*.
+ * We also care about what they *mean*.
+ * The natural meaning of an expression is the number it evaluates to.
+ * Actually, it's not quite that simple.
+ * We need to consider the meaning to be a function over a valuation
+ * to the variables, which in turn is itself a function from variable
+ * names to numbers. *)
+Definition valuation := var -> nat.
+
+Fixpoint interp (e : arith) (v : valuation) : nat :=
+  match e with
+  | Const n => n
+  | Var x => v x
+  | Plus e1 e2 => interp e1 v + interp e2 v
+  | Times e1 e2 => interp e1 v * interp e2 v
+  end.
+
+(* Let's sanity-check the interpretation. *)
+Definition valuation0 : valuation :=
+  fun x => if x ==v "x" then 17 else 23.
+
+Compute interp ex1 valuation0.
+Compute interp ex2 valuation0.
+
+(* Here's the silly transformation we defined last time. *)
+Fixpoint commuter (e : arith) : arith :=
+  match e with
+  | Const _ => e
+  | Var _ => e
+  | Plus e1 e2 => Plus (commuter e2) (commuter e1)
+  | Times e1 e2 => Times (commuter e2) (commuter e1)
+  end.
+
+(* Instead of proving various odds-and-ends properties about it,
+ * let's show what we *really* care about: it preserves the
+ * *meanings* of expressions! *)
+Theorem commuter_ok : forall v e, interp (commuter e) v = interp e v.
+Proof.
+  induct e; simplify.
+
+  equality.
+
+  equality.
+
+  linear_arithmetic.
+
+  rewrite IHe1.
+  rewrite IHe2.
+  ring.
+Qed.
+(* Well, that's a relief! ;-) *)
+
+(* Let's also revisit substitution. *)
+Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
+  match inThis with
+  | Const _ => inThis
+  | Var x => if x ==v replaceThis then withThis else inThis
+  | Plus e1 e2 => Plus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
+  | Times e1 e2 => Times (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
+  end.
+
+(* The natural semantic correctness condition for substitution,
+ * drawing on a helper function for adding a new mapping to a valuation *)
+Definition extend_valuation (v : valuation) (x : var) (n : nat) : valuation :=
+  fun y => if y ==v x then n else v y.
+
+Theorem substitute_ok : forall v replaceThis withThis inThis,
+  interp (substitute inThis replaceThis withThis) v
+  = interp inThis (extend_valuation v replaceThis (interp withThis v)).
+Proof.
+  induct inThis; simplify; try equality.
+
+  (* One case left after our basic heuristic:
+   * the variable case, naturally!
+   * A little trick: unfold a definition *before* case analysis,
+   * to expose an extra spot where our test expression appears,
+   * so that it can be handled by [cases] at the same time. *)
+  unfold extend_valuation.
+  cases (x ==v replaceThis); simplify; equality.
+Qed.
+(* Great; we seem to have gotten that one right, too. *)
+
+(* Let's also defined a pared-down version of the expression-simplificaton
+ * functions from last chapter. *)
+Fixpoint doSomeArithmetic (e : arith) : arith :=
+  match e with
+  | Const _ => e
+  | Var _ => e
+  | Plus (Const n1) (Const n2) => Const (n1 + n2)
+  | Plus e1 e2 => Plus (doSomeArithmetic e1) (doSomeArithmetic e2)
+  | Times (Const n1) (Const n2) => Const (n1 * n2)
+  | Times e1 e2 => Times (doSomeArithmetic e1) (doSomeArithmetic e2)
+  end.
+
+Theorem doSomeArithmetic_ok : forall e v, interp (doSomeArithmetic e) v = interp e v.
+Proof.
+  induct e; simplify; try equality.
+
+  cases e1; simplify; try equality.
+  cases e2; simplify; equality.
+
+  cases e1; simplify; try equality.
+  cases e2; simplify; equality.
+Qed.
+
+(* Of course, we're going to get bored if we confine ourselves to arithmetic
+ * expressions for the rest of our journey.  Let's get a bit fancier and define
+ * a *stack machine*, related to postfix calculators that some of you may have
+ * experienced. *)
+Inductive instruction :=
+| PushConst (n : nat)
+| PushVar (x : var)
+| Add
+| Multiply.
+
+(* What does it all mean?  An interpreter tells us unambiguously! *)
+Definition run1 (i : instruction) (v : valuation) (stack : list nat) : list nat :=
+  match i with
+  | PushConst n => n :: stack
+  | PushVar x => v x :: stack
+  | Add =>
+    match stack with
+    | arg2 :: arg1 :: stack' => arg1 + arg2 :: stack'
+    | _ => stack (* arbitrary behavior in erroneous case *)
+    end
+  | Multiply =>
+    match stack with
+    | arg2 :: arg1 :: stack' => arg1 * arg2 :: stack'
+    | _ => stack (* arbitrary behavior in erroneous case *)
+    end
+  end.
+
+(* That function explained how to run one instruction.
+ * Here's how to run several of them. *)
+Fixpoint run (is : list instruction) (v : valuation) (stack : list nat) : list nat :=
+  match is with
+  | nil => stack
+  | i :: is' => run is' v (run1 i v stack)
+  end.
+
+(* Instead of writing fiddly stack programs ourselves, let's *compile*
+ * arithmetic expressions into equivalent stack programs. *)
+Fixpoint compile (e : arith) : list instruction :=
+  match e with
+  | Const n => PushConst n :: nil
+  | Var x => PushVar x :: nil
+  | Plus e1 e2 => compile e1 ++ compile e2 ++ Add :: nil
+  | Times e1 e2 => compile e1 ++ compile e2 ++ Multiply :: nil
+  end.
+
+(* Now, of course, we should prove our compiler correct.
+ * Skip down to the next theorem to see the overall correctness statement.
+ * It turns out that we need to strengthen the induction hypothesis with a
+ * lemma, to push the proof through. *)
+Lemma compile_ok' : forall e v is stack, run (compile e ++ is) v stack = run is v (interp e v :: stack).
+Proof.
+  induct e; simplify.
+
+  equality.
+
+  equality.
+
+  (* Here we want to use associativity of [++], to get the conclusion to match
+   * an induction hypothesis.  Let's ask Coq to search its library for lemmas
+   * that would justify such a rewrite, giving a pattern with wildcards, to
+   * specify the essential structure that the rewrite should match. *)
+  SearchRewrite ((_ ++ _) ++ _).
+  (* Ah, we see just the one! *)
+  rewrite app_assoc_reverse.
+  rewrite IHe1.
+  rewrite app_assoc_reverse.
+  rewrite IHe2.
+  simplify.
+  equality.
+
+  rewrite app_assoc_reverse.
+  rewrite IHe1.
+  rewrite app_assoc_reverse.
+  rewrite IHe2.
+  simplify.
+  equality.
+Qed.
+
+(* The overall theorem follows as a simple corollary. *)
+Theorem compile_ok : forall e v, run (compile e) v nil = interp e v :: nil.
+Proof.
+  simplify.
+
+  (* To match the form of our lemma, we need to replace [compile e] with
+   * [compile e ++ nil], adding a "pointless" concatenation of the empty list.
+   * [SearchRewrite] again helps us find a library lemma. *)
+  SearchRewrite (_ ++ nil).
+  rewrite (app_nil_end (compile e)).
+  (* Note that we can use [rewrite] with explicit values of the first few
+   * quantified variables of a lemma.  Otherwise, [rewrite] picks an
+   * unhelpful place to rewrite.  (Try it and see!) *)
+
+  apply compile_ok'.
+  (* Direct appeal to a previously proved lemma *)
+Qed.
diff --git a/_CoqProject b/_CoqProject
index 7238be3..248bdbb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,3 +6,4 @@ Relations.v
 Frap.v
 BasicSyntax_template.v
 BasicSyntax.v
+Interpreters.v

From ba3bb5c351823100f47d0c62cedea95d54995ac4 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 6 Feb 2016 22:09:37 -0500
Subject: [PATCH 2/2] Interpreters: factorial example

---
 Frap.v         |   4 ++
 Interpreters.v | 188 ++++++++++++++++++++++++++++++++++++++++++-------
 Map.v          |  13 ++--
 Var.v          |   2 +-
 4 files changed, 175 insertions(+), 32 deletions(-)

diff --git a/Frap.v b/Frap.v
index 0ea8cf2..0cee9a3 100644
--- a/Frap.v
+++ b/Frap.v
@@ -75,3 +75,7 @@ Ltac cases E :=
          end.
 
 Global Opaque max min.
+
+Infix "==n" := eq_nat_dec (no associativity, at level 50).
+
+Export Frap.Map.
diff --git a/Interpreters.v b/Interpreters.v
index a28d906..6323b97 100644
--- a/Interpreters.v
+++ b/Interpreters.v
@@ -6,39 +6,44 @@
 Require Import Frap.
 
 
-(* We begin with a return to our arithmetic language from the last chapter. *)
+(* We begin with a return to our arithmetic language from the last chapter,
+ * adding subtraction, which will come in handy later. *)
 Inductive arith : Set :=
 | Const (n : nat)
 | Var (x : var)
 | Plus (e1 e2 : arith)
+| Minus (e1 e2 : arith)
 | Times (e1 e2 : arith).
 
-Example ex1 := Const 42.
-Example ex2 := Plus (Const 1) (Times (Var "x") (Const 3)).
-
 (* The above definition only explains what programs *look like*.
  * We also care about what they *mean*.
  * The natural meaning of an expression is the number it evaluates to.
  * Actually, it's not quite that simple.
  * We need to consider the meaning to be a function over a valuation
- * to the variables, which in turn is itself a function from variable
- * names to numbers. *)
-Definition valuation := var -> nat.
+ * to the variables, which in turn is itself a finite map from variable
+ * names to numbers.  We use the book library's [map] type family. *)
+Definition valuation := map var nat.
 
 Fixpoint interp (e : arith) (v : valuation) : nat :=
   match e with
   | Const n => n
-  | Var x => v x
+  | Var x =>
+    (* Note use of infix operator to look up a key in a finite map. *)
+    match v $? x with
+    | None => 0 (* goofy default value! *)
+    | Some n => n
+    end
   | Plus e1 e2 => interp e1 v + interp e2 v
+  | Minus e1 e2 => interp e1 v - interp e2 v
+                   (* For anyone who's wondering: this [-] sticks at 0,
+                    * if we would otherwise underflow. *)
   | Times e1 e2 => interp e1 v * interp e2 v
   end.
 
-(* Let's sanity-check the interpretation. *)
+(* Here's an example valuation.  Unfortunately, we can't execute code based on
+ * finite maps, since, for convenience, they use uncomputable features. *)
 Definition valuation0 : valuation :=
-  fun x => if x ==v "x" then 17 else 23.
-
-Compute interp ex1 valuation0.
-Compute interp ex2 valuation0.
+  $0 $+ ("x", 17).
 
 (* Here's the silly transformation we defined last time. *)
 Fixpoint commuter (e : arith) : arith :=
@@ -46,6 +51,7 @@ Fixpoint commuter (e : arith) : arith :=
   | Const _ => e
   | Var _ => e
   | Plus e1 e2 => Plus (commuter e2) (commuter e1)
+  | Minus e1 e2 => Minus (commuter e1) (commuter e2)
   | Times e1 e2 => Times (commuter e2) (commuter e1)
   end.
 
@@ -62,6 +68,8 @@ Proof.
 
   linear_arithmetic.
 
+  equality.
+
   rewrite IHe1.
   rewrite IHe2.
   ring.
@@ -74,27 +82,21 @@ Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : ar
   | Const _ => inThis
   | Var x => if x ==v replaceThis then withThis else inThis
   | Plus e1 e2 => Plus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
+  | Minus e1 e2 => Minus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
   | Times e1 e2 => Times (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
   end.
 
-(* The natural semantic correctness condition for substitution,
- * drawing on a helper function for adding a new mapping to a valuation *)
-Definition extend_valuation (v : valuation) (x : var) (n : nat) : valuation :=
-  fun y => if y ==v x then n else v y.
-
+(* Note the use of an infix operator for overriding one entry in a finite
+ * map. *)
 Theorem substitute_ok : forall v replaceThis withThis inThis,
   interp (substitute inThis replaceThis withThis) v
-  = interp inThis (extend_valuation v replaceThis (interp withThis v)).
+  = interp inThis (v $+ (replaceThis, interp withThis v)).
 Proof.
   induct inThis; simplify; try equality.
 
   (* One case left after our basic heuristic:
-   * the variable case, naturally!
-   * A little trick: unfold a definition *before* case analysis,
-   * to expose an extra spot where our test expression appears,
-   * so that it can be handled by [cases] at the same time. *)
-  unfold extend_valuation.
-  cases (x ==v replaceThis); simplify; equality.
+   * the variable case, naturally! *)
+  cases (x ==v replaceThis); simplify; try equality.
 Qed.
 (* Great; we seem to have gotten that one right, too. *)
 
@@ -106,6 +108,7 @@ Fixpoint doSomeArithmetic (e : arith) : arith :=
   | Var _ => e
   | Plus (Const n1) (Const n2) => Const (n1 + n2)
   | Plus e1 e2 => Plus (doSomeArithmetic e1) (doSomeArithmetic e2)
+  | Minus e1 e2 => Minus (doSomeArithmetic e1) (doSomeArithmetic e2)
   | Times (Const n1) (Const n2) => Const (n1 * n2)
   | Times e1 e2 => Times (doSomeArithmetic e1) (doSomeArithmetic e2)
   end.
@@ -129,18 +132,27 @@ Inductive instruction :=
 | PushConst (n : nat)
 | PushVar (x : var)
 | Add
+| Subtract
 | Multiply.
 
 (* What does it all mean?  An interpreter tells us unambiguously! *)
 Definition run1 (i : instruction) (v : valuation) (stack : list nat) : list nat :=
   match i with
   | PushConst n => n :: stack
-  | PushVar x => v x :: stack
+  | PushVar x => (match v $? x with
+                  | None => 0
+                  | Some n => n
+                  end) :: stack
   | Add =>
     match stack with
     | arg2 :: arg1 :: stack' => arg1 + arg2 :: stack'
     | _ => stack (* arbitrary behavior in erroneous case *)
     end
+  | Subtract =>
+    match stack with
+    | arg2 :: arg1 :: stack' => arg1 - arg2 :: stack'
+    | _ => stack (* arbitrary behavior in erroneous case *)
+    end
   | Multiply =>
     match stack with
     | arg2 :: arg1 :: stack' => arg1 * arg2 :: stack'
@@ -163,6 +175,7 @@ Fixpoint compile (e : arith) : list instruction :=
   | Const n => PushConst n :: nil
   | Var x => PushVar x :: nil
   | Plus e1 e2 => compile e1 ++ compile e2 ++ Add :: nil
+  | Minus e1 e2 => compile e1 ++ compile e2 ++ Subtract :: nil
   | Times e1 e2 => compile e1 ++ compile e2 ++ Multiply :: nil
   end.
 
@@ -197,6 +210,13 @@ Proof.
   rewrite IHe2.
   simplify.
   equality.
+
+  rewrite app_assoc_reverse.
+  rewrite IHe1.
+  rewrite app_assoc_reverse.
+  rewrite IHe2.
+  simplify.
+  equality.
 Qed.
 
 (* The overall theorem follows as a simple corollary. *)
@@ -216,3 +236,119 @@ Proof.
   apply compile_ok'.
   (* Direct appeal to a previously proved lemma *)
 Qed.
+
+
+(* Let's get a bit fancier, moving toward the level of general-purpose
+ * imperative languages.  Here's a language of commands, building on the
+ * language of expressions we have defined. *)
+Inductive cmd :=
+| Skip
+| Assign (x : var) (e : arith)
+| Sequence (c1 c2 : cmd)
+| Repeat (e : arith) (body : cmd).
+
+(* That last constructor is for repeating a body command some number of
+ * times.  Note that we sneakily avoid constructs that could introduce
+ * nontermination, since Coq only accepts terminating programs, and we want to
+ * write an interpreter for commands.
+ * In contrast to our last one, this interpreter *transforms valuations*.
+ * We use a helper function for self-composing a function some number of
+ * times. *)
+
+Fixpoint selfCompose {A} (f : A -> A) (n : nat) : A -> A :=
+  match n with
+  | O => fun x => x
+  | S n' => fun x => selfCompose f n' (f x)
+  end.
+
+Fixpoint exec (c : cmd) (v : valuation) : valuation :=
+  match c with
+  | Skip => v
+  | Assign x e => v $+ (x, interp e v)
+  | Sequence c1 c2 => exec c2 (exec c1 v)
+  | Repeat e body => selfCompose (exec body) (interp e v) v
+  end.
+
+(* Let's define some programs and prove that they operate in certain ways. *)
+
+Example factorial_ugly :=
+  Sequence
+    (Assign "output" (Const 1))
+    (Repeat (Var "input")
+            (Sequence
+               (Assign "output" (Times (Var "output") (Var "input")))
+               (Assign "input" (Minus (Var "input") (Const 1))))).
+
+(* Ouch; that code is hard to read.  Let's introduce some notations to make the
+ * concrete syntax more palatable.  We won't explain the general mechanisms on
+ * display here, but see the Coq manual for details, or try to reverse-engineer
+ * them from our examples. *)
+Coercion Const : nat >-> arith.
+Coercion Var : var >-> arith.
+Infix "+" := Plus : arith_scope.
+Infix "-" := Minus : arith_scope.
+Infix "*" := Times : arith_scope.
+Delimit Scope arith_scope with arith.
+Notation "x <- e" := (Assign x e%arith) (at level 75).
+Infix ";" := Sequence (at level 76).
+Notation "'repeat' e 'doing' body 'done'" := (Repeat e%arith body) (at level 75).
+
+(* OK, let's try that program again. *)
+Example factorial :=
+  "output" <- 1;
+  repeat "input" doing
+    "output" <- "output" * "input";
+    "input" <- "input" - 1
+  done.
+
+(* Now we prove that it really computes factorial.
+ * First, a reference implementation as a functional program. *)
+Fixpoint fact (n : nat) : nat :=
+  match n with
+  | O => 1
+  | S n' => n * fact n'
+  end.
+
+Definition factorial_body :=
+  "output" <- "output" * "input";
+  "input" <- "input" - 1.
+
+(* Note that here we're careful to put the quantified variable [input] *first*,
+ * because the variables coming after it will need to *change* in the course of
+ * the induction.  Try switching the order to see what goes wrong if we put
+ * [input] later. *)
+Lemma factorial_ok' : forall input output v,
+  v $? "input" = Some input
+  -> v $? "output" = Some output
+  -> selfCompose (exec factorial_body) input v
+     = v $+ ("input", 0) $+ ("output", output * fact input).
+Proof.
+  induct input; simplify.
+
+  maps_equal; simplify.
+
+  rewrite H0.
+  f_equal.
+  linear_arithmetic.
+
+  trivial.
+
+  rewrite H, H0.
+  rewrite (IHinput (output * S input)).
+  maps_equal; simplify.
+  f_equal; ring.
+  simplify; f_equal; linear_arithmetic.
+  simplify; equality.
+Qed.
+
+Theorem factorial_ok : forall v input,
+  v $? "input" = Some input
+  -> exec factorial v $? "output" = Some (fact input).
+Proof.
+  simplify.
+  rewrite H.
+  rewrite (factorial_ok' input 1); simplify.
+  f_equal; linear_arithmetic.
+  trivial.
+  trivial.
+Qed.
diff --git a/Map.v b/Map.v
index 77f1aea..cb2f47d 100644
--- a/Map.v
+++ b/Map.v
@@ -34,8 +34,9 @@ Module Type S.
     m $<= m'
     -> add m k v $<= add m' k v.
 
-  Axiom lookup_add_eq : forall A B (m : map A B) k v,
-    add m k v $? k = Some v.
+  Axiom lookup_add_eq : forall A B (m : map A B) k1 k2 v,
+    k1 = k2
+    -> add m k1 v $? k2 = Some v.
 
   Axiom lookup_add_ne : forall A B (m : map A B) k k' v,
     k' <> k
@@ -142,11 +143,13 @@ Module M : S.
     destruct (decide (k0 = k)); auto.
   Qed.
 
-  Theorem lookup_add_eq : forall A B (m : map A B) k v,
-    lookup (add m k v) k = Some v.
+  Theorem lookup_add_eq : forall A B (m : map A B) k1 k2 v,
+    k1 = k2
+    -> lookup (add m k1 v) k2 = Some v.
   Proof.
     unfold lookup, add; intuition.
-    destruct (decide (k = k)); tauto.
+    destruct (decide (k2 = k1)); try tauto.
+    congruence.
   Qed.
 
   Theorem lookup_add_ne : forall A B (m : map A B) k k' v,
diff --git a/Var.v b/Var.v
index b042217..787873c 100644
--- a/Var.v
+++ b/Var.v
@@ -1,7 +1,7 @@
 Require Import String.
 
 
-Definition var := string.
+Notation var := string.
 Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec.
 
 Infix "==v" := var_eq (no associativity, at level 50).