Replace `omega` tactic with `lia`

Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal.

Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`,
and `xomegaContradiction` with `lia` and `extlia`.

Turn back on the deprecation warning for uses of `omega`.

Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.

9 files changed, 133 insertions, 133 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 346cb649..b5f4c838 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -1293,7 +1293,7 @@ Ltac Equalities :=
   split. auto. intros. destruct B; auto. subst. auto.
 - (* trace length *)
   red; intros. inv H; simpl.
-  omega.
+  lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 - (* initial states *)
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index d3515a96..dc0bc509 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -67,7 +67,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma exec_straight_exec:
@@ -424,8 +424,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.
 
@@ -949,10 +949,10 @@ Local Transparent destroyed_by_op.
     rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
     reflexivity. 
     eexact U. }
-  exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
+  exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
   intros (ofs' & X & Y).                    
   left; exists (State rs3 m3'); split.
-  eapply exec_straight_steps_1; eauto. omega. constructor.
+  eapply exec_straight_steps_1; eauto. lia. constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
   apply agree_exten with rs2; eauto with asmgen.
@@ -981,7 +981,7 @@ Local Transparent destroyed_at_function_entry. simpl.
 
 - (* return *)
   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/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index d95376d2..5f27f6bf 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -81,8 +81,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 :=
@@ -100,43 +100,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. extlia.
 - 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.
+* extlia.
 + 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.
+* extlia.
 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. extlia.
 Qed.
 
 Corollary decompose_notint_eqmod: forall N n,
@@ -145,8 +145,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. extlia. lia.
 Qed.
 
 Lemma negate_decomposition_wf:
@@ -156,7 +156,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.
@@ -167,7 +167,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.
@@ -178,12 +178,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:
@@ -193,12 +193,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.
 
@@ -219,7 +219,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. exact P.
   split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
@@ -244,7 +244,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.
   reflexivity.
   split. exact Q. 
   intros. rewrite R by auto. unfold rs1; Simpl.
@@ -272,7 +272,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.
   reflexivity.  
   split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
   intros. rewrite R by auto. unfold rs1; Simpl.
@@ -302,8 +302,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:
@@ -323,7 +323,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. exact P.
   split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
@@ -348,7 +348,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.
   reflexivity.
   split. exact Q. 
   intros. rewrite R by auto. unfold rs1; Simpl.
@@ -376,7 +376,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.
   reflexivity.  
   split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
   intros. rewrite R by auto. unfold rs1; Simpl.
@@ -406,8 +406,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 *)
@@ -426,14 +426,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.
@@ -484,14 +484,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.
diff --git a/aarch64/ConstpropOpproof.v b/aarch64/ConstpropOpproof.v
index deab7cd4..7f5f1e06 100644
--- a/aarch64/ConstpropOpproof.v
+++ b/aarch64/ConstpropOpproof.v
@@ -391,7 +391,7 @@ Proof.
   Int.bit_solve. destruct (zlt i0 n0).
   replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
   rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
-  rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
+  rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
   rewrite Int.bits_not by auto. apply negb_involutive.
   rewrite H6 by auto. auto.
   econstructor; split; eauto. auto.
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v
index 4873dd91..cfcbcbf1 100644
--- a/aarch64/Conventions1.v
+++ b/aarch64/Conventions1.v
@@ -274,33 +274,33 @@ Proof.
   assert (ALP: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
   { intros. 
     assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
-    omega. }
+    lia. }
   assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
   { intros. apply Z.divide_trans with (typesize ty). apply typealign_typesize. apply align_divides. apply typesize_pos. }
   assert (ALP2: forall ofs, ofs >= 0 -> align ofs 2 >= 0).
   { intros. 
-    assert (ofs <= align ofs 2) by (apply align_le; omega).
-    omega. }
+    assert (ofs <= align ofs 2) by (apply align_le; lia).
+    lia. }
   assert (ALD2: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs 2)).
   { intros. eapply Z.divide_trans with 2.
     exists (2 / typealign ty). destruct ty; reflexivity.
-    apply align_divides. omega. }
+    apply align_divides. lia. }
   assert (STK: forall tyl ofs,
                ofs >= 0 -> OK (loc_arguments_stack tyl ofs)).
   { induction tyl as [ | ty tyl]; intros ofs OO; red; simpl; intros.
   - contradiction.
   - destruct H.
     + subst p. split. auto. simpl. apply Z.divide_1_l.
-    + apply IHtyl with (ofs := ofs + 2). omega. auto.
+    + apply IHtyl with (ofs := ofs + 2). lia. auto.
   }  
   assert (A: forall ty ri rf ofs f,
              OKF f -> ofs >= 0 -> OK (stack_arg ty ri rf ofs f)).
   { intros until f; intros OF OO; red; unfold stack_arg; intros.
     destruct Archi.abi; destruct H.
   - subst p; simpl; auto.
-  - eapply OF; [|eauto]. apply ALP2 in OO. omega.
+  - eapply OF; [|eauto]. apply ALP2 in OO. lia.
   - subst p; simpl; auto.  
-  - eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). omega.
+  - eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). lia.
   }
   assert (B: forall ty ri rf ofs f,
              OKF f -> ofs >= 0 -> OK (int_arg ty ri rf ofs f)).
@@ -332,7 +332,7 @@ Lemma loc_arguments_acceptable:
   In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
 Proof.
   unfold loc_arguments; intros.
-  eapply loc_arguments_rec_charact; eauto. omega.
+  eapply loc_arguments_rec_charact; eauto. lia.
 Qed.
 
 Hint Resolve loc_arguments_acceptable: locs.
diff --git a/aarch64/Op.v b/aarch64/Op.v
index a7483d56..f8d2510e 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -957,25 +957,25 @@ End SHIFT_AMOUNT.
 Program Definition mk_amount32 (n: int): amount32 :=
   {| a32_amount := Int.zero_ext 5 n |}.
 Next Obligation.
-  apply mk_amount_range. omega. reflexivity.
+  apply mk_amount_range. lia. reflexivity.
 Qed.
 
 Lemma mk_amount32_eq: forall n,
   Int.ltu n Int.iwordsize = true -> a32_amount (mk_amount32 n) = n.
 Proof.
-  intros. eapply mk_amount_eq; eauto. omega. reflexivity.
+  intros. eapply mk_amount_eq; eauto. lia. reflexivity.
 Qed.
 
 Program Definition mk_amount64 (n: int): amount64 :=
   {| a64_amount := Int.zero_ext 6 n |}.
 Next Obligation.
-  apply mk_amount_range. omega. reflexivity.
+  apply mk_amount_range. lia. reflexivity.
 Qed.
 
 Lemma mk_amount64_eq: forall n,
   Int.ltu n Int64.iwordsize' = true -> a64_amount (mk_amount64 n) = n.
 Proof.
-  intros. eapply mk_amount_eq; eauto. omega. reflexivity.
+  intros. eapply mk_amount_eq; eauto. lia. reflexivity.
 Qed.
  
 (** Recognition of move operations. *)
diff --git a/aarch64/SelectLongproof.v b/aarch64/SelectLongproof.v
index b051369c..aee09b12 100644
--- a/aarch64/SelectLongproof.v
+++ b/aarch64/SelectLongproof.v
@@ -225,8 +225,8 @@ Proof.
   intros. unfold Int.ltu; apply zlt_true.
   apply Int.ltu_inv in H. apply Int.ltu_inv in H0.
   change (Int.unsigned Int64.iwordsize') with Int64.zwordsize in *.
-  unfold Int.sub; rewrite Int.unsigned_repr. omega.
-  assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. omega.
+  unfold Int.sub; rewrite Int.unsigned_repr. lia.
+  assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. lia.
 Qed.
 
 Theorem eval_shrluimm:
@@ -242,13 +242,13 @@ Local Opaque Int64.zwordsize.
 + destruct (Int.ltu n a) eqn:L2.
 * assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true).
   { apply sub_shift_amount; auto using a64_range.
-    apply Int.ltu_inv in L2. omega. }
+    apply Int.ltu_inv in L2. lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
   simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto.
 * assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true).
   { apply sub_shift_amount; auto using a64_range.
-    unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
+    unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
   simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto.
@@ -261,11 +261,11 @@ Local Opaque Int64.zwordsize.
 * econstructor; split. EvalOp. rewrite mk_amount64_eq by auto.
   destruct v1; simpl; auto. rewrite ! L; simpl.
   set (s' := s - Int.unsigned n).
-  replace s with (s' + Int.unsigned n) by (unfold s'; omega).
-  rewrite Int64.shru'_zero_ext. auto. unfold s'; omega.
+  replace s with (s' + Int.unsigned n) by (unfold s'; lia).
+  rewrite Int64.shru'_zero_ext. auto. unfold s'; lia.
 * econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite ! L; simpl.
-  rewrite Int64.shru'_zero_ext_0 by omega. auto. 
+  rewrite Int64.shru'_zero_ext_0 by lia. auto. 
 + econstructor; eauto using eval_shrluimm_base.
 - intros; TrivialExists.
 Qed.
@@ -290,13 +290,13 @@ Proof.
 + destruct (Int.ltu n a) eqn:L2.
 * assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true).
   { apply sub_shift_amount; auto using a64_range.
-    apply Int.ltu_inv in L2. omega. }
+    apply Int.ltu_inv in L2. lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
   simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto.
 * assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true).
   { apply sub_shift_amount; auto using a64_range.
-    unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
+    unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
   simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto.
@@ -309,8 +309,8 @@ Proof.
 * InvBooleans. econstructor; split. EvalOp. rewrite mk_amount64_eq by auto.
   destruct v1; simpl; auto. rewrite ! L; simpl.
   set (s' := s - Int.unsigned n).
-  replace s with (s' + Int.unsigned n) by (unfold s'; omega).
-  rewrite Int64.shr'_sign_ext. auto. unfold s'; omega. unfold s'; omega.
+  replace s with (s' + Int.unsigned n) by (unfold s'; lia).
+  rewrite Int64.shr'_sign_ext. auto. unfold s'; lia. unfold s'; lia.
 * econstructor; split; [|eauto]. apply eval_shrlimm_base; auto. EvalOp.
 + econstructor; eauto using eval_shrlimm_base.
 - intros; TrivialExists.
@@ -392,7 +392,7 @@ Proof.
 - TrivialExists.
 - destruct (zlt (Int.unsigned a0) sz).
 + econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a64_range; simpl.
-  apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by omega. f_equal. omega.
+  apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by lia. f_equal. lia.
 + TrivialExists.
 - TrivialExists.
 Qed.
diff --git a/aarch64/SelectOpproof.v b/aarch64/SelectOpproof.v
index 625a0c14..ccc4c0f1 100644
--- a/aarch64/SelectOpproof.v
+++ b/aarch64/SelectOpproof.v
@@ -243,8 +243,8 @@ Remark sub_shift_amount:
 Proof.
   intros. unfold Int.ltu; apply zlt_true. rewrite Int.unsigned_repr_wordsize.
   apply Int.ltu_iwordsize_inv in H. apply Int.ltu_iwordsize_inv in H0.
-  unfold Int.sub; rewrite Int.unsigned_repr. omega.
-  generalize Int.wordsize_max_unsigned; omega.
+  unfold Int.sub; rewrite Int.unsigned_repr. lia.
+  generalize Int.wordsize_max_unsigned; lia.
 Qed.
 
 Theorem eval_shruimm:
@@ -260,13 +260,13 @@ Local Opaque Int.zwordsize.
 + destruct (Int.ltu n a) eqn:L2.
 * assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true).
   { apply sub_shift_amount; auto using a32_range.
-    apply Int.ltu_inv in L2. omega. }
+    apply Int.ltu_inv in L2. lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
   simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto.
 * assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true).
   { apply sub_shift_amount; auto using a32_range.
-    unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
+    unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
   simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto.
@@ -279,11 +279,11 @@ Local Opaque Int.zwordsize.
 * econstructor; split. EvalOp. rewrite mk_amount32_eq by auto.
   destruct v1; simpl; auto. rewrite ! L; simpl.
   set (s' := s - Int.unsigned n).
-  replace s with (s' + Int.unsigned n) by (unfold s'; omega).
-  rewrite Int.shru_zero_ext. auto. unfold s'; omega.
+  replace s with (s' + Int.unsigned n) by (unfold s'; lia).
+  rewrite Int.shru_zero_ext. auto. unfold s'; lia.
 * econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite ! L; simpl.
-  rewrite Int.shru_zero_ext_0 by omega. auto. 
+  rewrite Int.shru_zero_ext_0 by lia. auto. 
 + econstructor; eauto using eval_shruimm_base.
 - intros; TrivialExists.
 Qed.
@@ -308,13 +308,13 @@ Proof.
 + destruct (Int.ltu n a) eqn:L2.
 * assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true).
   { apply sub_shift_amount; auto using a32_range.
-    apply Int.ltu_inv in L2. omega. }
+    apply Int.ltu_inv in L2. lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
   simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto.
 * assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true).
   { apply sub_shift_amount; auto using a32_range.
-    unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
+    unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
   econstructor; split. EvalOp.
   destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
   simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto.
@@ -327,8 +327,8 @@ Proof.
 * InvBooleans. econstructor; split. EvalOp. rewrite mk_amount32_eq by auto.
   destruct v1; simpl; auto. rewrite ! L; simpl.
   set (s' := s - Int.unsigned n).
-  replace s with (s' + Int.unsigned n) by (unfold s'; omega).
-  rewrite Int.shr_sign_ext. auto. unfold s'; omega. unfold s'; omega.
+  replace s with (s' + Int.unsigned n) by (unfold s'; lia).
+  rewrite Int.shr_sign_ext. auto. unfold s'; lia. unfold s'; lia.
 * econstructor; split; [|eauto]. apply eval_shrimm_base; auto. EvalOp.
 + econstructor; eauto using eval_shrimm_base. 
 - intros; TrivialExists.
@@ -399,20 +399,20 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
-  unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
-  assert (N1: 0 <= n < 64) by omega.
+  assert (N1: 0 <= n < 64) by lia.
   rewrite Int64.bits_loword by auto.
   rewrite Int64.bits_shr' by auto.
   change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
-  rewrite zlt_true by omega.
+  rewrite zlt_true by lia.
   rewrite Int.testbit_repr by auto. 
-  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
   transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)).
-  rewrite Z.shiftr_spec by omega. auto.
+  rewrite Z.shiftr_spec by lia. auto.
   apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
-  change Int64.zwordsize with 64; omega.
+  change Int64.zwordsize with 64; lia.
 Qed.
 
 Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
@@ -425,20 +425,20 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
-  unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
-  assert (N1: 0 <= n < 64) by omega.
+  assert (N1: 0 <= n < 64) by lia.
   rewrite Int64.bits_loword by auto.
   rewrite Int64.bits_shru' by auto.
   change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
-  rewrite zlt_true by omega.
+  rewrite zlt_true by lia.
   rewrite Int.testbit_repr by auto. 
-  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
+  unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
   transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)).
-  rewrite Z.shiftr_spec by omega. auto.
+  rewrite Z.shiftr_spec by lia. auto.
   apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. 
-  change Int64.zwordsize with 64; omega.
+  change Int64.zwordsize with 64; lia.
 Qed.
 
 (** Integer conversions *)
@@ -451,7 +451,7 @@ Proof.
 - TrivialExists.
 - destruct (zlt (Int.unsigned a0) sz).
 + econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a32_range; simpl.
-  apply Val.lessdef_same. f_equal. rewrite Int.shl_zero_ext by omega. f_equal. omega.
+  apply Val.lessdef_same. f_equal. rewrite Int.shl_zero_ext by lia. f_equal. lia.
 + TrivialExists.
 - TrivialExists.
 Qed.
@@ -464,29 +464,29 @@ Proof.
 - TrivialExists.
 - destruct (zlt (Int.unsigned a0) sz).
 + econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a32_range; simpl.
-  apply Val.lessdef_same. f_equal. rewrite Int.shl_sign_ext by omega. f_equal. omega.
+  apply Val.lessdef_same. f_equal. rewrite Int.shl_sign_ext by lia. f_equal. lia.
 + TrivialExists.
 - TrivialExists.
 Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
-  apply eval_sign_ext; omega. 
+  apply eval_sign_ext; lia. 
 Qed.
 
 Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
 Proof.
-  apply eval_zero_ext; omega.
+  apply eval_zero_ext; lia.
 Qed.
 
 Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
 Proof.
-  apply eval_sign_ext; omega. 
+  apply eval_sign_ext; lia. 
 Qed.
 
 Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
 Proof.
-  apply eval_zero_ext; omega.
+  apply eval_zero_ext; lia.
 Qed.
 
 (** Bitwise not, and, or, xor *)
diff --git a/aarch64/Stacklayout.v b/aarch64/Stacklayout.v
index 86ba9f45..cdbc64d5 100644
--- a/aarch64/Stacklayout.v
+++ b/aarch64/Stacklayout.v
@@ -67,13 +67,13 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   change (size_chunk Mptr) with 8.
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + 8 <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + 8 <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + 8 <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + 8 <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -86,11 +86,11 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap45.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split_2. fold olink; omega. omega.
-  apply range_split. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol. omega. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_split_2. fold olink; lia. lia.
+  apply range_split. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol. lia. lia.
+  apply range_drop_right with ostkdata. lia.
   eapply sep_drop2. eexact H.
 Qed.
 
@@ -106,14 +106,14 @@ Proof.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + 8 <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + 8 <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + 8 <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + 8 <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
-  split. omega. apply align_le. omega. 
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
+  split. lia. apply align_le. lia. 
 Qed.
 
 Lemma frame_env_aligned:
@@ -133,8 +133,8 @@ Proof.
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   change (align_chunk Mptr) with 8.
   split. apply Z.divide_0_r.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl.
 Qed.