Ltac模式匹配:为什么`forall x,？P x`不匹配`forall x,x`？

Question

Ltac checkForall H :=
  let T := type of H in
  match T with
  | forall x, ?P x =>
    idtac
  | _ =>
    fail 1 "not a forall"
  end.

Example test : (forall x, x) -> True.
Proof.
  intros H.
  Fail checkForall H. (* not a forall *)
Abort.

我会天真地期望checkForall H成功,但事实并非如此.

在他的" 依赖类型认证编程"一书中,Adam Chlipala 讨论了依赖类型的模式匹配限制:

问题是统一变量可能不包含本地绑定变量.

这是我在这里看到的行为的原因吗？

Answer 1

正如larsr所解释的那样,模式?P x只能匹配语法上一个应用程序的术语,这不包括你正在考虑的情况.但是,Ltac确实为您正在寻找的匹配提供了功能.正如用户手册所说:

对于二阶模式匹配问题还有一个特殊的符号:在表单的应用模式中@?id id1 …idn,变量id匹配任何复杂表达式与变量中的(可能的)依赖关系,id1 …idn并返回表单的功能术语fun id1 …idn => term.

因此,我们可以编写以下证明脚本:

Goal (forall x : Prop, x) -> False.
intros H.
match goal with
| H : forall x : Prop, @?P x |- _ => idtac P
end.

打印(fun x : Prop => x).