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のように述べている：

は、2次パターンマッチング問題の特別な表記法がある：フォーム@?id id1 …idnの応用的なパターンで、変数IDが変数内（可能）依存性を有する任意の複雑な式に一致id1 …idnを返し、fun id1 …idn => termという形式の機能用語を返します。 (fun x : Prop => x)を印刷し

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

：

したがって、我々は次の証明のスクリプトを書くことができます。

Answer 2

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.