diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
| commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
| tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /kvx/PostpassScheduling.v | |
| parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
| parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
| download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip | |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'kvx/PostpassScheduling.v')
| -rw-r--r-- | kvx/PostpassScheduling.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v index 1f1f238a..08e640c6 100644 --- a/kvx/PostpassScheduling.v +++ b/kvx/PostpassScheduling.v @@ -18,6 +18,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. Require Peephole. +Require Import Lia. Local Open Scope error_monad_scope. @@ -87,8 +88,8 @@ Lemma concat2_zlt_size: Proof. intros. monadInv H. split. - - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega. - - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega. + - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. lia. + - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. lia. Qed. Lemma concat2_noexit: @@ -436,7 +437,7 @@ Lemma verified_schedule_size: Proof. intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (apply verified_schedule_nob_size; auto; fail). - inv H. simpl. omega. + inv H. simpl. lia. Qed. Lemma verified_schedule_no_header_in_middle: |