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

1 files changed, 31 insertions, 31 deletions

diff --git a/common/Memdata.v b/common/Memdata.v
index f3016efe..05a3d4ed 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -47,7 +47,7 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
 Lemma size_chunk_pos:
   forall chunk, size_chunk chunk > 0.
 Proof.
-  intros. destruct chunk; simpl; omega.
+  intros. destruct chunk; simpl; lia.
 Qed.
 
 Definition size_chunk_nat (chunk: memory_chunk) : nat :=
@@ -65,7 +65,7 @@ Proof.
   intros.
   generalize (size_chunk_pos chunk). rewrite size_chunk_conv.
   destruct (size_chunk_nat chunk).
-  simpl; intros; omegaContradiction.
+  simpl; intros; extlia.
   intros; exists n; auto.
 Qed.
 
@@ -101,7 +101,7 @@ Definition align_chunk (chunk: memory_chunk) : Z :=
 Lemma align_chunk_pos:
   forall chunk, align_chunk chunk > 0.
 Proof.
-  intro. destruct chunk; simpl; omega.
+  intro. destruct chunk; simpl; lia.
 Qed.
 
 Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4.
@@ -120,7 +120,7 @@ Lemma align_le_divides:
   align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2).
 Proof.
   intros. destruct chunk1; destruct chunk2; simpl in *;
-  solve [ omegaContradiction
+  solve [ extlia
         | apply Z.divide_refl
         | exists 2; reflexivity
         | exists 4; reflexivity
@@ -216,12 +216,12 @@ Proof.
   simpl. rewrite Zmod_1_r. auto.
 Opaque Byte.wordsize.
   rewrite Nat2Z.inj_succ. simpl.
-  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega.
-  rewrite two_p_is_exp; try omega.
+  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia.
+  rewrite two_p_is_exp; try lia.
   rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm.
   change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x).
   rewrite Byte.Z_mod_modulus_eq. reflexivity.
-  apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. lia. apply two_p_gt_ZERO. lia.
 Qed.
 
 Lemma rev_if_be_involutive:
@@ -280,15 +280,15 @@ Proof.
   intros; simpl; auto.
   intros until y.
   rewrite Nat2Z.inj_succ.
-  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega.
-  rewrite two_p_is_exp; try omega.
+  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia.
+  rewrite two_p_is_exp; try lia.
   intro EQM.
   simpl; decEq.
   apply Byte.eqm_samerepr. red.
   eapply eqmod_divides; eauto. apply Z.divide_factor_r.
   apply IHn.
   destruct EQM as [k EQ]. exists k. rewrite EQ.
-  rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega.
+  rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. lia.
 Qed.
 
 Lemma encode_int_8_mod:
@@ -517,9 +517,9 @@ Ltac solve_decode_encode_val_general :=
   | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2
   | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4
   | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8
-  | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega
-  | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega
-  | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega
+  | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; lia
+  | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; lia
+  | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; lia
   end.
 
 Lemma decode_encode_val_general:
@@ -543,7 +543,7 @@ Lemma decode_encode_val_similar:
   v2 = Val.load_result chunk2 v1.
 Proof.
   intros until v2; intros TY SZ DE.
-  destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction;
+  destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try extlia;
   destruct v1; auto.
 Qed.
 
@@ -553,7 +553,7 @@ Lemma decode_val_rettype:
 Proof.
   intros. unfold decode_val.
   destruct (proj_bytes cl).
-- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto.
+- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by lia; auto.
 - Local Opaque Val.load_result.
   destruct chunk; simpl;
   (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)).
@@ -653,7 +653,7 @@ Proof.
              exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q).
   {
     induction n; simpl; intros. contradiction. destruct H0.
-    exists n; split; auto. omega. apply IHn; auto. omega.
+    exists n; split; auto. lia. apply IHn; auto. lia.
   }
   assert (B: forall q,
              q = quantity_chunk chunk ->
@@ -663,7 +663,7 @@ Proof.
 Local Transparent inj_value.
     intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ'].
     rewrite EQ'. simpl. constructor; auto.
-    intros; eapply A; eauto. omega.
+    intros; eapply A; eauto. lia.
   }
   assert (C: forall bl,
              match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end ->
@@ -719,8 +719,8 @@ Proof.
     induction n; destruct mvs; simpl; intros; try discriminate.
     contradiction.
     destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst.
-    destruct H0. subst mv. exists n0; split; auto. omega.
-    eapply IHn; eauto. omega.
+    destruct H0. subst mv. exists n0; split; auto. lia.
+    eapply IHn; eauto. lia.
   }
   assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)).
   {
@@ -740,7 +740,7 @@ Proof.
     simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto.
     destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate.
     congruence.
-    intros. eapply B; eauto. omega.
+    intros. eapply B; eauto. lia.
   }
   unfold decode_val.
   destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB.
@@ -955,22 +955,22 @@ Proof.
   induction l1; simpl int_of_bytes; intros.
   simpl. ring.
   simpl length. rewrite Nat2Z.inj_succ.
-  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega.
+  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by lia.
   rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring.
-  omega. omega.
+  lia. lia.
 Qed.
 
 Lemma int_of_bytes_range:
   forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8).
 Proof.
   induction l; intros.
-  simpl. omega.
+  simpl. lia.
   simpl length. rewrite Nat2Z.inj_succ.
-  replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega.
+  replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by lia.
   rewrite two_p_is_exp. change (two_p 8) with 256.
   simpl int_of_bytes. generalize (Byte.unsigned_range a).
-  change Byte.modulus with 256. omega.
-  omega. omega.
+  change Byte.modulus with 256. lia.
+  lia. lia.
 Qed.
 
 Lemma length_proj_bytes:
@@ -1014,7 +1014,7 @@ Proof.
     intros. apply Int.unsigned_repr.
     generalize (int_of_bytes_range l). rewrite H2.
     change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1).
-    omega.
+    lia.
   apply Val.lessdef_same.
   unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2.
   + rewrite <- (rev_length b1) in L1.
@@ -1036,18 +1036,18 @@ Lemma bytes_of_int_append:
   bytes_of_int n1 x1 ++ bytes_of_int n2 x2.
 Proof.
   induction n1; intros.
-- simpl in *. f_equal. omega.
+- simpl in *. f_equal. lia.
 - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256).
   {
     rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp.
-    f_equal. omega. omega. omega.
+    f_equal. lia. lia. lia.
   }
   rewrite E in *. simpl. f_equal.
   apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)).
   change Byte.modulus with 256. ring.
   rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1.
-  apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega.
-  assumption. omega.
+  apply Zdiv_interval_1. lia. apply two_p_gt_ZERO; lia. lia.
+  assumption. lia.
 Qed.
 
 Lemma bytes_of_int64: