Mercurial > cpdt > repo
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
147:f103f28a6b57 | 148:0952c4ba209b |
---|---|
27 | 27 |
28 Inductive isEven : nat -> Prop := | 28 Inductive isEven : nat -> Prop := |
29 | Even_O : isEven O | 29 | Even_O : isEven O |
30 | Even_SS : forall n, isEven n -> isEven (S (S n)). | 30 | Even_SS : forall n, isEven n -> isEven (S (S n)). |
31 | 31 |
32 (* begin thide *) | |
32 Ltac prove_even := repeat constructor. | 33 Ltac prove_even := repeat constructor. |
34 (* end thide *) | |
33 | 35 |
34 Theorem even_256 : isEven 256. | 36 Theorem even_256 : isEven 256. |
35 prove_even. | 37 prove_even. |
36 Qed. | 38 Qed. |
37 | 39 |
63 | 65 |
64 Open Local Scope partial_scope. | 66 Open Local Scope partial_scope. |
65 | 67 |
66 (** 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. *) | 68 (** 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. *) |
67 | 69 |
70 (* begin thide *) | |
68 Definition check_even (n : nat) : [isEven n]. | 71 Definition check_even (n : nat) : [isEven n]. |
69 Hint Constructors isEven. | 72 Hint Constructors isEven. |
70 | 73 |
71 refine (fix F (n : nat) : [isEven n] := | 74 refine (fix F (n : nat) : [isEven n] := |
72 match n return [isEven n] with | 75 match n return [isEven n] with |
91 | 94 |
92 Ltac prove_even_reflective := | 95 Ltac prove_even_reflective := |
93 match goal with | 96 match goal with |
94 | [ |- isEven ?N] => exact (partialOut (check_even N)) | 97 | [ |- isEven ?N] => exact (partialOut (check_even N)) |
95 end. | 98 end. |
99 (* end thide *) | |
96 | 100 |
97 (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. *) | 101 (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. *) |
98 | 102 |
99 Theorem even_256' : isEven 256. | 103 Theorem even_256' : isEven 256. |
100 prove_even_reflective. | 104 prove_even_reflective. |
158 | 162 |
159 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. | 163 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. |
160 | 164 |
161 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: *) | 165 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: *) |
162 | 166 |
167 (* begin thide *) | |
163 Inductive taut : Set := | 168 Inductive taut : Set := |
164 | TautTrue : taut | 169 | TautTrue : taut |
165 | TautAnd : taut -> taut -> taut | 170 | TautAnd : taut -> taut -> taut |
166 | TautOr : taut -> taut -> taut | 171 | TautOr : taut -> taut -> taut |
167 | TautImp : taut -> taut -> taut. | 172 | TautImp : taut -> taut -> taut. |
209 let t := tautReflect P in | 214 let t := tautReflect P in |
210 exact (tautTrue t) | 215 exact (tautTrue t) |
211 end. | 216 end. |
212 | 217 |
213 (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *) | 218 (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *) |
219 (* end thide *) | |
214 | 220 |
215 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))). | 221 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))). |
216 obvious. | 222 obvious. |
217 Qed. | 223 Qed. |
218 | 224 |
248 | 254 |
249 (** 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. | 255 (** 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. |
250 | 256 |
251 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. *) | 257 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. *) |
252 | 258 |
259 (* begin thide *) | |
253 Inductive mexp : Set := | 260 Inductive mexp : Set := |
254 | Ident : mexp | 261 | Ident : mexp |
255 | Var : A -> mexp | 262 | Var : A -> mexp |
256 | Op : mexp -> mexp -> mexp. | 263 | Op : mexp -> mexp -> mexp. |
257 | 264 |
325 apply monoid_reflect; simpl mldenote | 332 apply monoid_reflect; simpl mldenote |
326 end. | 333 end. |
327 | 334 |
328 (** We can make short work of theorems like this one: *) | 335 (** We can make short work of theorems like this one: *) |
329 | 336 |
337 (* end thide *) | |
338 | |
330 Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d. | 339 Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d. |
331 intros; monoid. | 340 intros; monoid. |
332 (** [[ | 341 (** [[ |
333 | 342 |
334 ============================ | 343 ============================ |
365 | 374 |
366 To arrive at a nice implementation satisfying these criteria, we introduce the [quote] tactic and its associated library. *) | 375 To arrive at a nice implementation satisfying these criteria, we introduce the [quote] tactic and its associated library. *) |
367 | 376 |
368 Require Import Quote. | 377 Require Import Quote. |
369 | 378 |
379 (* begin thide *) | |
370 Inductive formula : Set := | 380 Inductive formula : Set := |
371 | Atomic : index -> formula | 381 | Atomic : index -> formula |
372 | Truth : formula | 382 | Truth : formula |
373 | Falsehood : formula | 383 | Falsehood : formula |
374 | And : formula -> formula -> formula | 384 | And : formula -> formula -> formula |
505 end; | 515 end; |
506 quote formulaDenote; | 516 quote formulaDenote; |
507 match goal with | 517 match goal with |
508 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f)) | 518 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f)) |
509 end. | 519 end. |
520 (* end thide *) | |
510 | 521 |
511 (** A few examples demonstrate how the tactic works. *) | 522 (** A few examples demonstrate how the tactic works. *) |
512 | 523 |
513 Theorem mt1 : True. | 524 Theorem mt1 : True. |
514 my_tauto. | 525 my_tauto. |