coq - ssreflect、Coq 的自动化，同时处理关于 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确实可以接近目标。