可以在Coq中隐式使用destruct吗？ [英] Can destruct used in implication in Coq?

问题描述

destruct 可用于在Coq中拆分和，或。但是似乎还可以暗示使用吗？
例如，我想证明 ~~（~~ P-> P）

destruct can be used to split and, or in Coq. But it seems can also be used in implication? For example, I want to prove ~~(~~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.

当破坏pff时。但我不知道为什么？有人可以为我解释吗？

when destruct pff. it works fine, but I don't know why? Can anyone explain it for me?

推荐答案

破坏策略在如果隐含的结论是归纳（或共归纳）类型，则表示隐含。因此它适用于您的示例，因为 False 是归纳定义的。但是，如果我们提出了 False 的不同定义，则不一定有效。例如，以下脚本在 destruct pff 行失败：

The destruct tactic works on implications if the conclusion of the implication is of inductive (or co-inductive) type. Hence it works on your example, because False is defined inductively. However, if we came up with a different definition of False, it might not necessarily work. For instance, the following script fails at the destruct pff line:

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.

这篇关于可以在Coq中隐式使用destruct吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！