From 42d48c6e5807459980e6932b5401d55b94069890 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 16 Jan 2016 20:32:12 -0500
Subject: [PATCH] More examples for first chapter

---
 BasicSyntax.v | 111 ++++++++++++++++++++++++++++++++++++++++++++++++++
 Frap.v        |   6 ++-
 2 files changed, 115 insertions(+), 2 deletions(-)

diff --git a/BasicSyntax.v b/BasicSyntax.v
index ed82e3f..a8adba5 100644
--- a/BasicSyntax.v
+++ b/BasicSyntax.v
@@ -247,4 +247,115 @@ Module ArithWithVariables.
            end; equality || linear_arithmetic || ring.
   Qed.
 
+  Definition isConst (e : arith) : option nat :=
+    match e with
+    | Const n => Some n
+    | _ => None
+    end.
+
+  Fixpoint pushMultiplicationInside' (multiplyBy : nat) (e : arith) : arith :=
+    match e with
+    | Const n => Const (multiplyBy * n)
+    | Var _ => Times (Const multiplyBy) e
+    | Plus e1 e2 => Plus (pushMultiplicationInside' multiplyBy e1)
+                         (pushMultiplicationInside' multiplyBy e2)
+    | Times e1 e2 =>
+      match isConst e1 with
+      | Some k => pushMultiplicationInside' (k * multiplyBy) e2
+      | None => Times (pushMultiplicationInside' multiplyBy e1) e2
+      end
+    end.
+
+  Definition pushMultiplicationInside (e : arith) : arith :=
+    pushMultiplicationInside' 1 e.
+
+  Lemma n_times_0 : forall n, n * 0 = 0.
+  Proof.
+    linear_arithmetic.
+  Qed.
+
+  Lemma depth_pushMultiplicationInside'_irrelevance0 : forall e multiplyBy,
+    depth (pushMultiplicationInside' multiplyBy e)
+    = depth (pushMultiplicationInside' 0 e).
+  Proof.
+    induct e; simplify.
+
+    linear_arithmetic.
+
+    linear_arithmetic.
+
+    rewrite IHe1.
+    rewrite IHe2.
+    linear_arithmetic.
+
+    cases (isConst e1); simplify.
+
+    rewrite IHe2.
+    rewrite n_times_0.
+    linear_arithmetic.
+
+    rewrite IHe1.
+    linear_arithmetic.
+  Qed.
+
+  Lemma depth_pushMultiplicationInside'_irrelevance0_snazzy : forall e multiplyBy,
+    depth (pushMultiplicationInside' multiplyBy e)
+    = depth (pushMultiplicationInside' 0 e).
+  Proof.
+    induct e; simplify;
+    try match goal with
+        | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
+        end; equality.
+  Qed.
+
+  Lemma depth_pushMultiplicationInside'_irrelevance : forall e multiplyBy1 multiplyBy2,
+    depth (pushMultiplicationInside' multiplyBy1 e)
+    = depth (pushMultiplicationInside' multiplyBy2 e).
+  Proof.
+    intros.
+    transitivity (depth (pushMultiplicationInside' 0 e)).
+    apply depth_pushMultiplicationInside'_irrelevance0.
+    symmetry.
+    apply depth_pushMultiplicationInside'_irrelevance0.
+  Qed.
+
+  Lemma depth_pushMultiplicationInside' : forall e,
+    depth (pushMultiplicationInside' 0 e) <= S (depth e).
+  Proof.
+    induct e; simplify.
+
+    linear_arithmetic.
+
+    linear_arithmetic.
+
+    linear_arithmetic.
+
+    cases (isConst e1); simplify.
+
+    rewrite n_times_0.
+    linear_arithmetic.
+
+    linear_arithmetic.
+  Qed.
+
+  Hint Rewrite n_times_0.
+
+  Lemma depth_pushMultiplicationInside'_snazzy : forall e,
+    depth (pushMultiplicationInside' 0 e) <= S (depth e).
+  Proof.
+    induct e; simplify;
+    try match goal with
+        | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
+        end; linear_arithmetic.
+  Qed.
+
+  Theorem depth_pushMultiplicationInside : forall e,
+    depth (pushMultiplicationInside e) <= S (depth e).
+  Proof.
+    simplify.
+    unfold pushMultiplicationInside.
+    rewrite depth_pushMultiplicationInside'_irrelevance0.
+    apply depth_pushMultiplicationInside'.
+  Qed.
+
 End ArithWithVariables.
diff --git a/Frap.v b/Frap.v
index c0a7a78..ca73cd3 100644
--- a/Frap.v
+++ b/Frap.v
@@ -42,9 +42,9 @@ Ltac invert0 e := invert e; fail.
 Ltac invert1 e := invert0 e || (invert e; []).
 Ltac invert2 e := invert1 e || (invert e; [|]).
 
-Ltac simplify := simpl in *.
+Ltac simplify := simpl in *; intros; try autorewrite with core in *.
 
-Ltac linear_arithmetic :=
+Ltac linear_arithmetic := intros;
     repeat match goal with
            | [ |- context[max ?a ?b] ] =>
              let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
@@ -68,3 +68,5 @@ Ltac cases E :=
      | {_} + {_} => destruct E
      | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
      end.
+
+Global Opaque max min.