Mercurial > cpdt > repo

comparison src/Reflection.v @ 508:36428dfcde84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Chapter 15
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Feb 2013 19:22:26 -0500
parents 2d66421b8aa1
children ed829eaa91b2
comparison
equal deleted inserted replaced
507:49f3b2d70302 508:36428dfcde84
50 50
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. 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.
52 52
53 It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals. 53 It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.
54 54
55 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. 55 The techniques of proof by reflection address both complaints. We will be able to write proofs like in the example above with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
56 56
57 For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *) 57 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 58
59 (* begin hide *) 59 (* begin hide *)
60 (* begin thide *) 60 (* begin thide *)
243 (TautImp (TautAnd TautTrue TautTrue) 243 (TautImp (TautAnd TautTrue TautTrue)
244 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue)))) 244 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
245 : True /\ True -> True \/ True /\ (True -> True) 245 : True /\ True -> True \/ True /\ (True -> True)
246 ]] 246 ]]
247 247
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. 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 benefit is in addition to the proof-size improvement that we have already seen.
249 249
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. *) 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. *)
251 251
252 252
253 (** * A Monoid Expression Simplifier *) 253 (** * A Monoid Expression Simplifier *)