From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 21 Jun 2020 18:22:00 +0200
Subject: 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`.
---
 backend/RTL.v | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

(limited to 'backend/RTL.v')

diff --git a/backend/RTL.v b/backend/RTL.v
index 9599a24a..a022f55a 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -352,7 +352,7 @@ Proof.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]].
   exists (Returnstate s0 vres2 m2). econstructor; eauto.
 (* trace length *)
-  red; intros; inv H; simpl; try omega.
+  red; intros; inv H; simpl; try lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
@@ -450,8 +450,8 @@ Proof.
   rewrite PTree.gempty. congruence.
   (* inductive case *)
   intros. rewrite PTree.gsspec in H2. destruct (peq pc k).
-  inv H2. xomega.
-  apply Ple_trans with a. auto. xomega.
+  inv H2. extlia.
+  apply Ple_trans with a. auto. extlia.
 Qed.
 
 (** Maximum pseudo-register mentioned in a function.  All results or arguments
@@ -489,9 +489,9 @@ Proof.
   assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     auto.
-    apply IHl. xomega. }
-  destruct i; simpl; try (destruct s0); repeat (apply X); try xomega.
-  destruct o; xomega.
+    apply IHl. extlia. }
+  destruct i; simpl; try (destruct s0); repeat (apply X); try extlia.
+  destruct o; extlia.
 Qed.
 
 Remark max_reg_instr_def:
@@ -499,12 +499,12 @@ Remark max_reg_instr_def:
 Proof.
   intros.
   assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)).
-  { induction l; simpl; intros. xomega. apply IHl. xomega. }
+  { induction l; simpl; intros. extlia. apply IHl. extlia. }
   destruct i; simpl in *; inv H.
-- apply X. xomega.
-- apply X. xomega.
-- destruct s0; apply X; xomega.
-- destruct b; inv H1. apply X. simpl. xomega.
+- apply X. extlia.
+- apply X. extlia.
+- destruct s0; apply X; extlia.
+- destruct b; inv H1. apply X. simpl. extlia.
 Qed.
 
 Remark max_reg_instr_uses:
@@ -514,14 +514,14 @@ Proof.
   assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     tauto.
-    apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
+    apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. }
   destruct i; simpl in *; try (destruct s0); try (apply X; auto).
 - contradiction.
-- destruct H. right; subst; xomega. auto.
-- destruct H. right; subst; xomega. auto.
-- destruct H. right; subst; xomega. auto.
-- intuition. subst; xomega.
-- destruct o; simpl in H; intuition. subst; xomega.
+- destruct H. right; subst; extlia. auto.
+- destruct H. right; subst; extlia. auto.
+- destruct H. right; subst; extlia. auto.
+- intuition. subst; extlia.
+- destruct o; simpl in H; intuition. subst; extlia.
 Qed.
 
 Lemma max_reg_function_def:
@@ -539,7 +539,7 @@ Proof.
      + inv H3. eapply max_reg_instr_def; eauto.
      + apply Ple_trans with a. auto. apply max_reg_instr_ge.
   }
-  unfold max_reg_function. xomega.
+  unfold max_reg_function. extlia.
 Qed.
 
 Lemma max_reg_function_use:
@@ -557,7 +557,7 @@ Proof.
      + inv H3. eapply max_reg_instr_uses; eauto.
      + apply Ple_trans with a. auto. apply max_reg_instr_ge.
   }
-  unfold max_reg_function. xomega.
+  unfold max_reg_function. extlia.
 Qed.
 
 Lemma max_reg_function_params:
@@ -567,8 +567,8 @@ Proof.
   assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     tauto.
-    apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
+    apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. }
   assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)).
   { apply X; auto. }
-  unfold max_reg_function. xomega.
+  unfold max_reg_function. extlia.
 Qed.
-- 
cgit