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

comparison src/Reflection.v @ 362:70ffa4d3726e

Template tweaks

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 02 Nov 2011 17:03:25 -0400
parents	df17b699a04f
children	549d604c3d16

comparison

equal deleted inserted replaced

-:df17b699a04f
+:70ffa4d3726e
 As usual, the type checker performs no reductions to simplify error messages.  If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *)
 Abort.
 (** Our tactic [prove_even_reflective] is reflective because it performs a proof search process (a trivial one, in this case) wholly within Gallina, where the only use of Ltac is to translate a goal into an appropriate use of [check_even]. *)
 (** * Reifying the Syntax of a Trivial Tautology Language *)
 (** We might also like to have reflective proofs of trivial tautologies like this one: *)
 | Truth : formula
 | Falsehood : formula
 | And : formula -> formula -> formula
 | Or : formula -> formula -> formula
 | Imp : formula -> formula -> formula.
+(* end thide *)
 (** The type %\index{Gallina terms!index}%[index] comes from the [Quote] library and represents a countable variable type.  The rest of [formula]'s definition should be old hat by now.
 The [quote] tactic will implement injection from [Prop] into [formula] for us, but it is not quite as smart as we might like.  In particular, it interprets implications incorrectly, so we will need to declare a wrapper definition for implication, as we did in the last chapter. *)
 (** Now we can define our denotation function. *)
 Definition asgn := varmap Prop.
+(* begin thide *)
 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
 match f with
 | Atomic v => varmap_find False v atomics
 | Truth => True
 | Falsehood => False
 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2
 end.
+(* end thide *)
 (** The %\index{Gallina terms!varmap}%[varmap] type family implements maps from [index] values.  In this case, we define an assignment as a map from variables to [Prop]s.  Our reifier [formulaDenote] works with an assignment, and we use the [varmap_find] function to consult the assignment in the [Atomic] case.  The first argument to [varmap_find] is a default value, in case the variable is not found. *)
 Section my_tauto.
 Variable atomics : asgn.
 end); crush.
 Defined.
 (** A [backward] function implements analysis of the final goal.  It calls [forward] to handle implications. *)
+(* begin thide *)
 Definition backward : forall (known : set index) (f : formula),
 [allTrue known -> formulaDenote atomics f].
 refine (fix F (known : set index) (f : formula)
 : [allTrue known -> formulaDenote atomics f] :=
 match f with
 | And f1 f2 => F known f1 && F known f2
 | Or f1 f2 => F known f1 || F known f2
 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2)
 end); crush; eauto.
 Defined.
+(* end thide *)
 (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *)
 Definition my_tauto : forall f : formula, [formulaDenote atomics f].
+(* begin thide *)
 intro; refine (Reduce (backward nil f)); crush.
 Defined.
+(* end thide *)
 End my_tauto.
 (** Our final tactic implementation is now fairly straightforward.  First, we [intro] all quantifiers that do not bind [Prop]s.  Then we call the [quote] tactic, which implements the reification for us.  Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *)
 Ltac my_tauto :=
 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *)
 (** ** Manual Reification of Terms with Variables *)
+(* begin thide *)
 (** The action of the [quote] tactic above may seem like magic.  Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable.  While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well.  To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced.
 Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables.  A useful helper function adds an element to a list, maintaining lack of duplicates.  Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality.  We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *)
 Ltac inList x xs :=
 ]]
 *)
 Abort.
 (** More work would be needed to complete the reflective tactic, as we must connect our new syntax type with the real meanings of formulas, but the details are the same as in our prior implementation with [quote]. *)
+(* end thide *)
 (** * Exercises *)
 (** remove printing * *)

Mercurial > cpdt > repo

comparison src/Reflection.v @ 362:70ffa4d3726e