Mercurial > cpdt > repo
comparison src/Reflection.v @ 145:617323a60cc4
Monoid code
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 28 Oct 2008 15:28:52 -0400 |
parents | 5ea9a0bff8f7 |
children | 2779c651406a |
comparison
equal
deleted
inserted
replaced
144:5ea9a0bff8f7 | 145:617323a60cc4 |
---|---|
227 : True /\ True -> True \/ True /\ (True -> True) | 227 : True /\ True -> True \/ True /\ (True -> True) |
228 | 228 |
229 ]] | 229 ]] |
230 | 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. *) | 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. *) |
232 | |
233 | |
234 (** * A Monoid Expression Simplifier *) | |
235 | |
236 Section monoid. | |
237 Variable A : Set. | |
238 Variable e : A. | |
239 Variable f : A -> A -> A. | |
240 | |
241 Infix "+" := f. | |
242 | |
243 Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c). | |
244 Hypothesis identl : forall a, e + a = a. | |
245 Hypothesis identr : forall a, a + e = a. | |
246 | |
247 Inductive mexp : Set := | |
248 | Ident : mexp | |
249 | Var : A -> mexp | |
250 | Op : mexp -> mexp -> mexp. | |
251 | |
252 Fixpoint mdenote (me : mexp) : A := | |
253 match me with | |
254 | Ident => e | |
255 | Var v => v | |
256 | Op me1 me2 => mdenote me1 + mdenote me2 | |
257 end. | |
258 | |
259 Fixpoint mldenote (ls : list A) : A := | |
260 match ls with | |
261 | nil => e | |
262 | x :: ls' => x + mldenote ls' | |
263 end. | |
264 | |
265 Fixpoint flatten (me : mexp) : list A := | |
266 match me with | |
267 | Ident => nil | |
268 | Var x => x :: nil | |
269 | Op me1 me2 => flatten me1 ++ flatten me2 | |
270 end. | |
271 | |
272 Lemma flatten_correct' : forall ml2 ml1, f (mldenote ml1) (mldenote ml2) = mldenote (ml1 ++ ml2). | |
273 induction ml1; crush. | |
274 Qed. | |
275 | |
276 Theorem flatten_correct : forall me, mdenote me = mldenote (flatten me). | |
277 Hint Resolve flatten_correct'. | |
278 | |
279 induction me; crush. | |
280 Qed. | |
281 | |
282 Theorem monoid_reflect : forall m1 m2, | |
283 mldenote (flatten m1) = mldenote (flatten m2) | |
284 -> mdenote m1 = mdenote m2. | |
285 intros; repeat rewrite flatten_correct; assumption. | |
286 Qed. | |
287 | |
288 Ltac reflect m := | |
289 match m with | |
290 | e => Ident | |
291 | ?m1 + ?m2 => | |
292 let r1 := reflect m1 in | |
293 let r2 := reflect m2 in | |
294 constr:(Op r1 r2) | |
295 | _ => constr:(Var m) | |
296 end. | |
297 | |
298 Ltac monoid := | |
299 match goal with | |
300 | [ |- ?m1 = ?m2 ] => | |
301 let r1 := reflect m1 in | |
302 let r2 := reflect m2 in | |
303 change (mdenote r1 = mdenote r2); | |
304 apply monoid_reflect; simpl mldenote | |
305 end. | |
306 | |
307 Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d. | |
308 intros. | |
309 monoid. | |
310 reflexivity. | |
311 Qed. | |
312 End monoid. | |
232 | 313 |
233 | 314 |
234 (** * A Smarter Tautology Solver *) | 315 (** * A Smarter Tautology Solver *) |
235 | 316 |
236 Require Import Quote. | 317 Require Import Quote. |