replacing omega with lia in some file

1 files changed, 8 insertions, 7 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 6f7d39fa..11219928 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -19,6 +19,7 @@ Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock IterList.
 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
+Require Import Lia.
 
 Module MB := Machblock.
 Module AB := Asmblock.
@@ -71,7 +72,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
@@ -298,8 +299,8 @@ Proof.
   split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
-  auto. omega.
-  generalize (transf_function_no_overflow _ _ H0). omega.
+  auto. lia.
+  generalize (transf_function_no_overflow _ _ H0). lia.
   intros. apply Pregmap.gso; auto.
 Qed.
 
@@ -389,7 +390,7 @@ Lemma mbsize_eqz:
 Proof.
   intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
   remember (length _) as a. remember (length_opt _) as b.
-  assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
+  assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
   inv H0. inv H1. destruct bdy; destruct ex; auto.
   all: try discriminate.
 Qed.
@@ -1452,11 +1453,11 @@ Proof.
       rewrite Pregmap.gso; auto. rewrite V; auto.
   } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
   exploit exec_straight_steps_2; eauto using functions_transl.
-  simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
+  simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
   intros (ofs' & X & Y).
   left; exists (State rs3' m3'); split.
   eapply exec_straight_steps_1; eauto.
-  simpl fn_blocks. simpl fn_blocks in g. omega.
+  simpl fn_blocks. simpl fn_blocks in g. lia.
   constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
@@ -1495,7 +1496,7 @@ Local Transparent destroyed_at_function_entry.
 - (* return *) 
   inv MS.
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
 Qed.