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

comparison src/Reflection.v @ 148:0952c4ba209b

Templatize Reflection

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 28 Oct 2008 17:03:25 -0400
parents	f103f28a6b57
children	e70fbfc56c46

comparison

equal deleted inserted replaced

-:f103f28a6b57
+:0952c4ba209b
 Inductive isEven : nat -> Prop :=
 | Even_O : isEven O
 | Even_SS : forall n, isEven n -> isEven (S (S n)).
+(* begin thide *)
 Ltac prove_even := repeat constructor.
+(* end thide *)
 Theorem even_256 : isEven 256.
 prove_even.
 Qed.
 Open Local Scope partial_scope.
 (** We bring into scope some notations for the [partial] type.  These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *)
+(* begin thide *)
 Definition check_even (n : nat) : [isEven n].
 Hint Constructors isEven.
 refine (fix F (n : nat) : [isEven n] :=
 match n return [isEven n] with
 Ltac prove_even_reflective :=
 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. *)
 Theorem even_256' : isEven 256.
 prove_even_reflective.
 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 %\textit{%#<i>#reflect#</i>#%}% [Prop] into some type that we %\textit{%#<i>#can#</i>#%}% 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.
 let t := tautReflect P in
 exact (tautTrue t)
 end.
 (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *)
+(* end thide *)
 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
 obvious.
 Qed.
 (** 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. *)
+(* begin thide *)
 Inductive mexp : Set :=
 | Ident : mexp
 | Var : A -> mexp
 | Op : mexp -> mexp -> mexp.
 apply monoid_reflect; simpl mldenote
 end.
 (** We can make short work of theorems like this one: *)
+(* end thide *)
 Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.
 intros; monoid.
 (** [[
 ============================
 To arrive at a nice implementation satisfying these criteria, we introduce the [quote] tactic and its associated library. *)
 Require Import Quote.
+(* begin thide *)
 Inductive formula : Set :=
 | Atomic : index -> formula
 | Truth : formula
 | Falsehood : formula
 | And : formula -> formula -> formula
 end;
 quote formulaDenote;
 match goal with
 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f))
 end.
+(* end thide *)
 (** A few examples demonstrate how the tactic works. *)
 Theorem mt1 : True.
 my_tauto.

Mercurial > cpdt > repo

comparison src/Reflection.v @ 148:0952c4ba209b