Mercurial > cpdt > repo
comparison src/Reflection.v @ 144:5ea9a0bff8f7
Code for my_tauto
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 28 Oct 2008 14:28:22 -0400 |
parents | f3e018e167f8 |
children | 617323a60cc4 |
comparison
equal
deleted
inserted
replaced
143:f3e018e167f8 | 144:5ea9a0bff8f7 |
---|---|
24 (** * Proving Evenness *) | 24 (** * Proving Evenness *) |
25 | 25 |
26 (** Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure. *) | 26 (** Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure. *) |
27 | 27 |
28 Inductive isEven : nat -> Prop := | 28 Inductive isEven : nat -> Prop := |
29 | Even_O : isEven O | 29 | Even_O : isEven O |
30 | Even_SS : forall n, isEven n -> isEven (S (S n)). | 30 | Even_SS : forall n, isEven n -> isEven (S (S n)). |
31 | 31 |
32 Ltac prove_even := repeat constructor. | 32 Ltac prove_even := repeat constructor. |
33 | 33 |
34 Theorem even_256 : isEven 256. | 34 Theorem even_256 : isEven 256. |
35 prove_even. | 35 prove_even. |
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 Smarter Tautology Solver *) | |
235 | |
236 Require Import Quote. | |
237 | |
238 Inductive formula : Set := | |
239 | Atomic : index -> formula | |
240 | Truth : formula | |
241 | Falsehood : formula | |
242 | And : formula -> formula -> formula | |
243 | Or : formula -> formula -> formula | |
244 | Imp : formula -> formula -> formula. | |
245 | |
246 Definition asgn := varmap Prop. | |
247 | |
248 Definition imp (P1 P2 : Prop) := P1 -> P2. | |
249 Infix "-->" := imp (no associativity, at level 95). | |
250 | |
251 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop := | |
252 match f with | |
253 | Atomic v => varmap_find False v atomics | |
254 | Truth => True | |
255 | Falsehood => False | |
256 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2 | |
257 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2 | |
258 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2 | |
259 end. | |
260 | |
261 Section my_tauto. | |
262 Variable atomics : asgn. | |
263 | |
264 Definition holds (v : index) := varmap_find False v atomics. | |
265 | |
266 Require Import ListSet. | |
267 | |
268 Definition index_eq : forall x y : index, {x = y} + {x <> y}. | |
269 decide equality. | |
270 Defined. | |
271 | |
272 Definition add (s : set index) (v : index) := set_add index_eq v s. | |
273 Definition In_dec : forall v (s : set index), {In v s} + {~In v s}. | |
274 Open Local Scope specif_scope. | |
275 | |
276 intro; refine (fix F (s : set index) : {In v s} + {~In v s} := | |
277 match s return {In v s} + {~In v s} with | |
278 | nil => No | |
279 | v' :: s' => index_eq v' v || F s' | |
280 end); crush. | |
281 Defined. | |
282 | |
283 Fixpoint allTrue (s : set index) : Prop := | |
284 match s with | |
285 | nil => True | |
286 | v :: s' => holds v /\ allTrue s' | |
287 end. | |
288 | |
289 Theorem allTrue_add : forall v s, | |
290 allTrue s | |
291 -> holds v | |
292 -> allTrue (add s v). | |
293 induction s; crush; | |
294 match goal with | |
295 | [ |- context[if ?E then _ else _] ] => destruct E | |
296 end; crush. | |
297 Qed. | |
298 | |
299 Theorem allTrue_In : forall v s, | |
300 allTrue s | |
301 -> set_In v s | |
302 -> varmap_find False v atomics. | |
303 induction s; crush. | |
304 Qed. | |
305 | |
306 Hint Resolve allTrue_add allTrue_In. | |
307 | |
308 Open Local Scope partial_scope. | |
309 | |
310 Definition forward (f : formula) (known : set index) (hyp : formula) | |
311 (cont : forall known', [allTrue known' -> formulaDenote atomics f]) | |
312 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. | |
313 refine (fix F (f : formula) (known : set index) (hyp : formula) | |
314 (cont : forall known', [allTrue known' -> formulaDenote atomics f]){struct hyp} | |
315 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] := | |
316 match hyp return [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] with | |
317 | Atomic v => Reduce (cont (add known v)) | |
318 | Truth => Reduce (cont known) | |
319 | Falsehood => Yes | |
320 | And h1 h2 => | |
321 Reduce (F (Imp h2 f) known h1 (fun known' => | |
322 Reduce (F f known' h2 cont))) | |
323 | Or h1 h2 => F f known h1 cont && F f known h2 cont | |
324 | Imp _ _ => Reduce (cont known) | |
325 end); crush. | |
326 Defined. | |
327 | |
328 Definition backward (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f]. | |
329 refine (fix F (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f] := | |
330 match f return [allTrue known -> formulaDenote atomics f] with | |
331 | Atomic v => Reduce (In_dec v known) | |
332 | Truth => Yes | |
333 | Falsehood => No | |
334 | And f1 f2 => F known f1 && F known f2 | |
335 | Or f1 f2 => F known f1 || F known f2 | |
336 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2) | |
337 end); crush; eauto. | |
338 Defined. | |
339 | |
340 Definition my_tauto (f : formula) : [formulaDenote atomics f]. | |
341 intro; refine (Reduce (backward nil f)); crush. | |
342 Defined. | |
343 End my_tauto. | |
344 | |
345 Ltac my_tauto := | |
346 repeat match goal with | |
347 | [ |- forall x : ?P, _ ] => | |
348 match type of P with | |
349 | Prop => fail 1 | |
350 | _ => intro | |
351 end | |
352 end; | |
353 quote formulaDenote; | |
354 match goal with | |
355 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f)) | |
356 end. | |
357 | |
358 Theorem mt1 : True. | |
359 my_tauto. | |
360 Qed. | |
361 | |
362 Print mt1. | |
363 | |
364 Theorem mt2 : forall x y : nat, x = y --> x = y. | |
365 my_tauto. | |
366 Qed. | |
367 | |
368 Print mt2. | |
369 | |
370 Theorem mt3 : forall x y z, | |
371 (x < y /\ y > z) \/ (y > z /\ x < S y) | |
372 --> y > z /\ (x < y \/ x < S y). | |
373 my_tauto. | |
374 Qed. | |
375 | |
376 Print mt3. | |
377 | |
378 Theorem mt4 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False. | |
379 my_tauto. | |
380 Qed. | |
381 | |
382 Print mt4. | |
383 | |
384 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False. | |
385 tauto. | |
386 Qed. | |
387 | |
388 Print mt4'. |