Search code examples
coq

How does one import the lia tactic given that the omega tactic was reprecated in Coq?

I got the error:

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

how do I fix it?

code:

Require Import Lia.

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

  • Do Require Import Lia. at the top. e.g.

    Require Import Lia.

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

    note this is a replacement for Omega

    Edit:

    As Ana Borges kindly pointed out:

    Note that according to the Coq changelog, omega was only deprecated in Coq 8.12 and removed in 8.14. If you are using an older version of Coq, you can still make use of it. However, even in 8.11 the recommendation was to switch to lia, and unless you have a very good reason I would recommend updating your Coq installation anyway (the latest is 8.15.2).