包含本地绑定变量的Ltac统一变量

Question

CPDT的Ltac章节显示了一种“错误的”策略：

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

这本书然后解释

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.

但是，以上策略实际上在Coq 8.11中有效！

统一变量现在可以包含局部变量吗？如果是这样，则上述内容与

有什么区别吗？

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

（（我们将?P替换为_）？

Answer 1

?P和_之间的区别在于，您实际上可以在分支中引用P。不幸的是，P是一个开放术语，因此它可能很快就会变得格式错误，因此您无法做很多事情。因此，我不会依赖它。最好使用forall x, @?P x作为模式，以便P是一个封闭项。