考虑到欧米茄策略是在COQ中重新定论的，该如何导入LIA策略？

Question

我有错误：

Error: The reference lia was not found in the current environment.

如何解决？

代码：

Require Import Lia.

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

Answer 1

做需要导入lia。在顶部。例如，

Require Import Lia.

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

注意这是Omega编辑的替代

---

：

正如Ana Borges所指出的那样：

请注意，根据 coq changelog ，Omega仅在COQ 8.12中弃权并在8.14中删除。如果您使用的是旧版本的Coq，则仍然可以使用它。但是，即使在8.11中，建议是切换到LIA，除非您有很好的理由，否则我建议您更新COQ安装（最新的是8.15.2）。