Prose for third LogicProg section

src/LogicProg.v

@@ -600,11 +600,15 @@ Print length_and_sum''.
 
 (** * Synthesizing Programs *)
 
+(** Here is a simple syntax type for arithmetic expressions, similar to those we have used several times before in the book.  In this case, we allow expressions to mention exactly one distinguished variable. *)
+
 Inductive exp : Set :=
 | Const : nat -> exp
 | Var : exp
 | Plus : exp -> exp -> exp.
 
+(** An inductive relation specifies the semantics of an expression, relating a variable value and an expression to the expression value. *)
+
 Inductive eval (var : nat) : exp -> nat -> Prop :=
 | EvalConst : forall n, eval var (Const n) n
 | EvalVar : eval var Var var
@@ -616,18 +620,24 @@ Inductive eval (var : nat) : exp -> nat -> Prop :=
 Hint Constructors eval.
 (* end thide *)
 
+(** We can use [auto] to execute the semantics for specific expressions. *)
+
 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
 (* begin thide *)
   auto.
 Qed.
 (* end thide *)
 
+(** Unfortunately, just the constructors of [eval] are not enough to prove theorems like the following, which depends on an arithmetic identity. *)
+
 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
 (* begin thide *)
   eauto.
 Abort.
 (* end thide *)
 
+(** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. *)
+
 (* begin thide *)
 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
   -> eval var e2 n2
@@ -638,9 +648,13 @@ Qed.
 
 Hint Resolve EvalPlus'.
 
+(** Further, we instruct [eauto] to apply %\index{tactics!omega}%[omega], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic.  Via [Hint Extern], we ask for use of [omega] on any equality goal.  The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
+
 Hint Extern 1 (_ = _) => abstract omega.
 (* end thide *)
 
+(** Now we can return to [eval1'] and prove it automatically. *)
+
 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
 (* begin thide *)
   eauto.
@@ -648,6 +662,19 @@ Qed.
 (* end thide *)
 
 Print eval1'.
+(** %\vspace{-.15in}%[[
+eval1' = 
+fun var : nat =>
+EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var))
+  (eval1'_subproof var)
+     : forall var : nat,
+       eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
+]]
+*)
+
+(** The lemma [eval1'_subproof] was generated by [abstract omega].
+
+   Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *)
 
 Example synthesize1 : exists e, forall var, eval var e (var + 7).
 (* begin thide *)
@@ -656,6 +683,15 @@ Qed.
 (* end thide *)
 
 Print synthesize1.
+(** %\vspace{-.15in}%[[
+synthesize1 = 
+ex_intro (fun e : exp => forall var : nat, eval var e (var + 7))
+  (Plus Var (Const 7))
+  (fun var : nat => EvalPlus (EvalVar var) (EvalConst var 7))
+]]
+*)
+
+(** Here are two more examples showing off our program synthesis abilities. *)
 
 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
 (* begin thide *)
@@ -663,7 +699,9 @@ Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
 Qed.
 (* end thide *)
 
+(* begin hide *)
 Print synthesize2.
+(* end hide *)
 
 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
 (* begin thide *)
@@ -671,7 +709,13 @@ Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
 Qed.
 (* end thide *)
 
+(* begin hide *)
 Print synthesize3.
+(* end hide *)
+
+(** These examples show linear expressions over the variable [var].  Any such expression is equivalent to [k * var + n] for some [k] and [n].  It is probably not so surprising that we can prove that any expression's semantics is equivalent to some such linear expression, but it is tedious to prove such a fact manually.  To finish this section, we will use [eauto] to complete the proof, finding [k] and [n] values automatically.
+
+   We prove a series of lemmas and add them as hints.  We have alternate [eval] constructor lemmas and some facts about arithmetic. *)
 
 (* begin thide *)
 Theorem EvalConst' : forall var n m, n = m
@@ -709,6 +753,8 @@ Qed.
 
 Hint Resolve plus_0 times_1.
 
+(** We finish with one more arithmetic lemma that is particularly specialized to this theorem.  This fact happens to follow by the axioms of the %\emph{%#<i>#ring#</i>#%}% algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
+
 Require Import Arith Ring.
 
 Theorem combine : forall x k1 k2 n1 n2,
@@ -718,14 +764,20 @@ Qed.
 
 Hint Resolve combine.
 
+(** Our choice of hints is cheating, to an extent, by telegraphing the procedure for choosing values of [k] and [n].  Nonetheless, with these lemmas in place, we achieve an automated proof without explicitly orchestrating the lemmas' composition. *)
+
 Theorem linear : forall e, exists k, exists n,
   forall var, eval var e (k * var + n).
   induction e; crush; eauto.
 Qed.
 
+(* begin hide *)
 Print linear.
+(* end hide *)
 (* end thide *)
 
+(** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *)
+
 
 (** * More on [auto] Hints *)