Mercurial > cpdt > repo

comparison src/Match.v @ 134:f9d8f33c9b46

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
autorewrite
author Adam Chlipala <adamc@hcoop.net>
date Sun, 26 Oct 2008 11:13:43 -0400
parents 28ef7f0da085
children 091583baf345
comparison
equal deleted inserted replaced
133:28ef7f0da085 134:f9d8f33c9b46
83 Hint Extern 1 (?P ?X) => 83 Hint Extern 1 (?P ?X) =>
84 match goal with 84 match goal with
85 | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X)) 85 | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X))
86 end. 86 end.
87 87
88 [[ 88 [[
89 User error: Bound head variable 89 User error: Bound head variable
90 ]] 90 ]]
91 91
92 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]. 92 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].
93 93
94 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. *) 94 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.
95
96 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.
97
98 This example shows a direct use of [autorewrite]. *)
99
100 Section autorewrite.
101 Variable A : Set.
102 Variable f : A -> A.
103
104 Hypothesis f_f : forall x, f (f x) = f x.
105
106 Hint Rewrite f_f : my_db.
107
108 Lemma f_f_f : forall x, f (f (f x)) = f x.
109 intros; autorewrite with my_db; reflexivity.
110 Qed.
111
112 (** 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: *)
113
114 Section garden_path.
115 Variable g : A -> A.
116 Hypothesis f_g : forall x, f x = g x.
117 Hint Rewrite f_g : my_db.
118
119 Lemma f_f_f' : forall x, f (f (f x)) = f x.
120 intros; autorewrite with my_db.
121 (** [[
122
123 ============================
124 g (g (g x)) = g x
125 ]] *)
126 Abort.
127
128 (** 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. *)
129
130 Reset garden_path.
131
132 (** [autorewrite] works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
133
134 Section garden_path.
135 Variable P : A -> Prop.
136 Variable g : A -> A.
137 Hypothesis f_g : forall x, P x -> f x = g x.
138 Hint Rewrite f_g : my_db.
139
140 Lemma f_f_f' : forall x, f (f (f x)) = f x.
141 intros; autorewrite with my_db.
142 (** [[
143
144 ============================
145 g (g (g x)) = g x
146
147 subgoal 2 is:
148 P x
149 subgoal 3 is:
150 P (f x)
151 subgoal 4 is:
152 P (f x)
153 ]] *)
154 Abort.
155
156 (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
157
158 Reset garden_path.
159
160 (** Our final, successful, attempt uses an extra argument to [Hint Rewrite] that specifies a tactic to apply to generated premises. *)
161
162 Section garden_path.
163 Variable P : A -> Prop.
164 Variable g : A -> A.
165 Hypothesis f_g : forall x, P x -> f x = g x.
166 Hint Rewrite f_g using assumption : my_db.
167
168 Lemma f_f_f' : forall x, f (f (f x)) = f x.
169 intros; autorewrite with my_db; reflexivity.
170 Qed.
171
172 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
173
174 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
175 intros; autorewrite with my_db; reflexivity.
176 Qed.
177 End garden_path.
178
179 (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
180
181 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
182 -> f x = f (f (f y)).
183 intros; autorewrite with my_db in *; assumption.
184 Qed.
185
186 End autorewrite.