Автоматизация ssreflect, Coq при работе с противоречивыми гипотезами о натуральных числах

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 действительно может закрыть цель.