在处理与nat数有关的自相矛盾的假设时，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确实可以关闭目标。