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

diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index c235031f..30e5c2ae 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -1553,13 +1553,13 @@ Proof.
   exploit external_call_trace_length; eauto. destruct t1; simpl; intros.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   econstructor; econstructor. left; eapply step_builtin; eauto.
-  omegaContradiction.
+  extlia.
   (* external calls *)
   inv H1.
   exploit external_call_trace_length; eauto. destruct t1; simpl; intros.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   exists (Returnstate vres2 k m2); exists E0; right; econstructor; eauto.
-  omegaContradiction.
+  extlia.
 (* well-behaved traces *)
   red; intros. inv H; inv H0; simpl; auto.
   (* valof volatile *)
@@ -1582,10 +1582,10 @@ Proof.
   exploit deref_loc_trace; eauto. destruct t; auto. destruct t; tauto.
   (* builtins *)
   exploit external_call_trace_length; eauto.
-  destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
+  destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia.
   (* external calls *)
   exploit external_call_trace_length; eauto.
-  destruct t; simpl; auto. destruct t; simpl; auto. intros; omegaContradiction.
+  destruct t; simpl; auto. destruct t; simpl; auto. intros; extlia.
 Qed.
 
 (** The main simulation result. *)
@@ -2734,7 +2734,7 @@ Proof.
   cofix COEL.
   intros. inv H.
 (* cons left *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)).
   eauto. eapply leftcontext_compose; eauto. constructor. auto.
   apply exprlist_app_leftcontext; auto. traceEq.
@@ -2745,7 +2745,7 @@ Proof.
   eapply leftcontext_compose; eauto. repeat constructor. auto.
   apply exprlist_app_leftcontext; auto.
   eapply forever_N_star with (a2 := (esizelist al0)).
-  eexact R. simpl; omega.
+  eexact R. simpl; lia.
   change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0).
   rewrite <- exprlist_app_assoc.
   eapply COEL. eauto. auto. auto.
@@ -2754,42 +2754,42 @@ Proof.
 
   intros. inv H.
 (* field *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Efield x f0 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* valof *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Evalof x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* deref *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ederef x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* addrof *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eaddrof x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* unop *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eunop op x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* binop left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* binop right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ebinop op x a2 ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia.
   eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq.
 (* cast *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecast x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqand left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eseqand x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqand 2 *)
@@ -2802,7 +2802,7 @@ Proof.
   eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqor left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eseqor x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* seqor 2 *)
@@ -2815,7 +2815,7 @@ Proof.
   eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* condition top *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* condition *)
@@ -2828,33 +2828,33 @@ Proof.
   eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assign left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assign right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassign x a2 ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia.
   eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq.
 (* assignop left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* assignop right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassignop op x a2 tyres ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; lia.
   eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq.
 (* postincr *)
-  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Epostincr id x ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* comma left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* comma right *)
@@ -2865,14 +2865,14 @@ Proof.
   left; eapply step_comma; eauto. reflexivity.
   eapply COE with (C := C); eauto. traceEq.
 (* call left *)
-  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega.
+  eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; lia.
   eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto.
   eapply leftcontext_compose; eauto. repeat constructor. traceEq.
 (* call right *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x a2 ty)) f k)
   as [P [Q R]].
   eapply leftcontext_compose; eauto. repeat constructor.
-  eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega.
+  eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; lia.
   eapply COEL with (al := Enil). eauto. auto. auto. auto. traceEq.
 (* call *)
   destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k)