replacing omega with lia in some file

3 files changed, 8 insertions, 7 deletions

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 0716dad7..cf51f5a2 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -620,7 +620,7 @@ Proof.
   destruct a; simpl in H10; try discriminate; simpl; trivial.
   rewrite negb_false_iff in H8.
   eapply Mem.load_storebytes_other. eauto.
-  rewrite H6. rewrite Z2Nat.id by omega.
+  rewrite H6. rewrite Z2Nat.id by lia.
   eapply pdisjoint_sound. eauto.
   unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto.
   erewrite <- regs_valnums_sound by eauto. eauto with va.
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index 9e5ad6df..dd5e72f8 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -89,7 +89,7 @@ Qed.
 Obligation 2.
 Proof.
   simpl in BOUND.
-  omega.
+  lia.
 Qed.
 
 Program Definition bounded_nth_S_statement : Prop :=
@@ -104,14 +104,14 @@ Lemma bounded_nth_proof_irr :
          (BOUND1 BOUND2 : (k < List.length l)%nat),
     (bounded_nth k l BOUND1) = (bounded_nth k l BOUND2).
 Proof.
-  induction k; destruct l; simpl; intros; trivial; omega.
+  induction k; destruct l; simpl; intros; trivial; lia.
 Qed.
 
 Lemma bounded_nth_S : bounded_nth_S_statement.
 Proof.
   unfold bounded_nth_S_statement.
   induction k; destruct l; simpl; intros; trivial.
-  1, 2: omega.
+  1, 2: lia.
   apply bounded_nth_proof_irr.
 Qed.
 
@@ -121,7 +121,7 @@ Lemma inject_list_injected:
     Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))).
 Proof.
   induction l; simpl; intros.
-  - omega.
+  - lia.
   - simpl.
     destruct k as [ | k]; simpl pos_add_nat.
     + simpl bounded_nth.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 0f895040..5a7cfc12 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -15,6 +15,7 @@ Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers RTL.
+Require Import Lia.
 
 (** The abstract domains for value analysis *)
 
@@ -2822,8 +2823,8 @@ Proof.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
-    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
-    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
+    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD.
+    unfold Int.modu. rewrite Int.unsigned_repr. lia. lia.
   }
   intros until y.
   intros HX HY.