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

comparison src/Reflection.v @ 432:17d01e51256c

Pass through Reflection, to incorporate new coqdoc features

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 26 Jul 2012 14:57:38 -0400
parents	5f25705a10ea
children	8077352044b2

comparison

equal deleted inserted replaced

-:85e743564b22
+:17d01e51256c
 The techniques of proof by reflection address both complaints.  We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *)
+(* begin hide *)
+Definition paartial := partial.
+(* end hide *)
 Print partial.
 (** %\vspace{-.15in}% [[
 Inductive partial (P : Prop) : Set :=  Proved : P -> [P] | Uncertain : [P]
 ]]
 match goal with
 | [ |- isEven ?N] => exact (partialOut (check_even N))
 end.
 (* end thide *)
-(** We identify which natural number we are considering, and we %``%#"#prove#"#%''% its evenness by pulling the proof out of the appropriate [check_even] call.  Recall that the %\index{tactics!exact}%[exact] tactic proves a proposition [P] when given a proof term of precisely type [P]. *)
+(** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call.  Recall that the %\index{tactics!exact}%[exact] tactic proves a proposition [P] when given a proof term of precisely type [P]. *)
 Theorem even_256' : isEven 256.
 prove_even_reflective.
 Qed.
 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
 tauto.
 Qed.
+(* begin hide *)
+Definition tg := (and_ind, or_introl).
+(* end hide *)
 Print true_galore.
 (** %\vspace{-.15in}% [[
 true_galore =
 fun H : True /\ True =>
 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
 ]]
 As we might expect, the proof that [tauto] builds contains explicit applications of natural deduction rules.  For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.
-To write a reflective procedure for this class of goals, we will need to get into the actual %``%#"#reflection#"#%''% part of %``%#"#proof by reflection.#"#%''%  It is impossible to case-analyze a [Prop] in any way in Gallina.  We must%\index{reification}% _reify_ [Prop] into some type that we _can_ analyze.  This inductive type is a good candidate: *)
+To write a reflective procedure for this class of goals, we will need to get into the actual "reflection" part of "proof by reflection."  It is impossible to case-analyze a [Prop] in any way in Gallina.  We must%\index{reification}% _reify_ [Prop] into some type that we _can_ analyze.  This inductive type is a good candidate: *)
 (* begin thide *)
 Inductive taut : Set :=
 | TautTrue : taut
 | TautAnd : taut -> taut -> taut
 | TautOr : taut -> taut -> taut
 | TautImp : taut -> taut -> taut.
-(** We write a recursive function to _reflect_ this syntax back to [Prop].  Such functions are also called%\index{interpretation function}% _interpretation functions_, and have used them in previous examples to give semantics to small programming languages. *)
+(** We write a recursive function to _reflect_ this syntax back to [Prop].  Such functions are also called%\index{interpretation function}% _interpretation functions_, and we have used them in previous examples to give semantics to small programming languages. *)
 Fixpoint tautDenote (t : taut) : Prop :=
 match t with
 | TautTrue => True
 | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
 (TautImp (TautAnd TautTrue TautTrue)
 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
 : True /\ True -> True \/ True /\ (True -> True)
 ]]
-It is worth considering how the reflective tactic improves on a pure-Ltac implementation.  The formula reification process is just as ad-hoc as before, so we gain little there.  In general, proofs will be more complicated than formula translation, and the %``%#"#generic proof rule#"#%''% that we apply here _is_ on much better formal footing than a recursive Ltac function.  The dependent type of the proof guarantees that it %``%#"#works#"#%''% on any input formula.  This is all in addition to the proof-size improvement that we have already seen.
+It is worth considering how the reflective tactic improves on a pure-Ltac implementation.  The formula reification process is just as ad-hoc as before, so we gain little there.  In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here _is_ on much better formal footing than a recursive Ltac function.  The dependent type of the proof guarantees that it "works" on any input formula.  This is all in addition to the proof-size improvement that we have already seen.
 It may also be worth pointing out that our previous example of evenness testing used a function [partialOut] for sound handling of input goals that the verified decision procedure fails to prove.  Here, we prove that our procedure [tautTrue] (recall that an inductive proof may be viewed as a recursive procedure) is able to prove any goal representable in [taut], so no extra step is necessary. *)
 (** * A Monoid Expression Simplifier *)
-(** Proof by reflection does not require encoding of all of the syntax in a goal.  We can insert %``%#"#variables#"#%''% in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them.  In this section, we explore that possibility by writing a tactic for normalizing monoid equations. *)
+(** Proof by reflection does not require encoding of all of the syntax in a goal.  We can insert "variables" in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them.  In this section, we explore that possibility by writing a tactic for normalizing monoid equations. *)
 Section monoid.
 Variable A : Set.
 Variable e : A.
 Variable f : A -> A -> A.
 Hypothesis identl : forall a, e + a = a.
 Hypothesis identr : forall a, a + e = a.
 (** We add variables and hypotheses characterizing an arbitrary instance of the algebraic structure of monoids.  We have an associative binary operator and an identity element for it.
-It is easy to define an expression tree type for monoid expressions.  A [Var] constructor is a %``%#"#catch-all#"#%''% case for subexpressions that we cannot model.  These subexpressions could be actual Gallina variables, or they could just use functions that our tactic is unable to understand. *)
+It is easy to define an expression tree type for monoid expressions.  A [Var] constructor is a "catch-all" case for subexpressions that we cannot model.  These subexpressions could be actual Gallina variables, or they could just use functions that our tactic is unable to understand. *)
 (* begin thide *)
 Inductive mexp : Set :=
 | Ident : mexp
 | Var : A -> mexp
 Theorem mt2 : forall x y : nat, x = y --> x = y.
 my_tauto.
 Qed.
+(* begin hide *)
+Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx).
+(* end hide *)
 Print mt2.
 (** %\vspace{-.15in}% [[
 mt2 =
 fun x y : nat =>
 partialOut
 *)
 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
 tauto.
 Qed.
+(* begin hide *)
+Definition fi := False_ind.
+(* end hide *)
 Print mt4'.
 (** %\vspace{-.15in}% [[
 mt4' =
 fun H : True /\ True /\ True /\ True /\ True /\ True /\ False =>
 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *)
 Ltac reifyTerm xs e :=
 match e with
-| True => Truth'
+| True => constr:Truth'
-| False => Falsehood'
+| False => constr:Falsehood'
 | ?e1 /\ ?e2 =>
 let p1 := reifyTerm xs e1 in
 let p2 := reifyTerm xs e2 in
 constr:(And' p1 p2)
 | ?e1 \/ ?e2 =>

Mercurial > cpdt > repo

comparison src/Reflection.v @ 432:17d01e51256c