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.