Automatisierung von ssreflect, Coq während Umgang mit widersprachen Hypothesen über nat Zahlen

Question

Während ssreflect in folgenden Lemma mit:

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. 

Darf ich fragen, warum diejenigen autos, dass ich auf Kommentar, nicht an diesen Beweis Staaten arbeiten ? wie es mir scheint, dass diese Staaten bereits Widerspruch im Zusammenhang beobachten.

Und gibt es eine Automatisierung von ssreflect, um dieses Lemma zu beweisen?

Answer 1

Ich denke, wenn Sie einige Notationen entfernen und die Nötigungen Sie bekommen eine klarere Sicht von dem, was in diesem Ziel vor sich geht:

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

Insbesondere auto nicht funktioniert, da es nicht leistungsfähig genug ist, um zu Grund für das Verhalten von negb. Wenn Sie jedoch neu zu schreiben, um Ihr Ziel wird:

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

so nach Vereinfachung, false = true ist im Kontext und auto kann in der Tat das Ziel schließen.