Mercurial > cpdt > repo

comparison src/Reflection.v @ 445:0650420c127b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished vertical spacing
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 17:31:56 -0400
parents 8077352044b2
children b6c47e6d43dc
comparison
equal deleted inserted replaced
444:0d66f1a710b8 445:0650420c127b
42 even_256 = 42 even_256 =
43 Even_SS 43 Even_SS
44 (Even_SS 44 (Even_SS
45 (Even_SS 45 (Even_SS
46 (Even_SS 46 (Even_SS
47
48 ]] 47 ]]
49 48
50 %\noindent%...and so on. This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length super-linear in the input value. Coq's implicit arguments mechanism is hiding the values given for parameter [n] of [Even_SS], which is why the proof term only appears linear here. Also, proof terms are represented internally as syntax trees, with opportunity for sharing of node representations, but in this chapter we will measure proof term size as simple textual length or as the number of nodes in the term's syntax tree, two measures that are approximately equivalent. Sometimes apparently large proof terms have enough internal sharing that they take up less memory than we expect, but one avoids having to reason about such sharing by ensuring that the size of a sharing-free version of a term is low enough. 49 %\noindent%...and so on. This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length super-linear in the input value. Coq's implicit arguments mechanism is hiding the values given for parameter [n] of [Even_SS], which is why the proof term only appears linear here. Also, proof terms are represented internally as syntax trees, with opportunity for sharing of node representations, but in this chapter we will measure proof term size as simple textual length or as the number of nodes in the term's syntax tree, two measures that are approximately equivalent. Sometimes apparently large proof terms have enough internal sharing that they take up less memory than we expect, but one avoids having to reason about such sharing by ensuring that the size of a sharing-free version of a term is low enough.
51 50
52 Superlinear evenness proof terms seem like a shame, since we could write a trivial and trustworthy program to verify evenness of constants. The proof checker could simply call our program where needed. 51 Superlinear evenness proof terms seem like a shame, since we could write a trivial and trustworthy program to verify evenness of constants. The proof checker could simply call our program where needed.
64 (* end hide *) 63 (* end hide *)
65 64
66 Print partial. 65 Print partial.
67 (** %\vspace{-.15in}% [[ 66 (** %\vspace{-.15in}% [[
68 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P] 67 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P]
69
70 ]] 68 ]]
71 69
72 A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *) 70 A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
73 71
74 Local Open Scope partial_scope. 72 Local Open Scope partial_scope.
172 (** %\vspace{-.15in}% [[ 170 (** %\vspace{-.15in}% [[
173 true_galore = 171 true_galore =
174 fun H : True /\ True => 172 fun H : True /\ True =>
175 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H 173 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
176 : True /\ True -> True \/ True /\ (True -> True) 174 : True /\ True -> True \/ True /\ (True -> True)
177
178 ]] 175 ]]
179 176
180 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. 177 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.
181 178
182 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: *) 179 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: *)
238 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))). 235 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
239 obvious. 236 obvious.
240 Qed. 237 Qed.
241 238
242 Print true_galore'. 239 Print true_galore'.
243
244 (** %\vspace{-.15in}% [[ 240 (** %\vspace{-.15in}% [[
245 true_galore' = 241 true_galore' =
246 tautTrue 242 tautTrue
247 (TautImp (TautAnd TautTrue TautTrue) 243 (TautImp (TautAnd TautTrue TautTrue)
248 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue)))) 244 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))