1

我对 nat 数字有两个条件：

H:  a < b
H1: b < a

如何区分目标？< 是否存在任何策略？

4

2 回答 2

2

使用lia：

From Coq Require Import Lia.

Goal forall a b, a < b -> b < a -> False.
  lia.
Qed.

您可以在此处了解更多关于lia算术决策程序和其他决策程序的信息。

于 2020-02-08T15:27:37.620 回答
0

作为参考，在这种情况下进行手动证明并不是那么困难：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo a b (a_lt_b : a < b) : b < a -> False.
Proof. by rewrite ltnNge (ltnW a_lt_b). Qed.
于 2020-02-09T00:24:03.343 回答