CODEWITHSUNDEEP
coq
Charlie Parker
Charlie Parker

Reputation: 5231

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.

Upvotes: 1

Views: 1595

Answers (1)

Charlie Parker
Charlie Parker

Reputation: 5231

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).

Upvotes: 0

Related Questions