Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

4 files changed, 43 insertions, 39 deletions

diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index 2f73f1fa..a4fce97e 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -26,6 +26,7 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL Linking.
+Require Import Lia.
 
 Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
          (at level 200, X ident, A at level 100, B at level 200)
@@ -582,8 +583,8 @@ Lemma wellformed_suffix_path c pm path path':
    exists pc', nth_default_succ c (path-path') pc = Some pc' /\ wellformed_path c pm path' pc'.
 Proof.
   induction 1 as [|m].
-  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|omega].
-  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|omega].
+  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|lia].
+  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|lia].
     inversion WF; subst; clear WF; intros; simplify_someHyps.
     intros; simplify_someHyps; eauto.
 Qed.
@@ -600,9 +601,9 @@ Proof.
   intros; exploit fn_path_wf; eauto.
   intro WF.
   set (ps:=path.(psize)).
-  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); omega || eauto.
+  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); lia || eauto.
   destruct 1 as (pc' & NTH_SUCC & WF'); auto.
-  assert (ps - 0 = ps)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH.
+  assert (ps - 0 = ps)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
   unfold nth_default_succ_inst.
   inversion WF'; clear WF'; subst. simplify_someHyps; eauto.
 Qed.
@@ -617,11 +618,11 @@ Lemma internal_node_path path f path0 pc:
 Proof.
   intros; exploit fn_path_wf; eauto.
   set (ps:=path0.(psize)).
-  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { omega. }
+  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { lia. }
   destruct 1 as (pc' & NTH_SUCC & WF').
-  assert (ps - (ps - path) = path)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH.
+  assert (ps - (ps - path) = path)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
   unfold nth_default_succ_inst. 
-  inversion WF'; clear WF'; subst. { omega. }
+  inversion WF'; clear WF'; subst. { lia. }
   simplify_someHyps; eauto.
 Qed.
 
@@ -706,7 +707,7 @@ Proof.
       rewrite CONT. auto.
     + intros; try_simplify_someHyps; try congruence.
       eexists. exists i. exists O; simpl. intuition eauto.
-      omega.
+      lia.
 Qed.
 
 Lemma isteps_resize ge path0 path1 f sp rs m pc st: 
@@ -837,15 +838,15 @@ Lemma stuttering path idx stack f sp rs m pc st t s1':
    RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' ->
    t = E0 /\ match_inst_states idx s1' (State stack f sp pc rs m).
 Proof.
-  intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); omega || eauto.
+  intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); lia || eauto.
   intros (i & pc' & Hi & Hpc & DUM).
   unfold nth_default_succ_inst in Hi.
   erewrite isteps_normal_exit in Hi; eauto.
   exploit istep_complete; congruence || eauto.
   intros (SILENT & st0 & STEP0 & EQ).
   intuition; subst; unfold match_inst_states; simpl.
-  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; omega || eauto.
-  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try omega.
+  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; lia || eauto.
+  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try lia.
   erewrite <- isteps_step_right; eauto.
 Qed.
 
@@ -874,7 +875,7 @@ Proof.
     destruct (initialize_path (*fn_code f*) (fn_path f) (ipc st0)) as (path0 & Hpath0); eauto.
     exists (path0.(psize)); intuition eauto.
     econstructor; eauto.
-    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
     * simpl; eauto.
   + generalize Hi; inversion RSTEP; clear RSTEP; subst; (repeat (simplify_someHyp; simpl in * |- * )); try congruence; eauto.
     - (* Icall *)
@@ -897,7 +898,7 @@ Proof.
       destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
       exists path0.(psize); intuition eauto.
       econstructor; eauto.
-      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
       * simpl; eauto.
    - (* Ijumptable *)
       intros; exploit exec_Ijumptable; eauto.
@@ -906,7 +907,7 @@ Proof.
       destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
       exists path0.(psize); intuition eauto.
       econstructor; eauto.
-      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
       * simpl; eauto.
   - (* Ireturn *)
       intros; exploit exec_Ireturn; eauto.
@@ -933,7 +934,7 @@ Proof.
   intros PSTEP PATH BOUND RSTEP WF; destruct (st.(icontinue)) eqn: CONT.
   destruct idx as [ | idx].
   + (* path_step on normal_exit *)
-     assert (path.(psize)-0=path.(psize))%nat as HH by omega. rewrite HH in PSTEP. clear HH.
+     assert (path.(psize)-0=path.(psize))%nat as HH by lia. rewrite HH in PSTEP. clear HH.
      exploit normal_exit; eauto.
      intros (s2' & LSTEP & (idx' & MATCH)).
      exists idx'; exists s2'; intuition eauto.
@@ -942,7 +943,7 @@ Proof.
     unfold match_states; exists idx; exists (State stack f sp pc rs m); 
     intuition.
   + (* one or two path_step on early_exit *)
-    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try omega.
+    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try lia.
     clear PSTEP; intros PSTEP.
     (* TODO for clarification: move the assert below into a separate lemma *)
     assert (HPATH0: exists path0, (fn_path f)!(ipc st) = Some path0).
@@ -952,7 +953,7 @@ Proof.
       exploit istep_early_exit; eauto.
       intros (X1 & X2 & EARLY_EXIT).
       destruct st as [cont pc0 rs0 m0]; simpl in * |- *; intuition subst.
-      exploit (internal_node_path path0); omega || eauto.
+      exploit (internal_node_path path0); lia || eauto.
       intros (i' & pc' & Hi' & Hpc' & ENTRY).
       unfold nth_default_succ_inst in Hi'.
       erewrite isteps_normal_exit in Hi'; eauto.
@@ -974,8 +975,8 @@ Proof.
       - simpl; eauto.
     * (* single step case *)
       exploit (stuttering path1 ps stack f sp (irs st) (imem st) (ipc st)); simpl; auto.
-      - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try omega.  simpl; eauto. }
-      - omega.
+      - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try lia.  simpl; eauto. }
+      - lia.
       - simpl; eauto.
       - simpl; eauto.
       - intuition subst.
@@ -1000,7 +1001,7 @@ Proof.
       exists path.(psize). constructor; auto.
       econstructor; eauto.
       - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
-        omega.
+        lia.
       - simpl; auto.
   + (* exec_function_external *)
     destruct f; simpl in H3 |-; inversion H3; subst; clear H3.
@@ -1019,7 +1020,7 @@ Proof.
       exists path.(psize). constructor; auto.
       econstructor; eauto.
       - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
-        omega.
+        lia.
       - simpl; auto.
 Qed.
 
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index 4bb3e18e..5051d805 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -7,6 +7,7 @@ Require Import RTL RTLpath.
 Require Import Errors.
 Require Import RTLpathSE_theory RTLpathLivegenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 Local Open Scope option_monad_scope.
@@ -666,7 +667,7 @@ Proof.
   induction l2.
   - intro. destruct l1; auto. apply is_tail_false in H. contradiction.
   - intros ITAIL. inv ITAIL; auto.
-    apply IHl2 in H1. clear IHl2. simpl. omega.
+    apply IHl2 in H1. clear IHl2. simpl. lia.
 Qed.
 
 Lemma is_tail_nth_error {A} (l1 l2: list A) x:
@@ -676,14 +677,14 @@ Proof.
   induction l2.
   - intro ITAIL. apply is_tail_false in ITAIL. contradiction.
   - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H.
-    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H.
+    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; lia). rewrite H. clear H.
     inv ITAIL.
-    + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H.
+    + assert (forall n, (n - n)%nat = 0%nat) by (intro; lia). rewrite H.
       simpl. reflexivity.
     + exploit IHl2; eauto. intros. clear IHl2.
-      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega).
+      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; lia).
       exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2.
-      assert ((length l2 > length l1)%nat) by omega. clear H2.
+      assert ((length l2 > length l1)%nat) by lia. clear H2.
       rewrite H0; auto.
 Qed.
 
diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v
index 404c2a96..c8eadbd7 100644
--- a/scheduling/postpass_lib/Machblock.v
+++ b/scheduling/postpass_lib/Machblock.v
@@ -29,6 +29,7 @@ Require Import Conventions.
 Require Stacklayout.
 Require Import Mach.
 Require Import Linking.
+Require Import Lia.
 
 (** * Abstract Syntax *)
 
@@ -87,9 +88,9 @@ Lemma size_null b:
 Proof.
   destruct b as [h b e]. cbn. unfold size. cbn.
   intros H.
-  assert (length h = 0%nat) as Hh; [ omega |].
-  assert (length b = 0%nat) as Hb; [ omega |].
-  assert (length_opt e = 0%nat) as He; [ omega|].
+  assert (length h = 0%nat) as Hh; [ lia |].
+  assert (length b = 0%nat) as Hb; [ lia |].
+  assert (length_opt e = 0%nat) as He; [ lia|].
   repeat split.
   destruct h; try (cbn in Hh; discriminate); auto.
   destruct b; try (cbn in Hb; discriminate); auto.
diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v
index d121a54b..1d6c6e18 100644
--- a/scheduling/postpass_lib/Machblockgenproof.v
+++ b/scheduling/postpass_lib/Machblockgenproof.v
@@ -30,6 +30,7 @@ Require Import Linking.
 Require Import Machblock.
 Require Import Machblockgen.
 Require Import ForwardSimulationBlock.
+Require Import Lia.
 
 Ltac subst_is_trans_code H :=
   rewrite is_trans_code_inv in H;
@@ -318,12 +319,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe
 
 Lemma size_add_label l bh: size (add_label l bh) = size bh + 1.
 Proof.
-  unfold add_label, size; cbn; omega.
+  unfold add_label, size; cbn; lia.
 Qed.
 
 Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1.
 Proof.
-  intro H. unfold add_basic, size; rewrite H; cbn. omega.
+  intro H. unfold add_basic, size; rewrite H; cbn. lia.
 Qed.
 
 
@@ -341,13 +342,13 @@ Proof.
   remember (trans_code (i::c)) as bl.
   rewrite <- is_trans_code_inv in Heqbl.
   inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl.
-  - rewrite size_add_to_newblock; omega.
+  - rewrite size_add_to_newblock; lia.
   - rewrite size_add_label;
     subst_is_trans_code H.
-    omega.
+    lia.
   - rewrite size_add_basic; auto.
     subst_is_trans_code H. 
-    omega.
+    lia.
 Qed.
 
 Local Hint Resolve dist_end_block_code_simu_mid_block: core.
@@ -357,9 +358,9 @@ Lemma size_nonzero c b bl:
   is_trans_code c (b :: bl) -> size b <> 0.
 Proof.
    intros H; inversion H; subst.
-   - rewrite size_add_to_newblock; omega.
-   - rewrite size_add_label; omega.
-   - rewrite size_add_basic; auto; omega.
+   - rewrite size_add_to_newblock; lia.
+   - rewrite size_add_label; lia.
+   - rewrite size_add_basic; auto; lia.
 Qed.
 
 Inductive is_header: list label -> Mach.code -> Mach.code -> Prop :=
@@ -633,7 +634,7 @@ Proof.
       unfold dist_end_block_code. 
       subst_is_trans_code Heqtc.
       lapply (size_nonzero c b bl); auto.
-      omega.
+      lia.
     }
     rewrite X in H; unfold size in H.
     (* decomposition of starN in 3 parts: header + body + exit *)
@@ -697,7 +698,7 @@ Proof.
   apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state).
 (* simu_mid_block *)
   - intros s1 t s1' H1 H2.
-    destruct H1; cbn in * |- *; omega || (intuition auto);
+    destruct H1; cbn in * |- *; lia || (intuition auto);
     destruct H2; eapply cfi_dist_end_block; cbn; eauto.
 (* public_preserved *)
   - apply senv_preserved.