Mercurial > cpdt > repo

comparison src/Match.v @ 136:d6b1e9de7fc1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
135:091583baf345 136:d6b1e9de7fc1
410 completer'. 410 completer'.
411 411
412 Coq loops forever at this point. What went wrong? *) 412 Coq loops forever at this point. What went wrong? *)
413 Abort. 413 Abort.
414 End firstorder'. 414 End firstorder'.
415
416 (** A few examples should illustrate the issue. Here we see a [match]-based proof that works fine: *)
417
418 Theorem t1 : forall x : nat, x = x.
419 match goal with
420 | [ |- forall x, _ ] => trivial
421 end.
422 Qed.
423
424 (** This one fails. *)
425
426 Theorem t1' : forall x : nat, x = x.
427 (** [[
428
429 match goal with
430 | [ |- forall x, ?P ] => trivial
431 end.
432
433 [[
434 User error: No matching clauses for match goal
435 ]] *)
436 Abort.
437
438 (** 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.
439
440 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.
441
442 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. *)