coq - Ltac 模式匹配 : why does `forall x, ?P x` not match `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 discusses依赖类型的模式匹配限制:

The problem is that unification variables may not contain locally bound variables.

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

Answer 1

正如 larsr 所解释的，模式 ?P x 只能匹配在语法上是应用程序的术语，这不包括您正在考虑的情况。但是，Ltac 确实为您正在寻找的匹配提供了功能。作为user manual说:

There is also a special notation for second-order pattern-matching problems: in an applicative pattern of the form @?id id1 …idn, the variable id matches any complex expression with (possible) dependencies in the variables id1 …idn and returns a functional term of the form 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).