Mercurial > cpdt > repo

comparison src/Reflection.v @ 143:f3e018e167f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trivial tautologies
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Oct 2008 13:19:33 -0400
parents 6a00d49e85fb
children 5ea9a0bff8f7
comparison
equal deleted inserted replaced
142:6a00d49e85fb 143:f3e018e167f8
134 end" while it is expected to have type "isEven 255" 134 end" while it is expected to have type "isEven 255"
135 ]] 135 ]]
136 136
137 As usual, the type-checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *) 137 As usual, the type-checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *)
138 Abort. 138 Abort.
139
140
141 (** * Reflecting the Syntax of a Trivial Tautology Language *)
142
143 (** We might also like to have reflective proofs of trivial tautologies like this one: *)
144
145 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
146 tauto.
147 Qed.
148
149 Print true_galore.
150
151 (** [[
152
153 true_galore =
154 fun H : True /\ True =>
155 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
156 : True /\ True -> True \/ True /\ (True -> True)
157 ]]
158
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.
160
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: *)
162
163 Inductive taut : Set :=
164 | TautTrue : taut
165 | TautAnd : taut -> taut -> taut
166 | TautOr : taut -> taut -> taut
167 | TautImp : taut -> taut -> taut.
168
169 (** We write a recursive function to "unreflect" this syntax back to [Prop]. *)
170
171 Fixpoint tautDenote (t : taut) : Prop :=
172 match t with
173 | TautTrue => True
174 | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
175 | TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
176 | TautImp t1 t2 => tautDenote t1 -> tautDenote t2
177 end.
178
179 (** It is easy to prove that every formula in the range of [tautDenote] is true. *)
180
181 Theorem tautTrue : forall t, tautDenote t.
182 induction t; crush.
183 Qed.
184
185 (** To use [tautTrue] to prove particular formulas, we need to implement the syntax reflection process. A recursive Ltac function does the job. *)
186
187 Ltac tautReflect P :=
188 match P with
189 | True => TautTrue
190 | ?P1 /\ ?P2 =>
191 let t1 := tautReflect P1 in
192 let t2 := tautReflect P2 in
193 constr:(TautAnd t1 t2)
194 | ?P1 \/ ?P2 =>
195 let t1 := tautReflect P1 in
196 let t2 := tautReflect P2 in
197 constr:(TautOr t1 t2)
198 | ?P1 -> ?P2 =>
199 let t1 := tautReflect P1 in
200 let t2 := tautReflect P2 in
201 constr:(TautImp t1 t2)
202 end.
203
204 (** With [tautReflect] available, it is easy to finish our reflective tactic. We look at the goal formula, reflect it, and apply [tautTrue] to the reflected formula. *)
205
206 Ltac obvious :=
207 match goal with
208 | [ |- ?P ] =>
209 let t := tautReflect P in
210 exact (tautTrue t)
211 end.
212
213 (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *)
214
215 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
216 obvious.
217 Qed.
218
219 Print true_galore'.
220
221 (** [[
222
223 true_galore' =
224 tautTrue
225 (TautImp (TautAnd TautTrue TautTrue)
226 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
227 : True /\ True -> True \/ True /\ (True -> True)
228
229 ]]
230
231 It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reflection 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 %\textit{%#<i>#is#</i>#%}% 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. *)