replacing omega with lia in some file

4 files changed, 34 insertions, 30 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index c606002a..073f1f4c 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -37,6 +37,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
 Require Import OptionMonad Asm.
+Require Import Lia.
 Require Export Asm.
 
 Local Open Scope option_monad_scope.
@@ -437,7 +438,7 @@ Qed.
 Lemma size_positive (b:bblock): size b > 0.
 Proof.
   unfold size. destruct b as [hd bdy ex cor]. cbn.
-  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega);
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia);
   unfold non_empty_bblockb in cor; simpl in cor.
   inversion cor.
 Qed.
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.
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 03d863a3..004cfd5c 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -38,6 +38,7 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Asmblockprops.
+Require Import Lia.
 
 Module MB:=Machblock.
 Module AB:=Asmblock.
@@ -395,7 +396,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
 Lemma code_tail_pos:
   forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
 Proof.
-  induction 1. omega. generalize (size_positive bi); intros; omega.
+  induction 1. lia. generalize (size_positive bi); intros; lia.
 Qed.
 
 Lemma find_bblock_tail:
@@ -405,10 +406,10 @@ Lemma find_bblock_tail:
 Proof.
   induction c1; simpl; intros.
   inversion H.  
-  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
   destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
-  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
   eauto.
 Qed.
 
@@ -422,13 +423,13 @@ Proof.
   induction 1; intros.
   - subst; eauto.
   - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
-    omega.
+    lia.
 Qed.
 
 Lemma size_blocks_pos c: 0 <= size_blocks c.
 Proof.
-  induction c as [| a l ]; simpl; try omega.
-  generalize (size_positive a); omega.
+  induction c as [| a l ]; simpl; try lia.
+  generalize (size_positive a); lia.
 Qed.
 
 Remark code_tail_positive:
@@ -436,15 +437,15 @@ Remark code_tail_positive:
   code_tail ofs fn c -> 0 <= ofs.
 Proof.
   induction 1; intros; simpl.
-  - omega.
-  - generalize (size_positive bi). omega.
+  - lia.
+  - generalize (size_positive bi). lia.
 Qed.
 
 Remark code_tail_size:
   forall fn ofs c,
   code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
 Proof.
-  induction 1; intros; simpl; try omega.
+  induction 1; intros; simpl; try lia.
 Qed.
 
 Remark code_tail_bounds fn ofs c:
@@ -453,7 +454,7 @@ Proof.
   intro H; 
   exploit code_tail_size; eauto.
   generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
-  omega.
+  lia.
 Qed.
 
 Local Hint Resolve code_tail_next: core.
@@ -470,8 +471,8 @@ Proof.
   intros.
   rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
   - rewrite Ptrofs.unsigned_repr; eauto.
-    omega.
-  - rewrite Ptrofs.unsigned_repr; omega.
+    lia.
+  - rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 (** The [find_label] function returns the code tail starting at the
@@ -505,12 +506,12 @@ Proof.
   simpl; intros until c'.
   case (is_label lbl a).
   - intros. inv H. exists pos. split; auto. split.
-    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
-    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+    replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
+    generalize (size_blocks_pos c). generalize (size_positive a). lia.
   - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
-  constructor. auto. generalize (size_positive a). omega.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
+  constructor. auto. generalize (size_positive a). lia.
 Qed.
 
 (** Predictor for return addresses in generated Asm code.
@@ -589,7 +590,7 @@ Proof.
     exists (Ptrofs.repr ofs). red; intros.
     rewrite Ptrofs.unsigned_repr. congruence.
     exploit code_tail_bounds; eauto.
-    intros; apply transf_function_len in TF. omega.
+    intros; apply transf_function_len in TF. lia.
   + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
@@ -613,7 +614,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
 Remark code_tail_no_bigger:
   forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
 Proof.
-  induction 1; simpl; omega.
+  induction 1; simpl; lia.
 Qed.
 
 Remark code_tail_unique:
@@ -621,8 +622,8 @@ Remark code_tail_unique:
   code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
 Proof.
   induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
-  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
+  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia.
   f_equal. eauto.
 Qed.
 
diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v
index 48840602..a5084b5f 100644
--- a/aarch64/PostpassSchedulingproof.v
+++ b/aarch64/PostpassSchedulingproof.v
@@ -21,6 +21,7 @@ Require Import Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -171,7 +172,7 @@ Proof.
   induction tc.
   - intros. simpl in H. discriminate.
   - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
-    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + inv H. assert (k = k') by lia. subst. reflexivity.
     + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
 Qed.