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, 18 insertions, 18 deletions

diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 272b929f..10ccbeff 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -561,7 +561,7 @@ Local Opaque sizeof.
 + destruct (zeq sz 0). 
   inv TR. exists (@nil init_data); split; auto. constructor.
   destruct (zle 0 sz).
-  inv TR. econstructor; split. constructor. omega. auto.
+  inv TR. econstructor; split. constructor. lia. auto.
   discriminate.
 + monadInv TR. 
   destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1).
@@ -672,8 +672,8 @@ Remark padding_size:
   forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.
 Proof.
   unfold tr_padding; intros. destruct (zlt frm to).
-  simpl. xomega.
-  simpl. omega.
+  simpl. extlia.
+  simpl. lia.
 Qed.
 
 Remark idlsize_app:
@@ -681,7 +681,7 @@ Remark idlsize_app:
 Proof.
   induction d1; simpl; intros.
   auto.
-  rewrite IHd1. omega.
+  rewrite IHd1. lia.
 Qed.
 
 Remark union_field_size:
@@ -690,8 +690,8 @@ Proof.
   induction fl as [|[i t]]; simpl; intros.
 - inv H.
 - destruct (ident_eq f i).
-  + inv H. xomega.
-  + specialize (IHfl H). xomega.
+  + inv H. extlia.
+  + specialize (IHfl H). extlia.
 Qed.
 
 Hypothesis ce_consistent: composite_env_consistent ge.
@@ -712,16 +712,16 @@ with tr_init_struct_size:
 Proof.
 Local Opaque sizeof.
 - destruct 1; simpl.
-+ erewrite transl_init_single_size by eauto. omega.
++ erewrite transl_init_single_size by eauto. lia.
 + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. 
-+ replace (idlsize d) with (idlsize d + 0) by omega.
++ replace (idlsize d) with (idlsize d + 0) by lia.
   eapply tr_init_struct_size; eauto. simpl.
   unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
   erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
   unfold sizeof_composite. rewrite H0. apply align_le.
   destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 + rewrite idlsize_app, padding_size. 
-  exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega.
+  exploit tr_init_size; eauto. intros EQ; rewrite EQ. lia.
   simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
   apply Z.le_trans with (sizeof_union ge (co_members co)).
   eapply union_field_size; eauto.
@@ -730,21 +730,21 @@ Local Opaque sizeof.
   destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
 
 - destruct 1; simpl.
-+ omega.
++ lia.
 + rewrite Z.mul_comm.
   assert (0 <= sizeof ge ty * sz).
-  { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. }
-  xomega.
+  { apply Zmult_gt_0_le_0_compat. lia. generalize (sizeof_pos ge ty); lia. }
+  extlia.
 + rewrite idlsize_app. 
   erewrite tr_init_size by eauto. 
   erewrite tr_init_array_size by eauto.
   ring.
 
 - destruct 1; simpl; intros.
-+ rewrite padding_size by auto. omega.
++ rewrite padding_size by auto. lia.
 + rewrite ! idlsize_app, padding_size. 
   erewrite tr_init_size by eauto. 
-  rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega.
+  rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). lia.
   unfold pos1. apply align_le. apply alignof_pos. 
 Qed.
 
@@ -806,7 +806,7 @@ Remark exec_init_array_length:
   forall m b ofs ty sz il m',
   exec_init_array m b ofs ty sz il m' -> sz >= 0.
 Proof.
-  induction 1; omega.
+  induction 1; lia.
 Qed.
 
 Lemma store_init_data_list_app:
@@ -847,10 +847,10 @@ Local Opaque sizeof.
   inv H3. simpl. erewrite transl_init_single_steps by eauto. auto.
 - (* array *)
   inv H1. replace (Z.max 0 sz) with sz in H7. eauto.
-  assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega.
+  assert (sz >= 0) by (eapply exec_init_array_length; eauto). extlia.
 - (* struct *)
   inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. 
-  replace ofs with (ofs + 0) by omega. eauto.
+  replace ofs with (ofs + 0) by lia. eauto.
 - (* union *)
   inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. 
   eapply store_init_data_list_app. eauto.
@@ -870,7 +870,7 @@ Local Opaque sizeof.
   inv H4. simpl in H3; inv H3. 
   eapply store_init_data_list_app. apply store_init_data_list_padding.
   rewrite padding_size.
-  replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega.
+  replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by lia.
   eapply store_init_data_list_app.
   eauto.
   rewrite (tr_init_size _ _ _ H9).