coq - 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成功，但事实并非如此。

在他的书Certified Programming with Dependent Types中，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.