Mercurial > cpdt > repo
comparison src/Reflection.v @ 361:df17b699a04f
New subsection on Ltac reification
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 02 Nov 2011 16:22:41 -0400 |
parents | e0d91bcf70ec |
children | 70ffa4d3726e |
comparison
equal
deleted
inserted
replaced
360:e0d91bcf70ec | 361:df17b699a04f |
---|---|
622 H9) H7) H5) H3) H1) H | 622 H9) H7) H5) H3) H1) H |
623 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False | 623 : True /\ True /\ True /\ True /\ True /\ True /\ False -> False |
624 ]] | 624 ]] |
625 | 625 |
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. *) | 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. *) |
627 | |
628 (** ** Manual Reification of Terms with Variables *) | |
629 | |
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. | |
631 | |
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. *) | |
633 | |
634 Ltac inList x xs := | |
635 match xs with | |
636 | tt => false | |
637 | (x, _) => true | |
638 | (_, ?xs') => inList x xs' | |
639 end. | |
640 | |
641 Ltac addToList x xs := | |
642 let b := inList x xs in | |
643 match b with | |
644 | true => xs | |
645 | false => constr:(x, xs) | |
646 end. | |
647 | |
648 (** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *) | |
649 | |
650 Ltac allVars xs e := | |
651 match e with | |
652 | True => xs | |
653 | False => xs | |
654 | ?e1 /\ ?e2 => | |
655 let xs := allVars xs e1 in | |
656 allVars xs e2 | |
657 | ?e1 \/ ?e2 => | |
658 let xs := allVars xs e1 in | |
659 allVars xs e2 | |
660 | ?e1 -> ?e2 => | |
661 let xs := allVars xs e1 in | |
662 allVars xs e2 | |
663 | _ => addToList e xs | |
664 end. | |
665 | |
666 (** We will also need a way to map a value to its position in a list. *) | |
667 | |
668 Ltac lookup x xs := | |
669 match xs with | |
670 | (x, _) => O | |
671 | (_, ?xs') => | |
672 let n := lookup x xs' in | |
673 constr:(S n) | |
674 end. | |
675 | |
676 (** The next building block is a procedure for reifying a term, given a list of all allowed variable values. We are free to make this procedure partial, where tactic failure may be triggered upon attempting to reflect a term containing subterms not included in the list of variables. The output type of the term is a copy of [formula] where [index] is replaced by [nat], in the type of the constructor for atomic formulas. *) | |
677 | |
678 Inductive formula' : Set := | |
679 | Atomic' : nat -> formula' | |
680 | Truth' : formula' | |
681 | Falsehood' : formula' | |
682 | And' : formula' -> formula' -> formula' | |
683 | Or' : formula' -> formula' -> formula' | |
684 | Imp' : formula' -> formula' -> formula'. | |
685 | |
686 (** Note that, when we write our own Ltac procedure, we can work directly with the normal [->] operator, rather than needing to introduce a wrapper for it. *) | |
687 | |
688 Ltac reifyTerm xs e := | |
689 match e with | |
690 | True => Truth' | |
691 | False => Falsehood' | |
692 | ?e1 /\ ?e2 => | |
693 let p1 := reifyTerm xs e1 in | |
694 let p2 := reifyTerm xs e2 in | |
695 constr:(And' p1 p2) | |
696 | ?e1 \/ ?e2 => | |
697 let p1 := reifyTerm xs e1 in | |
698 let p2 := reifyTerm xs e2 in | |
699 constr:(Or' p1 p2) | |
700 | ?e1 -> ?e2 => | |
701 let p1 := reifyTerm xs e1 in | |
702 let p2 := reifyTerm xs e2 in | |
703 constr:(Imp' p1 p2) | |
704 | _ => | |
705 let n := lookup e xs in | |
706 constr:(Atomic' n) | |
707 end. | |
708 | |
709 (** Finally, we bring all the pieces together. *) | |
710 | |
711 Ltac reify := | |
712 match goal with | |
713 | [ |- ?G ] => let xs := allVars tt G in | |
714 let p := reifyTerm xs G in | |
715 pose p | |
716 end. | |
717 | |
718 (** A quick test verifies that we are doing reification correctly. *) | |
719 | |
720 Theorem mt3' : forall x y z, | |
721 (x < y /\ y > z) \/ (y > z /\ x < S y) | |
722 -> y > z /\ (x < y \/ x < S y). | |
723 do 3 intro; reify. | |
724 | |
725 (** Our simple tactic adds the translated term as a new variable: | |
726 [[ | |
727 f := Imp' | |
728 (Or' (And' (Atomic' 2) (Atomic' 1)) (And' (Atomic' 1) (Atomic' 0))) | |
729 (And' (Atomic' 1) (Or' (Atomic' 2) (Atomic' 0))) : formula' | |
730 ]] | |
731 *) | |
732 Abort. | |
733 | |
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]. *) | |
627 | 735 |
628 | 736 |
629 (** * Exercises *) | 737 (** * Exercises *) |
630 | 738 |
631 (** remove printing * *) | 739 (** remove printing * *) |