Mercurial > cpdt > repo
comparison src/Reflection.v @ 362:70ffa4d3726e
Template tweaks
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 02 Nov 2011 17:03:25 -0400 |
parents | df17b699a04f |
children | 549d604c3d16 |
comparison
equal
deleted
inserted
replaced
361:df17b699a04f | 362:70ffa4d3726e |
---|---|
143 | 143 |
144 As usual, the type checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *) | 144 As usual, the type checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *) |
145 | 145 |
146 Abort. | 146 Abort. |
147 | 147 |
148 (** Our tactic [prove_even_reflective] is reflective because it performs a proof search process (a trivial one, in this case) wholly within Gallina, where the only use of Ltac is to translate a goal into an appropriate use of [check_even]. *) | 148 (** Our tactic [prove_even_reflective] is reflective because it performs a proof search process (a trivial one, in this case) wholly within Gallina, where the only use of Ltac is to translate a goal into an appropriate use of [check_even]. *) |
149 | 149 |
150 | 150 |
151 (** * Reifying the Syntax of a Trivial Tautology Language *) | 151 (** * Reifying the Syntax of a Trivial Tautology Language *) |
152 | 152 |
153 (** We might also like to have reflective proofs of trivial tautologies like this one: *) | 153 (** We might also like to have reflective proofs of trivial tautologies like this one: *) |
387 | Truth : formula | 387 | Truth : formula |
388 | Falsehood : formula | 388 | Falsehood : formula |
389 | And : formula -> formula -> formula | 389 | And : formula -> formula -> formula |
390 | Or : formula -> formula -> formula | 390 | Or : formula -> formula -> formula |
391 | Imp : formula -> formula -> formula. | 391 | Imp : formula -> formula -> formula. |
392 (* end thide *) | |
392 | 393 |
393 (** The type %\index{Gallina terms!index}%[index] comes from the [Quote] library and represents a countable variable type. The rest of [formula]'s definition should be old hat by now. | 394 (** The type %\index{Gallina terms!index}%[index] comes from the [Quote] library and represents a countable variable type. The rest of [formula]'s definition should be old hat by now. |
394 | 395 |
395 The [quote] tactic will implement injection from [Prop] into [formula] for us, but it is not quite as smart as we might like. In particular, it interprets implications incorrectly, so we will need to declare a wrapper definition for implication, as we did in the last chapter. *) | 396 The [quote] tactic will implement injection from [Prop] into [formula] for us, but it is not quite as smart as we might like. In particular, it interprets implications incorrectly, so we will need to declare a wrapper definition for implication, as we did in the last chapter. *) |
396 | 397 |
399 | 400 |
400 (** Now we can define our denotation function. *) | 401 (** Now we can define our denotation function. *) |
401 | 402 |
402 Definition asgn := varmap Prop. | 403 Definition asgn := varmap Prop. |
403 | 404 |
405 (* begin thide *) | |
404 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop := | 406 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop := |
405 match f with | 407 match f with |
406 | Atomic v => varmap_find False v atomics | 408 | Atomic v => varmap_find False v atomics |
407 | Truth => True | 409 | Truth => True |
408 | Falsehood => False | 410 | Falsehood => False |
409 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2 | 411 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2 |
410 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2 | 412 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2 |
411 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2 | 413 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2 |
412 end. | 414 end. |
415 (* end thide *) | |
413 | 416 |
414 (** The %\index{Gallina terms!varmap}%[varmap] type family implements maps from [index] values. In this case, we define an assignment as a map from variables to [Prop]s. Our reifier [formulaDenote] works with an assignment, and we use the [varmap_find] function to consult the assignment in the [Atomic] case. The first argument to [varmap_find] is a default value, in case the variable is not found. *) | 417 (** The %\index{Gallina terms!varmap}%[varmap] type family implements maps from [index] values. In this case, we define an assignment as a map from variables to [Prop]s. Our reifier [formulaDenote] works with an assignment, and we use the [varmap_find] function to consult the assignment in the [Atomic] case. The first argument to [varmap_find] is a default value, in case the variable is not found. *) |
415 | 418 |
416 Section my_tauto. | 419 Section my_tauto. |
417 Variable atomics : asgn. | 420 Variable atomics : asgn. |
487 end); crush. | 490 end); crush. |
488 Defined. | 491 Defined. |
489 | 492 |
490 (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *) | 493 (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *) |
491 | 494 |
495 (* begin thide *) | |
492 Definition backward : forall (known : set index) (f : formula), | 496 Definition backward : forall (known : set index) (f : formula), |
493 [allTrue known -> formulaDenote atomics f]. | 497 [allTrue known -> formulaDenote atomics f]. |
494 refine (fix F (known : set index) (f : formula) | 498 refine (fix F (known : set index) (f : formula) |
495 : [allTrue known -> formulaDenote atomics f] := | 499 : [allTrue known -> formulaDenote atomics f] := |
496 match f with | 500 match f with |
500 | And f1 f2 => F known f1 && F known f2 | 504 | And f1 f2 => F known f1 && F known f2 |
501 | Or f1 f2 => F known f1 || F known f2 | 505 | Or f1 f2 => F known f1 || F known f2 |
502 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2) | 506 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2) |
503 end); crush; eauto. | 507 end); crush; eauto. |
504 Defined. | 508 Defined. |
509 (* end thide *) | |
505 | 510 |
506 (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *) | 511 (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *) |
507 | 512 |
508 Definition my_tauto : forall f : formula, [formulaDenote atomics f]. | 513 Definition my_tauto : forall f : formula, [formulaDenote atomics f]. |
514 (* begin thide *) | |
509 intro; refine (Reduce (backward nil f)); crush. | 515 intro; refine (Reduce (backward nil f)); crush. |
510 Defined. | 516 Defined. |
517 (* end thide *) | |
511 End my_tauto. | 518 End my_tauto. |
512 | 519 |
513 (** 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 reification for us. Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *) | 520 (** 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 reification for us. Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *) |
514 | 521 |
515 Ltac my_tauto := | 522 Ltac my_tauto := |
625 | 632 |
626 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *) | 633 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *) |
627 | 634 |
628 (** ** Manual Reification of Terms with Variables *) | 635 (** ** Manual Reification of Terms with Variables *) |
629 | 636 |
637 (* begin thide *) | |
630 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced. | 638 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced. |
631 | 639 |
632 Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables. A useful helper function adds an element to a list, maintaining lack of duplicates. Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality. We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *) | 640 Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables. A useful helper function adds an element to a list, maintaining lack of duplicates. Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality. We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *) |
633 | 641 |
634 Ltac inList x xs := | 642 Ltac inList x xs := |
730 ]] | 738 ]] |
731 *) | 739 *) |
732 Abort. | 740 Abort. |
733 | 741 |
734 (** More work would be needed to complete the reflective tactic, as we must connect our new syntax type with the real meanings of formulas, but the details are the same as in our prior implementation with [quote]. *) | 742 (** More work would be needed to complete the reflective tactic, as we must connect our new syntax type with the real meanings of formulas, but the details are the same as in our prior implementation with [quote]. *) |
743 (* end thide *) | |
735 | 744 |
736 | 745 |
737 (** * Exercises *) | 746 (** * Exercises *) |
738 | 747 |
739 (** remove printing * *) | 748 (** remove printing * *) |