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`.

7 files changed, 60 insertions, 60 deletions

diff --git a/x86/Asm.v b/x86/Asm.v
index 33f1f2ad..799b533e 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -1193,7 +1193,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/x86/Asmgenproof.v b/x86/Asmgenproof.v
index f1fd41e3..67c42b2b 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -67,7 +67,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); monadInv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma exec_straight_exec:
@@ -332,8 +332,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.
 
@@ -852,7 +852,7 @@ Transparent destroyed_by_jumptable.
   econstructor; eauto.
   unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen.
   rewrite ATPC. simpl. constructor; eauto.
-  unfold fn_code. eapply code_tail_next_int. simpl in g. omega.
+  unfold fn_code. eapply code_tail_next_int. simpl in g. lia.
   constructor.
   apply agree_nextinstr. eapply agree_change_sp; eauto.
 Transparent destroyed_at_function_entry.
@@ -877,7 +877,7 @@ Transparent destroyed_at_function_entry.
 
 - (* return *)
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   econstructor; eauto. rewrite ATPC; eauto. congruence.
 Qed.
 
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 82179fa4..09c6e91b 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -532,7 +532,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/x86/Conventions1.v b/x86/Conventions1.v
index 645aae90..803d162a 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -302,14 +302,14 @@ Remark loc_arguments_32_charact:
   In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros.
 - contradiction.
 - destruct H.
-+ destruct ty; subst p; simpl; omega.
++ destruct ty; subst p; simpl; lia.
 + apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *.
-* eapply X; eauto; omega.
-* destruct H; split; eapply X; eauto; omega.
+* eapply X; eauto; lia.
+* destruct H; split; eapply X; eauto; lia.
 Qed.
 
 Remark loc_arguments_elf64_charact:
@@ -317,7 +317,7 @@ Remark loc_arguments_elf64_charact:
   In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
   assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
@@ -334,8 +334,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1.
     subst. left. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   assert (B: forall ty, In p
       match list_nth_z float_param_regs_elf64 fr with
       | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs
@@ -345,8 +345,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1.
     subst. right. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   destruct a; eauto.
 Qed.
 
@@ -355,7 +355,7 @@ Remark loc_arguments_win64_charact:
   In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p.
 Proof.
   assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l).
-  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. }
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
   assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
@@ -372,8 +372,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1.
     subst. left. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   assert (B: forall ty, In p
       match list_nth_z float_param_regs_win64 r with
       | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs
@@ -383,8 +383,8 @@ Opaque list_nth_z.
   { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1.
     subst. right. eapply list_nth_z_in; eauto.
     eapply IHtyl; eauto.
-    subst. split. omega. assumption.
-    eapply Y; eauto. omega. }
+    subst. split. lia. assumption.
+    eapply Y; eauto. lia. }
   destruct a; eauto.
 Qed.
 
diff --git a/x86/NeedOp.v b/x86/NeedOp.v
index d9a58fbb..775a23db 100644
--- a/x86/NeedOp.v
+++ b/x86/NeedOp.v
@@ -206,9 +206,9 @@ Proof.
   unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
   simpl in *; FuncInv; InvAgree; TrivialExists.
 - apply sign_ext_sound; auto. compute; auto.
-- apply zero_ext_sound; auto. omega.
+- apply zero_ext_sound; auto. lia.
 - apply sign_ext_sound; auto. compute; auto.
-- apply zero_ext_sound; auto. omega.
+- apply zero_ext_sound; auto. lia.
 - apply neg_sound; auto.
 - apply mul_sound; auto.
 - apply mul_sound; auto with na.
@@ -246,10 +246,10 @@ Lemma operation_is_redundant_sound:
   vagree v arg1' nv.
 Proof.
   intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply zero_ext_redundant_sound; auto. omega.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply zero_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply zero_ext_redundant_sound; auto. lia.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply zero_ext_redundant_sound; auto. lia.
 - apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 961f602c..d8ab32a4 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -381,9 +381,9 @@ Proof.
 - TrivialExists. simpl. rewrite Int.and_commut; auto.
 - TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto.
 - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
-  rewrite Int.and_commut. auto. omega.
+  rewrite Int.and_commut. auto. lia.
 - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
-  rewrite Int.and_commut. auto. omega.
+  rewrite Int.and_commut. auto. lia.
 - TrivialExists.
 Qed.
 
@@ -743,7 +743,7 @@ Proof.
   red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval.
   TrivialExists.
   subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
-  rewrite Int.and_commut. apply eval_andimm; auto. omega.
+  rewrite Int.and_commut. apply eval_andimm; auto. lia.
   TrivialExists.
 Qed.
 
@@ -759,7 +759,7 @@ Proof.
   red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
   TrivialExists.
   subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
-  rewrite Int.and_commut. apply eval_andimm; auto. omega.
+  rewrite Int.and_commut. apply eval_andimm; auto. lia.
   TrivialExists.
 Qed.
 
@@ -860,7 +860,7 @@ Proof.
   simpl. rewrite Heqo; reflexivity.
   simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned; auto.
   assert (Int.modulus < Int64.max_unsigned) by reflexivity. 
-  generalize (Int.unsigned_range n); omega.
+  generalize (Int.unsigned_range n); lia.
 Qed.
 
 Theorem eval_floatofintu:
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v
index 4f68cf26..002b86bf 100644
--- a/x86/Stacklayout.v
+++ b/x86/Stacklayout.v
@@ -69,16 +69,16 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
   replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; omega).
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= 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 (ostkdata + bound_stack_data b <= oretaddr) 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).
+  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -90,13 +90,13 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap45.
   rewrite sep_swap34.
 (* Apply range_split and range_split2 repeatedly *)
-  apply range_drop_left with 0. omega. 
-  apply range_split_2. fold olink. omega. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol. omega. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_drop_left with 0. lia. 
+  apply range_split_2. fold olink. lia. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol. lia. lia.
+  apply range_drop_right with ostkdata. lia.
   rewrite sep_swap.
-  apply range_drop_left with (ostkdata + bound_stack_data b). omega.
+  apply range_drop_left with (ostkdata + bound_stack_data b). lia.
   rewrite sep_swap.
   exact H.
 Qed.
@@ -113,17 +113,17 @@ Proof.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; omega).
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= 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 (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
-  split. omega. 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).
+  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; lia).
+  split. lia. lia.
 Qed.
 
 Lemma frame_env_aligned:
@@ -142,11 +142,11 @@ Proof.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
   split. exists (fe_ofs_arg / 8). unfold fe_ofs_arg; destruct Archi.win64; reflexivity.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  apply align_divides; omega.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  apply align_divides; lia.
 Qed.