Coq中蘊含的可以破壞嗎？

Question

destruct可用於在Coq。中拆分和,或。但它似乎也可以用於暗示？ 例如，我要證明~~(~~P -> P)

Lemma test : ~~(~~P -> P). 
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.