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

Question

CPDT 的 Ltac 章节显示了 "faulty" 策略：

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 是一个封闭的术语。

Answer 2

本书稍后会提供更多信息：

Actually, the behavior demonstrated here applies to Coq version 8.4,
but not 8.4pl1.  The latter version will allow regular Ltac pattern
variables to match terms that contain locally bound variables, but a
tactic failure occurs if that variable is later used as a Gallina term.

这意味着在

Ltac dummy :=
  match goal with
  | [ H: forall x, ?P |- _ ] => assert True
  end.

Lemma foo (a x : nat) :
  (forall n, n = 42) ->  
  True.
Proof.
  intros.
  dummy.

可以应用dummy策略（因为我们匹配了?P但是后面没有引用它），但是如果我们把dummy改成

Ltac dummy :=
  match goal with
  | [ H: forall x, ?P |- _ ] => assert ?P
  end.

那会失败，因为我们指的是 ?P，这可能是一个开放式术语。

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

Ltac unification variable containing locally-bound variables

coq

coq-tactic