## Mercurial > cpdt > repo

### comparison src/Match.v @ 507:49f3b2d70302

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

Pass through Chapter 14

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

date | Sun, 10 Feb 2013 18:59:59 -0500 |

parents | 31258618ef73 |

children | ed829eaa91b2 |

comparison

equal
deleted
inserted
replaced

506:05c0f872a129 | 507:49f3b2d70302 |
---|---|

313 *) | 313 *) |

314 | 314 |

315 Abort. | 315 Abort. |

316 (* end thide *) | 316 (* end thide *) |

317 | 317 |

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. | 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 restriction affects the behavior of the [completer] tactic, 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. |

319 | 319 |

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 Section 15.5. | 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 Section 15.5. |

321 | 321 |

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. | 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 | 323 |

530 | [ H : forall x : ?T, _, y : ?T |- _ ] => generalize (H y); inster n' | 530 | [ H : forall x : ?T, _, y : ?T |- _ ] => generalize (H y); inster n' |

531 end | 531 end |

532 end. | 532 end. |

533 (* end thide *) | 533 (* end thide *) |

534 | 534 |

535 (** The tactic begins by applying propositional simplification. Next, it checks if any chain length remains, failing if not. If so, it tries all possible ways of instantiating quantified hypotheses with properly typed local variables. It is critical to realize that, if the recursive call [inster n'] fails, then the [match goal] just seeks out another way of unifying its pattern against proof state. Thus, this small amount of code provides an elegant demonstration of how backtracking [match] enables exhaustive search. | 535 (** The tactic begins by applying propositional simplification. Next, it checks if any chain length remains, failing if not. Otherwise, it tries all possible ways of instantiating quantified hypotheses with properly typed local variables. It is critical to realize that, if the recursive call [inster n'] fails, then the [match goal] just seeks out another way of unifying its pattern against proof state. Thus, this small amount of code provides an elegant demonstration of how backtracking [match] enables exhaustive search. |

536 | 536 |

537 We can verify the efficacy of [inster] with two short examples. The built-in [firstorder] tactic (with no extra arguments) is able to prove the first but not the second. *) | 537 We can verify the efficacy of [inster] with two short examples. The built-in [firstorder] tactic (with no extra arguments) is able to prove the first but not the second. *) |

538 | 538 |

539 Section test_inster. | 539 Section test_inster. |

540 Variable A : Set. | 540 Variable A : Set. |

635 | [ |- _ --> _ ] => progress (tac || (apply and_True_prem; tac)) | 635 | [ |- _ --> _ ] => progress (tac || (apply and_True_prem; tac)) |

636 end. | 636 end. |

637 | 637 |

638 (** To understand how [search_prem] works, we turn first to the final [match]. If the premise begins with a conjunction, we call the [search] procedure on each of the conjuncts, or only the first conjunct, if that already yields a case where [tac] does not fail. The call [search P] expects and maintains the invariant that the premise is of the form [P /\ Q] for some [Q]. We pass [P] explicitly as a kind of decreasing induction measure, to avoid looping forever when [tac] always fails. The second [match] case calls a commutativity lemma to realize this invariant, before passing control to [search]. The final [match] case tries applying [tac] directly and then, if that fails, changes the form of the goal by adding an extraneous [True] conjunct and calls [tac] again. The %\index{tactics!progress}%[progress] tactical fails when its argument tactic succeeds without changing the current subgoal. | 638 (** To understand how [search_prem] works, we turn first to the final [match]. If the premise begins with a conjunction, we call the [search] procedure on each of the conjuncts, or only the first conjunct, if that already yields a case where [tac] does not fail. The call [search P] expects and maintains the invariant that the premise is of the form [P /\ Q] for some [Q]. We pass [P] explicitly as a kind of decreasing induction measure, to avoid looping forever when [tac] always fails. The second [match] case calls a commutativity lemma to realize this invariant, before passing control to [search]. The final [match] case tries applying [tac] directly and then, if that fails, changes the form of the goal by adding an extraneous [True] conjunct and calls [tac] again. The %\index{tactics!progress}%[progress] tactical fails when its argument tactic succeeds without changing the current subgoal. |

639 | 639 |

640 The [search] function itself tries the same tricks as in the last case of the final [match], using the [||] operator as a shorthand for trying one tactic and then, if the first fails, trying another. Additionally, if neither works, it checks if [P] is a conjunction. If so, it calls itself recursively on each conjunct, first applying associativity lemmas to maintain the goal-form invariant. | 640 The [search] function itself tries the same tricks as in the last case of the final [match], using the [||] operator as a shorthand for trying one tactic and then, if the first fails, trying another. Additionally, if neither works, it checks if [P] is a conjunction. If so, it calls itself recursively on each conjunct, first applying associativity/commutativity lemmas to maintain the goal-form invariant. |

641 | 641 |

642 We will also want a dual function [search_conc], which does tree search through an [imp] conclusion. *) | 642 We will also want a dual function [search_conc], which does tree search through an [imp] conclusion. *) |

643 | 643 |

644 Ltac search_conc tac := | 644 Ltac search_conc tac := |

645 let rec search P := | 645 let rec search P := |