Mercurial > cpdt > repo

comparison src/Reflection.v @ 145:617323a60cc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.