Omega模块废弃后，替代exfalso omega的正确方法是什么？

在处理像0 > 0这类算术矛盾目标时，原exfalso. omega.的组合可以用以下几种方式替代：

直接使用lia tactic #

lia是Coq官方推荐用于替代Omega的线性算术求解器，功能覆盖Omega的核心场景，且维护更活跃。对于矛盾的算术目标，你可以直接用：

exfalso. lia.

甚至很多时候，lia本身就能识别矛盾并完成证明，不需要先调用exfalso，直接写lia.即可。

针对非整数算术场景的somega #

如果你的证明涉及实数等非整数算术，somega（属于Coq的Ssreflect库）是更合适的选择，用法类似：

exfalso. somomega.

使用somega需要先导入Ssreflect库：

Require Import ssreflect ssrbool ssrnat.

基础逻辑矛盾的简化处理 #

如果矛盾是非常基础的逻辑或自然数命题（比如0 = 1），也可以用更基础的tactic直接解决：

• 对于自然数的矛盾，用discriminate.或inversion.
• 对于布尔值矛盾，用contradiction.

比如遇到0 > 0，也可以这样写：

exfalso. apply Nat.nle_gt in H. contradiction.

不过这种写法不如lia简洁通用。

内容的提问来源于stack exchange，提问作者Attila Károly