Mercurial > cpdt > repo

comparison src/LogicProg.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents f3146d40c2a1
children 3c941750c347
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
779 (** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *) 779 (** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *)
780 780
781 781
782 (** * More on [auto] Hints *) 782 (** * More on [auto] Hints *)
783 783
784 (** Another class of built-in tactics includes [auto], [eauto], and [autorewrite]. These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. These tactics are important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. 784 (** Let us stop at this point and take stock of the possibilities for [auto] and [eauto] hints. Hints are contained within %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. When no hint database is specified, a default database is used. Hints in the default database are always used by [auto] or [eauto]. The chance to extend hint databases imperatively is important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. In fact, [crush] is defined in terms of [auto], which explains how we achieve this extensibility. Other user-defined tactics can take similar advantage of [auto] and [eauto].
785 785
786 The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; [Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and [Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5. 786 The basic hints for [auto] and [eauto] are %\index{Vernacular commands!Hint Immediate}%[Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; %\index{Vernacular commands!Hint Resolve}%[Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; %\index{Vernacular commands!Hint Constructors}%[Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and %\index{Vernacular commands!Hint Unfold}%[Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5.
787 787
788 All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few examples should do best to explain how [Hint Extern] works. *) 788 All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *)
789 789
790 Theorem bool_neq : true <> false. 790 Theorem bool_neq : true <> false.
791 (* begin thide *) 791 (* begin thide *)
792 auto. 792 auto.
793 793
794 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *) 794 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
795 795
796 Abort. 796 Abort.
797 797
798 (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices. *) 798 (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices, by appealing to the built-in tactic %\index{tactics!congruence}%[congruence], a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors. *)
799 799
800 Hint Extern 1 (_ <> _) => congruence. 800 Hint Extern 1 (_ <> _) => congruence.
801 801
802 Theorem bool_neq : true <> false. 802 Theorem bool_neq : true <> false.
803 auto. 803 auto.
804 Qed. 804 Qed.
805 (* end thide *) 805 (* end thide *)
806 806
807 (** Our hint says: %``%#"#whenever the conclusion matches the pattern [_ <> _], try applying [congruence].#"#%''% The [1] is a cost for this rule. During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints. 807 (** [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
808
809 [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
810 808
811 Section forall_and. 809 Section forall_and.
812 Variable A : Set. 810 Variable A : Set.
813 Variables P Q : A -> Prop. 811 Variables P Q : A -> Prop.
814 812
816 814
817 Theorem forall_and : forall z, P z. 815 Theorem forall_and : forall z, P z.
818 (* begin thide *) 816 (* begin thide *)
819 crush. 817 crush.
820 818
821 (** [crush] makes no progress beyond what [intros] would have accomplished. [auto] will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal. However, we can teach [auto] to handle this kind of goal. *) 819 (** The [crush] invocation makes no progress beyond what [intros] would have accomplished. An [auto] invocation will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal. However, we can teach [auto] to handle this kind of goal. *)
822 820
823 Hint Extern 1 (P ?X) => 821 Hint Extern 1 (P ?X) =>
824 match goal with 822 match goal with
825 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X)) 823 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
826 end. 824 end.
827 825
828 auto. 826 auto.
829 Qed. 827 Qed.
830 (* end thide *) 828 (* end thide *)
831 829
832 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *) 830 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. The function [proj1] is from the standard library, for extracting a proof of [R] from a proof of [R /\ S]. *)
833 831
834 End forall_and. 832 End forall_and.
835 833
836 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P]. 834 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
837
838 [[ 835 [[
839 Hint Extern 1 (?P ?X) => 836 Hint Extern 1 (?P ?X) =>
840 match goal with 837 match goal with
841 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X)) 838 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
842 end. 839 end.
843 840 ]]
841 <<
844 User error: Bound head variable 842 User error: Bound head variable
845 843 >>
846 ]] 844
847 845 Coq's [auto] hint databases work as tables mapping %\index{head symbol}\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
848 Coq's [auto] hint databases work as tables mapping %\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P]. 846
849 847 Fortunately, a more basic form of [Hint Extern] also applies. We may simply leave out the pattern to the left of the [=>], incorporating the corresponding logic into the Ltac script. *)
850 This restriction on [Extern] hints is the main limitation of the [auto] mechanism, preventing us from using it for general context simplifications that are not keyed off of the form of the conclusion. This is perhaps just as well, since we can often code more efficient tactics with specialized Ltac programs, and we will see how in the next chapter. *) 848
849 Hint Extern 1 =>
850 match goal with
851 | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X))
852 end.
853
854 (** Be forewarned that a [Hint Extern] of this kind will be applied at %\emph{%#<i>#every#</i>#%}% node of a proof tree, so an expensive Ltac script may slow proof search significantly. *)
851 855
852 856
853 (** * Rewrite Hints *) 857 (** * Rewrite Hints *)
854 858
855 (** We have used [Hint Rewrite] in many examples so far. [crush] uses these hints by calling [autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma : cpdt], adding them to the [cpdt] rewrite database. This is because, in contrast to [auto], [autorewrite] has no default database. Thus, we set the convention that [crush] uses the [cpdt] database. 859 (** Another dimension of extensibility with hints is rewriting with quantified equalities. We have used the associated command %\index{Vernacular commands!Hint Rewrite}%[Hint Rewrite] in many examples so far. The [crush] tactic uses these hints by calling the built-in tactic %\index{tactics!autorewrite}%[autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma], which by default adds them to the default hint database [core]; but alternate hint databases may also be specified just as with, e.g., [Hint Resolve].
856 860
857 This example shows a direct use of [autorewrite]. *) 861 The next example shows a direct use of [autorewrite]. Note that, while [Hint Rewrite] uses a default database, [autorewrite] requires that a database be named. *)
858 862
859 Section autorewrite. 863 Section autorewrite.
860 Variable A : Set. 864 Variable A : Set.
861 Variable f : A -> A. 865 Variable f : A -> A.
862 866
863 Hypothesis f_f : forall x, f (f x) = f x. 867 Hypothesis f_f : forall x, f (f x) = f x.
864 868
865 Hint Rewrite f_f : my_db. 869 Hint Rewrite f_f.
866 870
867 Lemma f_f_f : forall x, f (f (f x)) = f x. 871 Lemma f_f_f : forall x, f (f (f x)) = f x.
868 intros; autorewrite with my_db; reflexivity. 872 intros; autorewrite with core; reflexivity.
869 Qed. 873 Qed.
870 874
871 (** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints. First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate. Second, we may add hints that %``%#"#lead [autorewrite] down the wrong path.#"#%''% For instance: *) 875 (** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints. First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate. Second, we may add hints that %``%#"#lead [autorewrite] down the wrong path.#"#%''% For instance: *)
872 876
873 Section garden_path. 877 Section garden_path.
874 Variable g : A -> A. 878 Variable g : A -> A.
875 Hypothesis f_g : forall x, f x = g x. 879 Hypothesis f_g : forall x, f x = g x.
876 Hint Rewrite f_g : my_db. 880 Hint Rewrite f_g.
877 881
878 Lemma f_f_f' : forall x, f (f (f x)) = f x. 882 Lemma f_f_f' : forall x, f (f (f x)) = f x.
879 intros; autorewrite with my_db. 883 intros; autorewrite with core.
880 (** [[ 884 (** [[
881 ============================ 885 ============================
882 g (g (g x)) = g x 886 g (g (g x)) = g x
883 ]] 887 ]]
884 *) 888 *)
887 891
888 (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied. This %``%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %``%#"#break#"#%''% old proofs. The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them. The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *) 892 (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied. This %``%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %``%#"#break#"#%''% old proofs. The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them. The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
889 893
890 Reset garden_path. 894 Reset garden_path.
891 895
892 (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *) 896 (** The [autorewrite] tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
893 897
894 Section garden_path. 898 Section garden_path.
895 Variable P : A -> Prop. 899 Variable P : A -> Prop.
896 Variable g : A -> A. 900 Variable g : A -> A.
897 Hypothesis f_g : forall x, P x -> f x = g x. 901 Hypothesis f_g : forall x, P x -> f x = g x.
898 Hint Rewrite f_g : my_db. 902 Hint Rewrite f_g.
899 903
900 Lemma f_f_f' : forall x, f (f (f x)) = f x. 904 Lemma f_f_f' : forall x, f (f (f x)) = f x.
901 intros; autorewrite with my_db. 905 intros; autorewrite with core.
902 (** [[ 906 (** [[
903 907
904 ============================ 908 ============================
905 g (g (g x)) = g x 909 g (g (g x)) = g x
906 910
924 Section garden_path. 928 Section garden_path.
925 Variable P : A -> Prop. 929 Variable P : A -> Prop.
926 Variable g : A -> A. 930 Variable g : A -> A.
927 Hypothesis f_g : forall x, P x -> f x = g x. 931 Hypothesis f_g : forall x, P x -> f x = g x.
928 (* begin thide *) 932 (* begin thide *)
929 Hint Rewrite f_g using assumption : my_db. 933 Hint Rewrite f_g using assumption.
930 (* end thide *) 934 (* end thide *)
931 935
932 Lemma f_f_f' : forall x, f (f (f x)) = f x. 936 Lemma f_f_f' : forall x, f (f (f x)) = f x.
933 (* begin thide *) 937 (* begin thide *)
934 intros; autorewrite with my_db; reflexivity. 938 intros; autorewrite with core; reflexivity.
935 Qed. 939 Qed.
936 (* end thide *) 940 (* end thide *)
937 941
938 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *) 942 (** We may still use [autorewrite] to apply [f_g] when the generated premise is among our assumptions. *)
939 943
940 Lemma f_f_f_g : forall x, P x -> f (f x) = g x. 944 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
941 (* begin thide *) 945 (* begin thide *)
942 intros; autorewrite with my_db; reflexivity. 946 intros; autorewrite with core; reflexivity.
943 (* end thide *) 947 (* end thide *)
944 Qed. 948 Qed.
945 End garden_path. 949 End garden_path.
946 950
947 (** remove printing * *) 951 (** remove printing * *)
948 952
949 (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *) 953 (** It can also be useful to apply the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
950 954
951 (** printing * $*$ *) 955 (** printing * $*$ *)
952 956
953 Lemma in_star : forall x y, f (f (f (f x))) = f (f y) 957 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
954 -> f x = f (f (f y)). 958 -> f x = f (f (f y)).
955 (* begin thide *) 959 (* begin thide *)
956 intros; autorewrite with my_db in *; assumption. 960 intros; autorewrite with core in *; assumption.
957 (* end thide *) 961 (* end thide *)
958 Qed. 962 Qed.
959 963
960 End autorewrite. 964 End autorewrite.
965
966 (** Many proofs can be automated in pleasantly modular ways with deft combination of [auto] and [autorewrite]. *)