diff options
Diffstat (limited to 'scheduling/RTLpathSE_simu_specs.v')
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 11 |
1 files changed, 6 insertions, 5 deletions
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. |