lia instead of omega in lib

1 files changed, 51 insertions, 51 deletions

diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index e26c24e7..754b49d6 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -18,7 +18,7 @@
 
 Require Import Coqlib Errors Maps Zbits.
 Require Import AST Integers Floats Values Memory Globalenvs Linking.
-Require Import Op Locations Machblock Conventions.
+Require Import Op Locations Machblock Conventions Lia.
 Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
 
 Module MB := Machblock.
@@ -139,8 +139,8 @@ Local Opaque Zzero_ext.
   induction N as [ | N]; simpl; intros.
   - constructor.
   - set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0).
-    + apply IHN. omega.
-    + econstructor. reflexivity. omega. apply IHN; omega. 
+    + apply IHN. lia.
+    + econstructor. reflexivity. lia. apply IHN; lia. 
 Qed.
 
 Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z :=
@@ -158,43 +158,43 @@ Lemma decompose_int_correct:
    if zlt i p then Z.testbit accu i else Z.testbit n i).
 Proof.
   induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE.
-  - simpl. rewrite zlt_true; auto. xomega.
+  - simpl. rewrite zlt_true; auto. lia.
   - rewrite inj_S in RANGE. simpl.
     set (frag := Zzero_ext 16 (Z.shiftr n p)).
     assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)).
-    { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega.
-      rewrite Z.shiftr_spec by omega. f_equal; omega. }
+    { unfold frag; intros. rewrite Zzero_ext_spec by lia. rewrite zlt_true by lia.
+      rewrite Z.shiftr_spec by lia. f_equal; lia. }
     destruct (Z.eqb_spec frag 0).
     + rewrite IHN.
-      * destruct (zlt i p). rewrite zlt_true by omega. auto.
+      * destruct (zlt i p). rewrite zlt_true by lia. auto.
         destruct (zlt i (p + 16)); auto.
-        rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto.
-      * omega.
-      * intros; apply ABOVE; omega.
-      * xomega.
+        rewrite ABOVE by lia. rewrite FRAG by lia. rewrite e, Z.testbit_0_l. auto.
+      * lia.
+      * intros; apply ABOVE; lia.
+      * lia.
     + simpl. rewrite IHN.
       * destruct (zlt i (p + 16)).
-        ** rewrite Zinsert_spec by omega. unfold proj_sumbool.
-           rewrite zlt_true by omega.
+        ** rewrite Zinsert_spec by lia. unfold proj_sumbool.
+           rewrite zlt_true by lia.
            destruct (zlt i p).
-           rewrite zle_false by omega. auto.
-           rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega.
-        ** rewrite Z.ldiff_spec, Z.shiftl_spec by omega.
-           change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega.
-           rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. 
-      * omega.
-      * intros. rewrite Zinsert_spec by omega. unfold proj_sumbool.
-        rewrite zle_true by omega. rewrite zlt_false by omega. simpl.
-        apply ABOVE. omega.
-      * xomega.
+           rewrite zle_false by lia. auto.
+           rewrite zle_true by lia. simpl. symmetry; apply FRAG; lia.
+        ** rewrite Z.ldiff_spec, Z.shiftl_spec by lia.
+           change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by lia.
+           rewrite zlt_false by lia. rewrite zlt_false by lia. apply andb_true_r. 
+      * lia.
+      * intros. rewrite Zinsert_spec by lia. unfold proj_sumbool.
+        rewrite zle_true by lia. rewrite zlt_false by lia. simpl.
+        apply ABOVE. lia.
+      * lia.
 Qed.
 
 Corollary decompose_int_eqmod: forall N n,
   eqmod (two_power_nat (N * 16)%nat) (recompose_int 0 (decompose_int N n 0)) n.
 Proof.
   intros; apply eqmod_same_bits; intros.
-  rewrite decompose_int_correct. apply zlt_false; omega. 
-  omega. intros; apply Z.testbit_0_l. xomega.
+  rewrite decompose_int_correct. apply zlt_false; lia. 
+  lia. intros; apply Z.testbit_0_l. lia.
 Qed.
 
 Corollary decompose_notint_eqmod: forall N n,
@@ -203,8 +203,8 @@ Corollary decompose_notint_eqmod: forall N n,
 Proof.
   intros; apply eqmod_same_bits; intros.
   rewrite Z.lnot_spec, decompose_int_correct.
-  rewrite zlt_false by omega. rewrite Z.lnot_spec by omega. apply negb_involutive.
-  omega. intros; apply Z.testbit_0_l. xomega. omega.
+  rewrite zlt_false by lia. rewrite Z.lnot_spec by lia. apply negb_involutive.
+  lia. intros; apply Z.testbit_0_l. lia. lia.
 Qed.
 
 Lemma negate_decomposition_wf:
@@ -214,7 +214,7 @@ Proof.
   instantiate (1 := (Z.lnot m)).
   apply equal_same_bits; intros.
   rewrite H. change 65535 with (two_p 16 - 1).
-  rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by omega.
+  rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by lia.
   destruct (zlt i 16).
   apply xorb_true_r.
   auto.
@@ -225,7 +225,7 @@ Lemma Zinsert_eqmod:
   eqmod (two_power_nat n) x1 x2 ->
   eqmod (two_power_nat n) (Zinsert x1 y p l) (Zinsert x2 y p l).
 Proof.
-  intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by omega.
+  intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by lia.
   destruct (zle p i && zlt i (p + l)); auto.
   apply same_bits_eqmod with n; auto.
 Qed.
@@ -236,12 +236,12 @@ Lemma Zinsert_0_l:
   Z.shiftl (Zzero_ext l y) p = Zinsert 0 (Zzero_ext l y) p l.
 Proof.
   intros. apply equal_same_bits; intros.
-  rewrite Zinsert_spec by omega. unfold proj_sumbool.
-  destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl.
+  rewrite Zinsert_spec by lia. unfold proj_sumbool.
+  destruct (zlt i p); [rewrite zle_false by lia|rewrite zle_true by lia]; simpl.
   - rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto.
-  - rewrite Z.shiftl_spec by omega. 
+  - rewrite Z.shiftl_spec by lia. 
     destruct (zlt i (p + l)); auto.
-    rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto.
+    rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by lia. auto.
 Qed.
 
 Lemma recompose_int_negated:
@@ -251,12 +251,12 @@ Proof.
   induction 1; intros accu; simpl.
   - auto.
   - rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. 
-    rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega.
+    rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by lia.
     unfold proj_sumbool.
     destruct (zle p i); simpl; auto.
     destruct (zlt i (p + 16)); simpl; auto.
     change 65535 with (two_p 16 - 1).
-    rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega.
+    rewrite Ztestbit_two_p_m1 by lia. rewrite zlt_true by lia.
     apply xorb_true_r. 
 Qed.
 
@@ -277,7 +277,7 @@ Proof.
                   (Zinsert accu n p 16))
     as (rs' & P & Q & R).
     Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. 
-    apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+    apply Zinsert_eqmod. auto. lia. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
     exists rs'; split.
     eapply exec_straight_opt_step_opt. simpl. eauto. auto.
     split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
@@ -302,7 +302,7 @@ Proof.
     unfold rs1; Simpl.
     exists rs2; split.
     eapply exec_straight_opt_step; eauto.
-    simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
+    simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; lia.
     split. exact Q. 
     intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
@@ -329,7 +329,7 @@ Proof.
     exists rs2; split.
     eapply exec_straight_opt_step; eauto.
     simpl. unfold rs1. do 5 f_equal.
-    unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
+    unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; lia.
     split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
     intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
@@ -358,8 +358,8 @@ Proof.
       apply Int.eqm_samerepr. apply decompose_notint_eqmod. 
       apply Int.repr_unsigned. }
     destruct Nat.leb.
-    + rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
-    + rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
+    + rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; lia.
+    + rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; lia.
 Qed.
 
 Lemma exec_loadimm_k_x:
@@ -379,7 +379,7 @@ Proof.
                   (Zinsert accu n p 16))
     as (rs' & P & Q & R).
     Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. 
-    apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
+    apply Zinsert_eqmod. auto. lia. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
     exists rs'; split.
     eapply exec_straight_opt_step_opt. simpl; eauto. auto.
     split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
@@ -404,7 +404,7 @@ Proof.
     unfold rs1; Simpl.
     exists rs2; split.
     eapply exec_straight_opt_step; eauto.
-    simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
+    simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; lia.
     split. exact Q. 
     intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
@@ -431,7 +431,7 @@ Proof.
     exists rs2; split.
     eapply exec_straight_opt_step; eauto.
     simpl. unfold rs1. do 5 f_equal.
-    unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
+    unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; lia.
     split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
     intros. rewrite R by auto. unfold rs1; Simpl.
 Qed.
@@ -460,8 +460,8 @@ Proof.
       apply Int64.eqm_samerepr. apply decompose_notint_eqmod. 
       apply Int64.repr_unsigned. }
     destruct Nat.leb.
-    + rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
-    + rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
+    + rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; lia.
+    + rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; lia.
 Qed.
 
 (** Add immediate *)
@@ -480,14 +480,14 @@ Lemma exec_addimm_aux_32:
 Proof.
   intros insn sem SEM ASSOC; intros. unfold addimm_aux.
   set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo).
-  assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega).
+  assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; lia).
   rewrite <- (Int.repr_unsigned n).
   destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
   - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-    split. Simpl. do 3 f_equal; omega.
+    split. Simpl. do 3 f_equal; lia.
     intros; Simpl.
   - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-    split. Simpl. do 3 f_equal; omega.
+    split. Simpl. do 3 f_equal; lia.
     intros; Simpl.
   - econstructor; split. eapply exec_straight_two.
     apply SEM. apply SEM. simpl. Simpl.
@@ -538,14 +538,14 @@ Lemma exec_addimm_aux_64:
 Proof.
   intros insn sem SEM ASSOC; intros. unfold addimm_aux.
   set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo).
-  assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega).
+  assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; lia).
   rewrite <- (Int64.repr_unsigned n).
   destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
   - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-    split. Simpl. do 3 f_equal; omega.
+    split. Simpl. do 3 f_equal; lia.
     intros; Simpl.
   - econstructor; split. apply exec_straight_one. apply SEM. Simpl. 
-    split. Simpl. do 3 f_equal; omega.
+    split. Simpl. do 3 f_equal; lia.
     intros; Simpl.
   - econstructor; split. eapply exec_straight_two.
     apply SEM. apply SEM. Simpl. Simpl.