3 
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は、彼の著書Certified Programming with Dependent Typesで、依存型に対するパターン マッチングの制限について説明しています。

問題は、統合変数にローカルにバインドされた変数が含まれていない可能性があることです。

これが私がここで見ている動作の理由ですか?

4

2 に答える 2

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.
于 2017-06-05T05:15:32.090 に答える