# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1225227805 14400
# Node ID 0952c4ba209bf55fc666305b5da25aa6f61e0fdc
# Parent  f103f28a6b5756ee44936ad2706890c8b64e5161
Templatize Reflection

diff -r f103f28a6b57 -r 0952c4ba209b src/Reflection.v
--- a/src/Reflection.v	Tue Oct 28 16:31:55 2008 -0400
+++ b/src/Reflection.v	Tue Oct 28 17:03:25 2008 -0400
@@ -29,7 +29,9 @@
 | 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.
@@ -65,6 +67,7 @@
 
 (** 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.
 
@@ -93,6 +96,7 @@
   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. *)
 
@@ -160,6 +164,7 @@
 
    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
@@ -211,6 +216,7 @@
   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.
@@ -250,6 +256,7 @@
 
      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
@@ -327,6 +334,8 @@
 
   (** 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.
     (** [[
@@ -367,6 +376,7 @@
 
 Require Import Quote.
 
+(* begin thide *)
 Inductive formula : Set :=
 | Atomic : index -> formula
 | Truth : formula
@@ -507,6 +517,7 @@
   match goal with
     | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f))
   end.
+(* end thide *)
 
 (** A few examples demonstrate how the tactic works. *)