Mercurial > cpdt > repo
diff src/Match.v @ 136:d6b1e9de7fc1
Free variables in unification variables issue
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 26 Oct 2008 14:39:21 -0400 |
parents | 091583baf345 |
children | c0bda476b44b |
line wrap: on
line diff
--- a/src/Match.v Sun Oct 26 14:11:41 2008 -0400 +++ b/src/Match.v Sun Oct 26 14:39:21 2008 -0400 @@ -412,3 +412,31 @@ Coq loops forever at this point. What went wrong? *) Abort. End firstorder'. + +(** A few examples should illustrate the issue. Here we see a [match]-based proof that works fine: *) + +Theorem t1 : forall x : nat, x = x. + match goal with + | [ |- forall x, _ ] => trivial + end. +Qed. + +(** This one fails. *) + +Theorem t1' : forall x : nat, x = x. +(** [[ + + match goal with + | [ |- forall x, ?P ] => trivial + end. + + [[ +User error: No matching clauses for match goal + ]] *) +Abort. + +(** 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. + + 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. + + No matter which 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. *)