Mercurial > cpdt > repo

comparison src/Reflection.v @ 297:b441010125d4

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