Coq中omega策略弃用后如何正确导入lia策略修复引用报错

报错核心原因 #

触发Error: The reference lia was not found in the current environment.报错，本质是lia策略所属的模块未被正确加载，和Coq版本、导入语句写法、依赖完整性直接相关。

对应修复方案 #

适用于Coq 8.12及以上版本 #

从Coq 8.12版本开始，lia正式作为标准库内置策略替代弃用的omega，归入独立的Lia模块，按以下步骤排查修复：

• 优先使用全路径导入语句，避免第三方库同名文件冲突，将原代码开头的导入语句替换为From Coq Require Import Lia.，该写法比直接写Require Import Lia.兼容性更好
• 导入后仍报错的话，先在终端执行coqc -v确认本地Coq版本确实≥8.12
• 版本符合要求的前提下，直接重启CoqIDE/Proof General的Coq后台进程，从头重新编译整个文件即可
• 如果是通过OPAM包管理器安装的Coq，执行opam install coq-micromega补全线性算术策略的相关依赖，安装完成后重启Coq进程即可正常使用

验证可用的最小测试代码如下：

From Coq Require Import Lia.

Theorem t:
    forall n: nat, 1 + n > n.
Proof.
 intro n.
 lia.
Qed.

适用于Coq 8.11及更早版本 #

8.12之前的版本没有独立的Lia模块，lia作为测试功能随Omega模块分发，按以下方式处理：

• 将导入语句替换为Require Import Omega.即可正常调用lia
• 如果导入Omega后仍找不到lia，说明当前版本过老还未内置lia，直接使用当时尚未弃用的omega策略即可完成整数/自然数线性算术目标的证明，对应代码：

Require Import Omega.

Theorem t:
    forall n: nat, 1 + n > n.
Proof.
 intro n.
 omega.
Qed.

内容的提问来源于stack exchange，提问作者Charlie Parker