## Mercurial > cpdt > repo

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

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Update Match to take into account a number of misunderstandings of tactic execution in 8.4 and 8.4pl1

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Sun, 06 Jan 2013 15:19:01 -0500 |

parents | 1fd4109f7b31 |

children | 5025a401ad9e |

comparison

equal
deleted
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. *) |