aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpath.v
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/RTLpath.v')
-rw-r--r--scheduling/RTLpath.v43
1 files changed, 22 insertions, 21 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.
generated by cgit (git 2.34.1) at 2024-06-02 14:39:25 +0000