### comparison src/Match.v @ 483:582cf453878e

Update Match to take into account a number of misunderstandings of tactic execution in 8.4 and 8.4pl1
comparison
equal inserted replaced
482:e3b32a87347f 483:582cf453878e
212 212
213 (** We use the same kind of conjunction and implication handling as previously. Note that, since [->] is the special non-dependent case of [forall], the fourth rule handles [intro] for implications, too. 213 (** We use the same kind of conjunction and implication handling as previously. Note that, since [->] is the special non-dependent case of [forall], the fourth rule handles [intro] for implications, too.
214 214
215 In the fifth rule, when we find a [forall] fact [H] with a premise matching one of our hypotheses, we add the appropriate instantiation of [H]'s conclusion, if we have not already added it. 215 In the fifth rule, when we find a [forall] fact [H] with a premise matching one of our hypotheses, we add the appropriate instantiation of [H]'s conclusion, if we have not already added it.
216 216
217 We can check that [completer] is working properly: *) 217 We can check that [completer] is working properly, with a theorem that introduces a spurious variable whose didactic purpose we will come to shortly. *)
218 218
219 Section firstorder. 219 Section firstorder.
220 Variable A : Set. 220 Variable A : Set.
221 Variables P Q R S : A -> Prop. 221 Variables P Q R S : A -> Prop.
222 222
223 Hypothesis H1 : forall x, P x -> Q x /\ R x. 223 Hypothesis H1 : forall x, P x -> Q x /\ R x.
224 Hypothesis H2 : forall x, R x -> S x. 224 Hypothesis H2 : forall x, R x -> S x.
225 225
226 Theorem fo : forall x, P x -> S x. 226 Theorem fo : forall (y x : A), P x -> S x.
227 (* begin thide *) 227 (* begin thide *)
228 completer. 228 completer.
229 (** [[ 229 (** [[
230 y : A
230 x : A 231 x : A
231 H : P x 232 H : P x
232 H0 : Q x 233 H0 : Q x
233 H3 : R x 234 H3 : R x
234 H4 : S x 235 H4 : S x
240 assumption. 241 assumption.
241 Qed. 242 Qed.
242 (* end thide *) 243 (* end thide *)
243 End firstorder. 244 End firstorder.
244 245
245 (** We narrowly avoided a subtle pitfall in our definition of [completer]. Let us try another definition that even seems preferable to the original, to the untrained eye. *) 246 (** We narrowly avoided a subtle pitfall in our definition of [completer]. Let us try another definition that even seems preferable to the original, to the untrained eye. (We change the second [match] case a bit to make the tactic smart enough to handle some subtleties of Ltac behavior that had not been exercised previously.) *)
246 247
247 (* begin thide *) 248 (* begin thide *)
248 Ltac completer' := 249 Ltac completer' :=
249 repeat match goal with 250 repeat match goal with
250 | [ |- _ /\ _ ] => constructor 251 | [ |- _ /\ _ ] => constructor
251 | [ H : _ /\ _ |- _ ] => destruct H 252 | [ H : ?P /\ ?Q |- _ ] => destruct H;
253 repeat match goal with
254 | [ H' : P /\ Q |- _ ] => clear H'
255 end
252 | [ H : ?P -> _, H' : ?P |- _ ] => specialize (H H') 256 | [ H : ?P -> _, H' : ?P |- _ ] => specialize (H H')
253 | [ |- forall x, _ ] => intro 257 | [ |- forall x, _ ] => intro
254 258
255 | [ H : forall x, ?P x -> _, H' : ?P ?X |- _ ] => extend (H X H') 259 | [ H : forall x, ?P x -> _, H' : ?P ?X |- _ ] => extend (H X H')
256 end. 260 end.
257 (* end thide *) 261 (* end thide *)
258 262
259 (** The only difference is in the modus ponens rule, where we have replaced an unused unification variable [?Q] with a wildcard. Let us try our example again with this version: *) 263 (** The only other difference is in the modus ponens rule, where we have replaced an unused unification variable [?Q] with a wildcard. Let us try our example again with this version: *)
260 264
261 Section firstorder'. 265 Section firstorder'.
262 Variable A : Set. 266 Variable A : Set.
263 Variables P Q R S : A -> Prop. 267 Variables P Q R S : A -> Prop.
264 268
265 Hypothesis H1 : forall x, P x -> Q x /\ R x. 269 Hypothesis H1 : forall x, P x -> Q x /\ R x.
266 Hypothesis H2 : forall x, R x -> S x. 270 Hypothesis H2 : forall x, R x -> S x.
267 271
268 Theorem fo' : forall x, P x -> S x. 272 Theorem fo' : forall (y x : A), P x -> S x.
269 (* begin thide *)
270 (** %\vspace{-.25in}%[[
271 completer'. 273 completer'.
272 ]] 274 (** [[
273 %\vspace{-.15in}%Coq loops forever at this point. What went wrong? *) 275 y : A
276 H1 : P y -> Q y /\ R y
277 H2 : R y -> S y
278 x : A
279 H : P x
280 ============================
281 S x
282 ]]
283 The quantified theorems have been instantiated with [y] instead of [x], reducing a provable goal to one that is unprovable. Our code in the last [match] case for [completer'] is careful only to instantiate quantifiers along with suitable hypotheses, so why were incorrect choices made?
284 *)
274 285
275 Abort. 286 Abort.
276 (* end thide *) 287 (* end thide *)
277 End firstorder'. 288 End firstorder'.
278 289
306 317
307 (** The problem is that unification variables may not contain locally bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. To understand why this applies to the [completer] tactics, recall that, in Coq, implication is shorthand for degenerate universal quantification where the quantified variable is not used. Nonetheless, in an Ltac pattern, Coq is happy to match a wildcard implication against a universal quantification. 318 (** The problem is that unification variables may not contain locally bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. To understand why this applies to the [completer] tactics, recall that, in Coq, implication is shorthand for degenerate universal quantification where the quantified variable is not used. Nonetheless, in an Ltac pattern, Coq is happy to match a wildcard implication against a universal quantification.
308 319
309 The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables. That unification variable is then bound to a function from the free variables to the "real" value. In Coq 8.1 and earlier, there is no such workaround. We will see an example of this fancier binding form in the next chapter. 320 The Coq 8.2 release includes a special pattern form for a unification variable with an explicit set of free variables. That unification variable is then bound to a function from the free variables to the "real" value. In Coq 8.1 and earlier, there is no such workaround. We will see an example of this fancier binding form in the next chapter.
310 321
311 No matter which Coq version you use, it is important to be aware of this restriction. As we have alluded to, the restriction is the culprit behind the infinite-looping behavior of [completer']. We unintentionally match quantified facts with the modus ponens rule, circumventing the "already present" check and leading to different behavior, where the same fact may be added to the context repeatedly in an infinite loop. Our earlier [completer] tactic uses a modus ponens rule that matches the implication conclusion with a variable, which blocks matching against non-trivial universal quantifiers. *) 322 No matter which Coq version you use, it is important to be aware of this restriction. As we have alluded to, the restriction is the culprit behind the surprising behavior of [completer']. We unintentionally match quantified facts with the modus ponens rule, circumventing the check that a suitably matching hypothesis is available and leading to different behavior, where wrong quantifier instantiations are chosen. Our earlier [completer] tactic uses a modus ponens rule that matches the implication conclusion with a variable, which blocks matching against non-trivial universal quantifiers.
323
324 Actually, the behavior demonstrated here applies to Coq version 8.4, but not 8.4pl1. The latter version will allow regular Ltac pattern variables to match terms that contain locally bound variables, but a tactic failure occurs if that variable is later used as a Gallina term. *)
312 325
313 326
314 (** * Functional Programming in Ltac *) 327 (** * Functional Programming in Ltac *)
315 328
316 (* EX: Write a list length function in Ltac. *) 329 (* EX: Write a list length function in Ltac. *)