coq - Coqで暗黙のうちにdestructを使用できますか?

Question

destructはCoq でand、orを分割するために使用できます。しかし、それは暗示的にも使用できるようですか？たとえば、私は証明したい~~(~~P -> P)

Lemma test P : ~~(~~P -> P).
Proof.
unfold not.
intro pffpf.
apply pffpf.
intro pff.
destruct pff.
intro p.
apply pffpf.
intro pff.
exact p.
Qed.

正常にdestruct pff.動作するのですが、理由がわかりません。誰かが私のためにそれを説明できますか?

Answer 1

destruct含意の結論が帰納的 (または共帰納的) 型である場合、この戦術は含意に対して機能します。したがって、False帰納的に定義されているため、例で機能します。ただし、 の別の定義を思いついた場合、False必ずしもうまくいくとは限りません。たとえば、次のスクリプトは次のdestruct pff行で失敗します。

Definition False : Prop := forall A : Prop, A.
Definition not (P : Prop) : Prop := P -> False.

Lemma test P : not (not (not (not P) -> P)).
unfold not.
intro pffpf.
apply pffpf.
intro pff.
destruct pff. (* Fails here *)
intro p.
apply pffpf.
intro pff.
exact p.
Qed.