Search code examples
coqcoq-tactic

Ltac unification variable containing locally-bound variables

The Ltac chapter of CPDT, shows a "faulty" tactic:

Theorem t1' : forall x : nat, x = x.
  match goal with
    | [ |- forall x, ?P ] => trivial
  end.

The book then explains

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.

However, the tactic above actually works in Coq 8.11!

Can unification variables now contain locally-bound variables? If so, is there any difference between the above and

Theorem t1' : forall x : nat, x = x.
  match goal with
    | [ |- forall x, _ ] => trivial
  end.

(where we replaced ?P by _)?

Solution

  • The difference between ?P and _ is that you can actually refer to P in the branch. Unfortunately, P is an open term, so it might quickly end up being ill-formed, so there is not much you can do with it. So, I would not rely on it. It is better to use forall x, @?P x as a pattern, so that P is a closed term.