From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- scheduling/RTLpath.v | 43 +++++++++++++++-------------- scheduling/RTLpathSE_simu_specs.v | 11 ++++---- scheduling/postpass_lib/Machblock.v | 7 +++-- scheduling/postpass_lib/Machblockgenproof.v | 21 +++++++------- 4 files changed, 43 insertions(+), 39 deletions(-) (limited to 'scheduling') diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v index 5b34dc16..0f303597 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. Declare Scope option_monad_scope. @@ -584,8 +585,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. @@ -602,9 +603,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. @@ -619,11 +620,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. @@ -708,7 +709,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: @@ -839,15 +840,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. @@ -876,7 +877,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 *) @@ -899,7 +900,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. @@ -908,7 +909,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. @@ -935,7 +936,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. @@ -944,7 +945,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). @@ -954,7 +955,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. @@ -976,8 +977,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. @@ -1002,7 +1003,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. @@ -1021,7 +1022,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 c6a4d409..21f89f90 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. @@ -668,7 +669,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: @@ -678,14 +679,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. -- cgit