replacing omega with lia in some file

3 files changed, 11 insertions, 8 deletions

diff --git a/common/Events.v b/common/Events.v
index 13741ebd..aff9e256 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -25,6 +25,7 @@ Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
 Require Import Builtins.
+Require Import Lia.
 
 (** * Events and traces *)
 
@@ -1443,7 +1444,7 @@ Proof.
   econstructor; eauto.
   red; intros; congruence.
 (* trace length *)
-- inv H; simpl; omega.
+- inv H; simpl; lia.
 (* receptive *)
 - inv H; inv H0. exists Vundef, m1; constructor.
 (* determ *)
diff --git a/common/Memdata.v b/common/Memdata.v
index 1d651db2..6f04db36 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -23,6 +23,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
+Require Import Lia.
 
 (** * Properties of memory chunks *)
 
@@ -48,7 +49,7 @@ Definition largest_size_chunk := 8.
 
 Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8.
 Proof.
-  destruct chunk; simpl; omega.
+  destruct chunk; simpl; lia.
 Qed.
 
 Lemma size_chunk_pos:
diff --git a/common/Values.v b/common/Values.v
index 1d272932..c48dca25 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -20,6 +20,7 @@ Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
+Require Import Lia.
 
 Definition block : Type := positive.
 Definition eq_block := peq.
@@ -1535,14 +1536,14 @@ Proof.
     replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl.
     replace (Int.ltu n Int.iwordsize) with true.
     f_equal; apply Int.shrx_shr_2; assumption.
-    symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
+    symmetry; apply zlt_true. change (Int.unsigned n < 32); lia.
     symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
     assert (Int.unsigned n <> 0).
     { red; intros; elim H.
       rewrite <- (Int.repr_unsigned n), H0. auto. }
     rewrite Int.unsigned_repr.
-    change (Int.unsigned Int.iwordsize) with 32; omega.
-    assert (32 < Int.max_unsigned) by reflexivity. omega.
+    change (Int.unsigned Int.iwordsize) with 32; lia.
+    assert (32 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem or_rolm:
@@ -1848,12 +1849,12 @@ simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl.
   replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl.
   replace (Int.ltu n Int64.iwordsize') with true.
   f_equal; apply Int64.shrx'_shr_2; assumption.
-  symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
+  symmetry; apply zlt_true. change (Int.unsigned n < 64); lia.
   symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
   assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
   rewrite Int.unsigned_repr.
-  change (Int.unsigned Int64.iwordsize') with 64; omega.
-  assert (64 < Int.max_unsigned) by reflexivity. omega.
+  change (Int.unsigned Int64.iwordsize') with 64; lia.
+  assert (64 < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem negate_cmp_bool: