0

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.
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • related: https://stackoverflow.com/questions/36381470/coq-error-the-reference-evenb-was-not-found-in-the-current-environment – Charlie Parker Jun 11 '22 at 16:46
  • Which version of Coq are you using? You can check with `coqc --version` on a terminal. – Ana Borges Jun 11 '22 at 20:39
  • I am using `8.11.0` @AnaBorges – Charlie Parker Jun 13 '22 at 14:36
  • Ok, I just realized you answered yourself. I was super confused because your *question* already includes the solution. I was afraid `Require Import Lia` was not working for you for some reason. – Ana Borges Jun 13 '22 at 16:50
  • Note that according to the [Coq changelog](https://coq.inria.fr/refman/changes.html), `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). – Ana Borges Jun 13 '22 at 16:50
  • @AnaBorges thanks ana! Appreciate it. My code is sort of a silly debug example, so for me it doesn't matter, but I think your comment is useful to whoever is actually curious/need to know this. Will thus update my answer with your comment and credit. :) – Charlie Parker Jun 13 '22 at 16:53

1 Answers1

0

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

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323