diff options
Diffstat (limited to 'scheduling/ForwardSimulationBlock.v')
| -rw-r--r-- | scheduling/ForwardSimulationBlock.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/scheduling/ForwardSimulationBlock.v b/scheduling/ForwardSimulationBlock.v index 61466dad..cc6ecdd8 100644 --- a/scheduling/ForwardSimulationBlock.v +++ b/scheduling/ForwardSimulationBlock.v @@ -25,7 +25,7 @@ Require Import Coqlib. Require Import Events. Require Import Globalenvs. Require Import Smallstep. - +Require Import Lia. Local Open Scope nat_scope. @@ -43,8 +43,8 @@ Lemma starN_split n s t s': exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. Proof. induction 1; cbn. - + intros m k H; assert (X: m=0); try omega. - assert (X0: k=0); try omega. + + intros m k H; assert (X: m=0); try lia. + assert (X0: k=0); try lia. subst; repeat (eapply ex_intro); intuition eauto. + intros m; destruct m as [| m']; cbn. - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. @@ -119,10 +119,10 @@ Proof. intros t [H1 H2] H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. - + omega. - + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). + + lia. + + replace (dist_end_block head - dist_end_block next) with (S (dist_end_block head - dist_end_block previous)). - eapply starN_tailstep; eauto. - - omega. + - lia. Qed. Lemma follows_in_block_init (head current: state L1): @@ -131,10 +131,10 @@ Proof. intros t H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. - + omega. - + cutrewrite (dist_end_block head - dist_end_block current = 1). + + lia. + + replace (dist_end_block head - dist_end_block current) with 1. - eapply starN_tailstep; eauto. - - omega. + - lia. Qed. @@ -156,10 +156,10 @@ Proof. destruct s as [rs ms Hs]. cbn. destruct ms as [ms|]; unfold head; cbn; auto. constructor 1. - omega. - cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). + lia. + replace (dist_end_block rs - dist_end_block rs)%nat with O. + apply starN_refl; auto. - + omega. + + lia. Qed. Inductive is_well_memorized (s s': memostate): Prop := @@ -259,7 +259,7 @@ Proof. constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. * destruct (head_followed s1) as [H4 H3]. - cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. + replace (dist_end_block (head s1) - dist_end_block (real s1)) with (dist_end_block (head s1)) in H3; try lia. eapply starN_tailstep; eauto. * unfold head; rewrite H2; cbn. intuition eauto. Qed. |