Ltac模式匹配:为什么‘`forall x，?P’不匹配` `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)。

Answer 2

H的类型是forall x, x，而不是forall x, P x。

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

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

Abort.

或者为了匹配你的checkForall

Example test {T} (f:T->Prop)  : (forall x, f x) -> True.
Proof.
  intros H.
  checkForall H.