Mercurial > cpdt > repo
comparison src/LogicProg.v @ 398:05efde66559d
Get it working in Coq 8.4beta1; use nice coqdoc notation for italics
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 06 Jun 2012 11:25:13 -0400 |
parents | 3c941750c347 |
children | b4c37245502e |
comparison
equal
deleted
inserted
replaced
397:d62ed7381a0b | 398:05efde66559d |
---|---|
153 ]] | 153 ]] |
154 *) | 154 *) |
155 Qed. | 155 Qed. |
156 (* end thide *) | 156 (* end thide *) |
157 | 157 |
158 (** The two key components of logic programming are %\index{backtracking}\emph{%#<i>#backtracking#</i>#%}% and %\index{unification}\emph{%#<i>#unification#</i>#%}%. To see these techniques in action, consider this further silly example. Here our candidate proof steps will be reflexivity and quantifier instantiation. *) | 158 (** The two key components of logic programming are %\index{backtracking}%_backtracking_ and %\index{unification}%_unification_. To see these techniques in action, consider this further silly example. Here our candidate proof steps will be reflexivity and quantifier instantiation. *) |
159 | 159 |
160 Example seven_minus_three : exists x, x + 3 = 7. | 160 Example seven_minus_three : exists x, x + 3 = 7. |
161 (* begin thide *) | 161 (* begin thide *) |
162 (** For explanatory purposes, let us simulate a user with minimal understanding of arithmetic. We start by choosing an instantiation for the quantifier. Recall that [ex_intro] is the constructor for existentially quantified formulas. *) | 162 (** For explanatory purposes, let us simulate a user with minimal understanding of arithmetic. We start by choosing an instantiation for the quantifier. Recall that [ex_intro] is the constructor for existentially quantified formulas. *) |
163 | 163 |
168 %\vspace{-.2in}% | 168 %\vspace{-.2in}% |
169 << | 169 << |
170 Error: Impossible to unify "7" with "0 + 3". | 170 Error: Impossible to unify "7" with "0 + 3". |
171 >> | 171 >> |
172 | 172 |
173 This seems to be a dead end. Let us %\emph{%#<i>#backtrack#</i>#%}% to the point where we ran [apply] and make a better alternate choice. | 173 This seems to be a dead end. Let us _backtrack_ to the point where we ran [apply] and make a better alternate choice. |
174 *) | 174 *) |
175 | 175 |
176 Restart. | 176 Restart. |
177 apply ex_intro with 4. | 177 apply ex_intro with 4. |
178 reflexivity. | 178 reflexivity. |
183 | 183 |
184 Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition. *) | 184 Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition. *) |
185 | 185 |
186 Example seven_minus_three' : exists x, plusR x 3 7. | 186 Example seven_minus_three' : exists x, plusR x 3 7. |
187 (* begin thide *) | 187 (* begin thide *) |
188 (** We could attempt to guess the quantifier instantiation manually as before, but here there is no need. Instead of [apply], we use %\index{tactics!eapply}%[eapply] instead, which proceeds with placeholder %\index{unification variable}\emph{%#<i>#unification variables#</i>#%}% standing in for those parameters we wish to postpone guessing. *) | 188 (** We could attempt to guess the quantifier instantiation manually as before, but here there is no need. Instead of [apply], we use %\index{tactics!eapply}%[eapply] instead, which proceeds with placeholder %\index{unification variable}%_unification variables_ standing in for those parameters we wish to postpone guessing. *) |
189 | 189 |
190 eapply ex_intro. | 190 eapply ex_intro. |
191 (** [[ | 191 (** [[ |
192 1 subgoal | 192 1 subgoal |
193 | 193 |
378 ]] | 378 ]] |
379 *) | 379 *) |
380 Abort. | 380 Abort. |
381 End slow. | 381 End slow. |
382 | 382 |
383 (** Sometimes, though, transitivity is just what is needed to get a proof to go through automatically with [eauto]. For those cases, we can use named %\index{hint databases}\emph{%#<i>#hint databases#</i>#%}% to segragate hints into different groups that may be called on as needed. Here we put [eq_trans] into the database [slow]. *) | 383 (** Sometimes, though, transitivity is just what is needed to get a proof to go through automatically with [eauto]. For those cases, we can use named %\index{hint databases}%_hint databases_ to segragate hints into different groups that may be called on as needed. Here we put [eq_trans] into the database [slow]. *) |
384 | 384 |
385 (* begin thide *) | 385 (* begin thide *) |
386 Hint Resolve eq_trans : slow. | 386 Hint Resolve eq_trans : slow. |
387 (* end thide *) | 387 (* end thide *) |
388 | 388 |
411 %\vspace{-.2in}% *) | 411 %\vspace{-.2in}% *) |
412 | 412 |
413 Qed. | 413 Qed. |
414 (* end thide *) | 414 (* end thide *) |
415 | 415 |
416 (** When we %\emph{%#<i>#do#</i>#%}% need transitivity, we ask for it explicitly. *) | 416 (** When we _do_ need transitivity, we ask for it explicitly. *) |
417 | 417 |
418 Example needs_trans : forall x y, 1 + x = y | 418 Example needs_trans : forall x y, 1 + x = y |
419 -> y = 2 | 419 -> y = 2 |
420 -> exists z, z + x = 3. | 420 -> exists z, z + x = 3. |
421 (* begin thide *) | 421 (* begin thide *) |
485 No more subgoals but non-instantiated existential variables: | 485 No more subgoals but non-instantiated existential variables: |
486 Existential 1 = ?20249 : [ |- nat] | 486 Existential 1 = ?20249 : [ |- nat] |
487 Existential 2 = ?20252 : [ |- nat] | 487 Existential 2 = ?20252 : [ |- nat] |
488 >> | 488 >> |
489 | 489 |
490 Coq complains that we finished the proof without determining the values of some unification variables created during proof search. The error message may seem a bit silly, since %\emph{%#<i>#any#</i>#%}% value of type [nat] (for instance, 0) can be plugged in for either variable! However, for more complex types, finding their inhabitants may be as complex as theorem-proving in general. | 490 Coq complains that we finished the proof without determining the values of some unification variables created during proof search. The error message may seem a bit silly, since _any_ value of type [nat] (for instance, 0) can be plugged in for either variable! However, for more complex types, finding their inhabitants may be as complex as theorem-proving in general. |
491 | 491 |
492 The %\index{Vernacular commands!Show Proof}%[Show Proof] command shows exactly which proof term [eauto] has found, with the undetermined unification variables appearing explicitly where they are used. *) | 492 The %\index{Vernacular commands!Show Proof}%[Show Proof] command shows exactly which proof term [eauto] has found, with the undetermined unification variables appearing explicitly where they are used. *) |
493 | 493 |
494 Show Proof. | 494 Show Proof. |
495 (** << | 495 (** << |
593 | 593 |
594 (* begin hide *) | 594 (* begin hide *) |
595 Print length_and_sum''. | 595 Print length_and_sum''. |
596 (* end hide *) | 596 (* end hide *) |
597 | 597 |
598 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding %\emph{%#<i>#programs#</i>#%}% automatically. *) | 598 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding _programs_ automatically. *) |
599 | 599 |
600 | 600 |
601 (** * Synthesizing Programs *) | 601 (** * Synthesizing Programs *) |
602 | 602 |
603 (** Here is a simple syntax type for arithmetic expressions, similar to those we have used several times before in the book. In this case, we allow expressions to mention exactly one distinguished variable. *) | 603 (** Here is a simple syntax type for arithmetic expressions, similar to those we have used several times before in the book. In this case, we allow expressions to mention exactly one distinguished variable. *) |
751 crush. | 751 crush. |
752 Qed. | 752 Qed. |
753 | 753 |
754 Hint Resolve plus_0 times_1. | 754 Hint Resolve plus_0 times_1. |
755 | 755 |
756 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the %\emph{%#<i>#ring#</i>#%}% algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) | 756 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) |
757 | 757 |
758 Require Import Arith Ring. | 758 Require Import Arith Ring. |
759 | 759 |
760 Theorem combine : forall x k1 k2 n1 n2, | 760 Theorem combine : forall x k1 k2 n1 n2, |
761 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2). | 761 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2). |
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 (** 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]. | 784 (** Let us stop at this point and take stock of the possibilities for [auto] and [eauto] hints. Hints are contained within _hint databases_, 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 %\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. | 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 more examples of [Hint Extern] should illustrate more of the possibilities. *) | 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 |
840 ]] | 840 ]] |
841 << | 841 << |
842 User error: Bound head variable | 842 User error: Bound head variable |
843 >> | 843 >> |
844 | 844 |
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]. | 845 Coq's [auto] hint databases work as tables mapping %\index{head symbol}%_head symbols_ 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 | 846 |
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. *) | 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. *) |
848 | 848 |
849 Hint Extern 1 => | 849 Hint Extern 1 => |
850 match goal with | 850 match goal with |
851 | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X)) | 851 | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X)) |
852 end. | 852 end. |
853 | 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. *) | 854 (** Be forewarned that a [Hint Extern] of this kind will be applied at _every_ node of a proof tree, so an expensive Ltac script may slow proof search significantly. *) |
855 | 855 |
856 | 856 |
857 (** * Rewrite Hints *) | 857 (** * Rewrite Hints *) |
858 | 858 |
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]. | 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]. |