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

comparison src/LogicProg.v @ 374:f3146d40c2a1

Prose for third LogicProg section

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 26 Mar 2012 16:24:19 -0400
parents	b13f76abc724
children	d1276004eec9

comparison

equal deleted inserted replaced

-:b13f76abc724
+:f3146d40c2a1
 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding %\emph{%#<i>#programs#</i>#%}% automatically. *)
 (** * 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
 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
 (* begin thide *)
 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
 -> n1 + n2 = n
 crush.
 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.
 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 *)
 eauto.
 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 *)
 eauto.
 Qed.
 (* end thide *)
+(* begin hide *)
 Print synthesize2.
+(* end hide *)
 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
 (* begin thide *)
 eauto.
 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
 -> eval var (Const n) m.
 crush.
 crush.
 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,
 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
 intros; ring.
 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 thide *)
+(* 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 *)
 (** Another class of built-in tactics includes [auto], [eauto], and [autorewrite].  These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far.  These tactics are important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files.  We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments.

Mercurial > cpdt > repo

comparison src/LogicProg.v @ 374:f3146d40c2a1