Mercurial > cpdt > repo
comparison src/Reflection.v @ 297:b441010125d4
Everything compiles in Coq 8.3pl1
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 14 Jan 2011 14:39:12 -0500 |
parents | 4662b6f099b0 |
children | 7b38729be069 |
comparison
equal
deleted
inserted
replaced
296:559ec7328410 | 297:b441010125d4 |
---|---|
1 (* Copyright (c) 2008-2010, Adam Chlipala | 1 (* Copyright (c) 2008-2011, Adam Chlipala |
2 * | 2 * |
3 * This work is licensed under a | 3 * This work is licensed under a |
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
5 * Unported License. | 5 * Unported License. |
6 * The license text is available at: | 6 * The license text is available at: |
66 Local Open Scope partial_scope. | 66 Local Open Scope partial_scope. |
67 | 67 |
68 (** We bring into scope some notations for the [partial] type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *) | 68 (** We bring into scope some notations for the [partial] type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *) |
69 | 69 |
70 (* begin thide *) | 70 (* begin thide *) |
71 Definition check_even (n : nat) : [isEven n]. | 71 Definition check_even : forall n : nat, [isEven n]. |
72 Hint Constructors isEven. | 72 Hint Constructors isEven. |
73 | 73 |
74 refine (fix F (n : nat) : [isEven n] := | 74 refine (fix F (n : nat) : [isEven n] := |
75 match n with | 75 match n with |
76 | 0 => Yes | 76 | 0 => Yes |
460 | 460 |
461 Local Open Scope partial_scope. | 461 Local Open Scope partial_scope. |
462 | 462 |
463 (** Now we can write a function [forward] which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 6, guaranteeing correctness. The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *) | 463 (** Now we can write a function [forward] which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 6, guaranteeing correctness. The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *) |
464 | 464 |
465 Definition forward (f : formula) (known : set index) (hyp : formula) | 465 Definition forward : forall (f : formula) (known : set index) (hyp : formula) |
466 (cont : forall known', [allTrue known' -> formulaDenote atomics f]) | 466 (cont : forall known', [allTrue known' -> formulaDenote atomics f]), |
467 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. | 467 [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. |
468 refine (fix F (f : formula) (known : set index) (hyp : formula) | 468 refine (fix F (f : formula) (known : set index) (hyp : formula) |
469 (cont : forall known', [allTrue known' -> formulaDenote atomics f]) | 469 (cont : forall known', [allTrue known' -> formulaDenote atomics f]) |
470 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] := | 470 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] := |
471 match hyp with | 471 match hyp with |
472 | Atomic v => Reduce (cont (add known v)) | 472 | Atomic v => Reduce (cont (add known v)) |
480 end); crush. | 480 end); crush. |
481 Defined. | 481 Defined. |
482 | 482 |
483 (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *) | 483 (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *) |
484 | 484 |
485 Definition backward (known : set index) (f : formula) | 485 Definition backward : forall (known : set index) (f : formula), |
486 : [allTrue known -> formulaDenote atomics f]. | 486 [allTrue known -> formulaDenote atomics f]. |
487 refine (fix F (known : set index) (f : formula) | 487 refine (fix F (known : set index) (f : formula) |
488 : [allTrue known -> formulaDenote atomics f] := | 488 : [allTrue known -> formulaDenote atomics f] := |
489 match f with | 489 match f with |
490 | Atomic v => Reduce (In_dec v known) | 490 | Atomic v => Reduce (In_dec v known) |
491 | Truth => Yes | 491 | Truth => Yes |
496 end); crush; eauto. | 496 end); crush; eauto. |
497 Defined. | 497 Defined. |
498 | 498 |
499 (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *) | 499 (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *) |
500 | 500 |
501 Definition my_tauto (f : formula) : [formulaDenote atomics f]. | 501 Definition my_tauto : forall f : formula, [formulaDenote atomics f]. |
502 intro; refine (Reduce (backward nil f)); crush. | 502 intro; refine (Reduce (backward nil f)); crush. |
503 Defined. | 503 Defined. |
504 End my_tauto. | 504 End my_tauto. |
505 | 505 |
506 (** Our final tactic implementation is now fairly straightforward. First, we [intro] all quantifiers that do not bind [Prop]s. Then we call the [quote] tactic, which implements the reflection for us. Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *) | 506 (** Our final tactic implementation is now fairly straightforward. First, we [intro] all quantifiers that do not bind [Prop]s. Then we call the [quote] tactic, which implements the reflection for us. Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *) |