Mercurial > cpdt > repo
changeset 148:0952c4ba209b
Templatize Reflection
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 28 Oct 2008 17:03:25 -0400 |
parents | f103f28a6b57 |
children | e70fbfc56c46 |
files | src/Reflection.v |
diffstat | 1 files changed, 11 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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. *)