Automatisation des ssreflect, Coq tout en traitant des hypothèses contredite sur les chiffres nat

Question

En utilisant ssreflect dans le lemme suivant:

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. 

Puis-je demander pourquoi les autos, que j'ai commenté, ne fonctionnent pas à ces états de preuve ? car il me semble que ces états observent déjà une contradiction dans le contexte.

Y at-il une automatisation par ssreflect pour prouver ce lemme?

Answer 1

Je pense que si vous supprimez certaines notations et les coercitions vous obtenez une vue plus claire de ce qui se passe dans cet objectif:

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

En particulier, auto ne fonctionne pas comme il est pas assez puissant pour raison du comportement de negb. Toutefois, lorsque vous repassez, votre objectif devient:

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

donc après simplification, false = true est dans le contexte et auto peut en effet fermer l'objectif.