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成功，但它不会。

在他的书中认证的程序与相关类型，亚当Chlipala discusses模式匹配的上依赖类型的限制：

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

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

Answer 1

由于larsr解释，该模式?P x只能匹配一个术语，是语法上的应用程序，这并不包括你正在考虑的情况下。但是，Ltac确实为您正在寻找的比赛提供了功能。作为user manual说：

还为二阶模式匹配问题一个特殊的符号：在形式@?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.