Mercurial > cpdt > repo
comparison src/Reflection.v @ 432:17d01e51256c
Pass through Reflection, to incorporate new coqdoc features
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 26 Jul 2012 14:57:38 -0400 |
parents | 5f25705a10ea |
children | 8077352044b2 |
comparison
equal
deleted
inserted
replaced
431:85e743564b22 | 432:17d01e51256c |
---|---|
55 | 55 |
56 The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina. | 56 The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina. |
57 | 57 |
58 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *) | 58 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *) |
59 | 59 |
60 (* begin hide *) | |
61 Definition paartial := partial. | |
62 (* end hide *) | |
63 | |
60 Print partial. | 64 Print partial. |
61 (** %\vspace{-.15in}% [[ | 65 (** %\vspace{-.15in}% [[ |
62 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P] | 66 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P] |
63 | 67 |
64 ]] | 68 ]] |
100 match goal with | 104 match goal with |
101 | [ |- isEven ?N] => exact (partialOut (check_even N)) | 105 | [ |- isEven ?N] => exact (partialOut (check_even N)) |
102 end. | 106 end. |
103 (* end thide *) | 107 (* end thide *) |
104 | 108 |
105 (** We identify which natural number we are considering, and we %``%#"#prove#"#%''% its evenness by pulling the proof out of the appropriate [check_even] call. Recall that the %\index{tactics!exact}%[exact] tactic proves a proposition [P] when given a proof term of precisely type [P]. *) | 109 (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. Recall that the %\index{tactics!exact}%[exact] tactic proves a proposition [P] when given a proof term of precisely type [P]. *) |
106 | 110 |
107 Theorem even_256' : isEven 256. | 111 Theorem even_256' : isEven 256. |
108 prove_even_reflective. | 112 prove_even_reflective. |
109 Qed. | 113 Qed. |
110 | 114 |
154 | 158 |
155 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))). | 159 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))). |
156 tauto. | 160 tauto. |
157 Qed. | 161 Qed. |
158 | 162 |
163 (* begin hide *) | |
164 Definition tg := (and_ind, or_introl). | |
165 (* end hide *) | |
166 | |
159 Print true_galore. | 167 Print true_galore. |
160 (** %\vspace{-.15in}% [[ | 168 (** %\vspace{-.15in}% [[ |
161 true_galore = | 169 true_galore = |
162 fun H : True /\ True => | 170 fun H : True /\ True => |
163 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H | 171 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H |
165 | 173 |
166 ]] | 174 ]] |
167 | 175 |
168 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. | 176 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. |
169 | 177 |
170 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%\index{reification}% _reify_ [Prop] into some type that we _can_ analyze. This inductive type is a good candidate: *) | 178 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%\index{reification}% _reify_ [Prop] into some type that we _can_ analyze. This inductive type is a good candidate: *) |
171 | 179 |
172 (* begin thide *) | 180 (* begin thide *) |
173 Inductive taut : Set := | 181 Inductive taut : Set := |
174 | TautTrue : taut | 182 | TautTrue : taut |
175 | TautAnd : taut -> taut -> taut | 183 | TautAnd : taut -> taut -> taut |
176 | TautOr : taut -> taut -> taut | 184 | TautOr : taut -> taut -> taut |
177 | TautImp : taut -> taut -> taut. | 185 | TautImp : taut -> taut -> taut. |
178 | 186 |
179 (** We write a recursive function to _reflect_ this syntax back to [Prop]. Such functions are also called%\index{interpretation function}% _interpretation functions_, and have used them in previous examples to give semantics to small programming languages. *) | 187 (** We write a recursive function to _reflect_ this syntax back to [Prop]. Such functions are also called%\index{interpretation function}% _interpretation functions_, and we have used them in previous examples to give semantics to small programming languages. *) |
180 | 188 |
181 Fixpoint tautDenote (t : taut) : Prop := | 189 Fixpoint tautDenote (t : taut) : Prop := |
182 match t with | 190 match t with |
183 | TautTrue => True | 191 | TautTrue => True |
184 | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2 | 192 | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2 |
235 (TautImp (TautAnd TautTrue TautTrue) | 243 (TautImp (TautAnd TautTrue TautTrue) |
236 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue)))) | 244 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue)))) |
237 : True /\ True -> True \/ True /\ (True -> True) | 245 : True /\ True -> True \/ True /\ (True -> True) |
238 ]] | 246 ]] |
239 | 247 |
240 It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reification process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the %``%#"#generic proof rule#"#%''% that we apply here _is_ on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it %``%#"#works#"#%''% on any input formula. This is all in addition to the proof-size improvement that we have already seen. | 248 It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reification process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here _is_ on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it "works" on any input formula. This is all in addition to the proof-size improvement that we have already seen. |
241 | 249 |
242 It may also be worth pointing out that our previous example of evenness testing used a function [partialOut] for sound handling of input goals that the verified decision procedure fails to prove. Here, we prove that our procedure [tautTrue] (recall that an inductive proof may be viewed as a recursive procedure) is able to prove any goal representable in [taut], so no extra step is necessary. *) | 250 It may also be worth pointing out that our previous example of evenness testing used a function [partialOut] for sound handling of input goals that the verified decision procedure fails to prove. Here, we prove that our procedure [tautTrue] (recall that an inductive proof may be viewed as a recursive procedure) is able to prove any goal representable in [taut], so no extra step is necessary. *) |
243 | 251 |
244 | 252 |
245 (** * A Monoid Expression Simplifier *) | 253 (** * A Monoid Expression Simplifier *) |
246 | 254 |
247 (** Proof by reflection does not require encoding of all of the syntax in a goal. We can insert %``%#"#variables#"#%''% in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them. In this section, we explore that possibility by writing a tactic for normalizing monoid equations. *) | 255 (** Proof by reflection does not require encoding of all of the syntax in a goal. We can insert "variables" in our syntax types to allow injection of arbitrary pieces, even if we cannot apply specialized reasoning to them. In this section, we explore that possibility by writing a tactic for normalizing monoid equations. *) |
248 | 256 |
249 Section monoid. | 257 Section monoid. |
250 Variable A : Set. | 258 Variable A : Set. |
251 Variable e : A. | 259 Variable e : A. |
252 Variable f : A -> A -> A. | 260 Variable f : A -> A -> A. |
257 Hypothesis identl : forall a, e + a = a. | 265 Hypothesis identl : forall a, e + a = a. |
258 Hypothesis identr : forall a, a + e = a. | 266 Hypothesis identr : forall a, a + e = a. |
259 | 267 |
260 (** 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. | 268 (** 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. |
261 | 269 |
262 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. *) | 270 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. *) |
263 | 271 |
264 (* begin thide *) | 272 (* begin thide *) |
265 Inductive mexp : Set := | 273 Inductive mexp : Set := |
266 | Ident : mexp | 274 | Ident : mexp |
267 | Var : A -> mexp | 275 | Var : A -> mexp |
549 | 557 |
550 Theorem mt2 : forall x y : nat, x = y --> x = y. | 558 Theorem mt2 : forall x y : nat, x = y --> x = y. |
551 my_tauto. | 559 my_tauto. |
552 Qed. | 560 Qed. |
553 | 561 |
562 (* begin hide *) | |
563 Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx). | |
564 (* end hide *) | |
565 | |
554 Print mt2. | 566 Print mt2. |
555 (** %\vspace{-.15in}% [[ | 567 (** %\vspace{-.15in}% [[ |
556 mt2 = | 568 mt2 = |
557 fun x y : nat => | 569 fun x y : nat => |
558 partialOut | 570 partialOut |
608 *) | 620 *) |
609 | 621 |
610 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False. | 622 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False. |
611 tauto. | 623 tauto. |
612 Qed. | 624 Qed. |
625 | |
626 (* begin hide *) | |
627 Definition fi := False_ind. | |
628 (* end hide *) | |
613 | 629 |
614 Print mt4'. | 630 Print mt4'. |
615 (** %\vspace{-.15in}% [[ | 631 (** %\vspace{-.15in}% [[ |
616 mt4' = | 632 mt4' = |
617 fun H : True /\ True /\ True /\ True /\ True /\ True /\ False => | 633 fun H : True /\ True /\ True /\ True /\ True /\ True /\ False => |
693 | 709 |
694 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) | 710 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) |
695 | 711 |
696 Ltac reifyTerm xs e := | 712 Ltac reifyTerm xs e := |
697 match e with | 713 match e with |
698 | True => Truth' | 714 | True => constr:Truth' |
699 | False => Falsehood' | 715 | False => constr:Falsehood' |
700 | ?e1 /\ ?e2 => | 716 | ?e1 /\ ?e2 => |
701 let p1 := reifyTerm xs e1 in | 717 let p1 := reifyTerm xs e1 in |
702 let p2 := reifyTerm xs e2 in | 718 let p2 := reifyTerm xs e2 in |
703 constr:(And' p1 p2) | 719 constr:(And' p1 p2) |
704 | ?e1 \/ ?e2 => | 720 | ?e1 \/ ?e2 => |