Mercurial > cpdt > repo

comparison src/Match.v @ 324:06d11a6363cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New LogicProg chapter
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Sep 2011 14:07:21 -0400
parents d5787b70cf48
children cbeccef45f4e
comparison
equal deleted inserted replaced
323:3513d8b0531a 324:06d11a6363cd
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\part{Proof Engineering} 19 (** %\chapter{Proof Search in Ltac}% *)
20
21 \chapter{Proof Search in Ltac}% *)
22 20
23 (** We have seen many examples of proof automation so far. This chapter aims to give a principled presentation of the features of Ltac, focusing in particular on the Ltac [match] construct, which supports a novel approach to backtracking search. First, though, we will run through some useful automation tactics that are built into Coq. They are described in detail in the manual, so we only outline what is possible. *) 21 (** We have seen many examples of proof automation so far. This chapter aims to give a principled presentation of the features of Ltac, focusing in particular on the Ltac [match] construct, which supports a novel approach to backtracking search. First, though, we will run through some useful automation tactics that are built into Coq. They are described in detail in the manual, so we only outline what is possible. *)
24 22
25 (** * Some Built-In Automation Tactics *) 23 (** * Some Built-In Automation Tactics *)
26 24
27 (** A number of tactics are called repeatedly by [crush]. [intuition] simplifies propositional structure of goals. [congruence] applies the rules of equality and congruence closure, plus properties of constructors of inductive types. The [omega] tactic provides a complete decision procedure for a theory that is called quantifier-free linear arithmetic or Presburger arithmetic, depending on whom you ask. That is, [omega] proves any goal that follows from looking only at parts of that goal that can be interpreted as propositional formulas whose atomic formulas are basic comparison operations on natural numbers or integers. 25 (** A number of tactics are called repeatedly by [crush]. [intuition] simplifies propositional structure of goals. [congruence] applies the rules of equality and congruence closure, plus properties of constructors of inductive types. The [omega] tactic provides a complete decision procedure for a theory that is called quantifier-free linear arithmetic or Presburger arithmetic, depending on whom you ask. That is, [omega] proves any goal that follows from looking only at parts of that goal that can be interpreted as propositional formulas whose atomic formulas are basic comparison operations on natural numbers or integers.
28 26
29 The [ring] tactic solves goals by appealing to the axioms of rings or semi-rings (as in algebra), depending on the type involved. Coq developments may declare new types to be parts of rings and semi-rings by proving the associated axioms. There is a simlar tactic [field] for simplifying values in fields by conversion to fractions over rings. Both [ring] and [field] can only solve goals that are equalities. The [fourier] tactic uses Fourier's method to prove inequalities over real numbers, which are axiomatized in the Coq standard library. 27 The [ring] tactic solves goals by appealing to the axioms of rings or semi-rings (as in algebra), depending on the type involved. Coq developments may declare new types to be parts of rings and semi-rings by proving the associated axioms. There is a simlar tactic [field] for simplifying values in fields by conversion to fractions over rings. Both [ring] and [field] can only solve goals that are equalities. The [fourier] tactic uses Fourier's method to prove inequalities over real numbers, which are axiomatized in the Coq standard library.
30 28
31 The %\textit{%#<i>#setoid#</i>#%}% facility makes it possible to register new equivalence relations to be understood by tactics like [rewrite]. For instance, [Prop] is registered as a setoid with the equivalence relation %``%#"#if and only if.#"#%''% The ability to register new setoids can be very useful in proofs of a kind common in math, where all reasoning is done after %``%#"#modding out by a relation.#"#%''% *) 29 The %\textit{%#<i>#setoid#</i>#%}% facility makes it possible to register new equivalence relations to be understood by tactics like [rewrite]. For instance, [Prop] is registered as a setoid with the equivalence relation %``%#"#if and only if.#"#%''% The ability to register new setoids can be very useful in proofs of a kind common in math, where all reasoning is done after %``%#"#modding out by a relation.#"#%''% *)
32
33
34 (** * Hint Databases *)
35
36 (** 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.
37
38 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; [Constructor 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.
39
40 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. *)
41
42 Theorem bool_neq : true <> false.
43 (* begin thide *)
44 auto.
45
46 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
47
48 Abort.
49
50 (** 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. *)
51
52 Hint Extern 1 (_ <> _) => congruence.
53
54 Theorem bool_neq : true <> false.
55 auto.
56 Qed.
57 (* end thide *)
58
59 (** 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.
60
61 [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
62
63 Section forall_and.
64 Variable A : Set.
65 Variables P Q : A -> Prop.
66
67 Hypothesis both : forall x, P x /\ Q x.
68
69 Theorem forall_and : forall z, P z.
70 (* begin thide *)
71 crush.
72
73 (** [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. *)
74
75 Hint Extern 1 (P ?X) =>
76 match goal with
77 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
78 end.
79
80 auto.
81 Qed.
82 (* end thide *)
83
84 (** 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]. *)
85
86 End forall_and.
87
88 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
89
90 [[
91 Hint Extern 1 (?P ?X) =>
92 match goal with
93 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
94 end.
95
96 User error: Bound head variable
97
98 ]]
99
100 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].
101
102 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 later sections of the chapter.
103
104 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.
105
106 This example shows a direct use of [autorewrite]. *)
107
108 Section autorewrite.
109 Variable A : Set.
110 Variable f : A -> A.
111
112 Hypothesis f_f : forall x, f (f x) = f x.
113
114 Hint Rewrite f_f : my_db.
115
116 Lemma f_f_f : forall x, f (f (f x)) = f x.
117 intros; autorewrite with my_db; reflexivity.
118 Qed.
119
120 (** 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: *)
121
122 Section garden_path.
123 Variable g : A -> A.
124 Hypothesis f_g : forall x, f x = g x.
125 Hint Rewrite f_g : my_db.
126
127 Lemma f_f_f' : forall x, f (f (f x)) = f x.
128 intros; autorewrite with my_db.
129 (** [[
130 ============================
131 g (g (g x)) = g x
132 ]]
133 *)
134
135 Abort.
136
137 (** 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. *)
138
139 Reset garden_path.
140
141 (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
142
143 Section garden_path.
144 Variable P : A -> Prop.
145 Variable g : A -> A.
146 Hypothesis f_g : forall x, P x -> f x = g x.
147 Hint Rewrite f_g : my_db.
148
149 Lemma f_f_f' : forall x, f (f (f x)) = f x.
150 intros; autorewrite with my_db.
151 (** [[
152
153 ============================
154 g (g (g x)) = g x
155
156 subgoal 2 is:
157 P x
158 subgoal 3 is:
159 P (f x)
160 subgoal 4 is:
161 P (f x)
162 ]]
163 *)
164
165 Abort.
166
167 (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
168
169 Reset garden_path.
170
171 (** Our final, successful, attempt uses an extra argument to [Hint Rewrite] that specifies a tactic to apply to generated premises. Such a hint is only used when the tactic succeeds for all premises, possibly leaving further subgoals for some premises. *)
172
173 Section garden_path.
174 Variable P : A -> Prop.
175 Variable g : A -> A.
176 Hypothesis f_g : forall x, P x -> f x = g x.
177 (* begin thide *)
178 Hint Rewrite f_g using assumption : my_db.
179 (* end thide *)
180
181 Lemma f_f_f' : forall x, f (f (f x)) = f x.
182 (* begin thide *)
183 intros; autorewrite with my_db; reflexivity.
184 Qed.
185 (* end thide *)
186
187 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
188
189 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
190 (* begin thide *)
191 intros; autorewrite with my_db; reflexivity.
192 (* end thide *)
193 Qed.
194 End garden_path.
195
196 (** remove printing * *)
197
198 (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
199
200 (** printing * $*$ *)
201
202 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
203 -> f x = f (f (f y)).
204 (* begin thide *)
205 intros; autorewrite with my_db in *; assumption.
206 (* end thide *)
207 Qed.
208
209 End autorewrite.
210 30
211 31
212 (** * Ltac Programming Basics *) 32 (** * Ltac Programming Basics *)
213 33
214 (** We have already seen many examples of Ltac programs. In the rest of this chapter, we attempt to give a more principled introduction to the important features and design patterns. 34 (** We have already seen many examples of Ltac programs. In the rest of this chapter, we attempt to give a more principled introduction to the important features and design patterns.