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

【问题标题】：Ltac unification variable containing locally-bound variables包含本地绑定变量的 Ltac 统一变量
【发布时间】：2020-05-14 10:27:39
【问题描述】：

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 替换为_）？

【问题讨论】：

标签： coq coq-tactic

【解决方案1】：

?P 和_ 的区别在于你实际上可以在分支中引用P。不幸的是，P 是一个开放的术语，所以它可能很快就会变得不正确，所以你无能为力。所以，我不会依赖它。最好使用forall x, @?P x 作为模式，这样P 是一个封闭的术语。

【讨论】：

【解决方案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，这可能是一个开放的术语。

【讨论】：