coq - 可以在 Coq 中隐含使用 destruct 吗？

Question

destruct可用于拆分and，或在 Coq 中。不过好像也可以用含蓄？例如，我想证明~~(~~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.