自動化ssreflect的，勒柯克而與矛盾的假設處理有關NAT號

Question

而在下面的引理使用ssreflect：

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype. 

Lemma nat_dec n m: (m <= n) -> (~~ (m <= n)) -> False. 
Proof. 
    intros A notA. 
    (* auto. *) 
    red in A. 
    red in notA. 
    (* auto. *) 
    rewrite -> A in notA. 
    auto. 
Qed. 

我可以問一下爲什麼這些autos，我註釋掉，不工作的那些證明狀態？因爲在我看來，這些國家已經在上下文中觀察到了矛盾。

是否有一些自動化由ssreflect來證明這個引理？

Answer 1

我認爲，如果你刪除一些符號和的強制你是怎麼回事這個目標更清晰的視野：

Lemma nat_dec n m: (m <= n = true) -> (negb (m <= n) = true) -> False. 

尤其auto不起作用，因爲它不是足夠強大關於negb的行爲的原因。然而，當你改寫，你的目標就變成了：

Lemma nat_dec n m: (m <= n = true) -> (negb true = true) -> False. 

如此簡單化後，false = true是在上下文和auto的確可以關閉目標。