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 --- aarch64/Asmblock.v | 3 ++- aarch64/Asmblockgenproof.v | 15 +++++++------- aarch64/Asmblockgenproof0.v | 43 ++++++++++++++++++++------------------- aarch64/PostpassSchedulingproof.v | 3 ++- 4 files changed, 34 insertions(+), 30 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index c606002a..073f1f4c 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -37,6 +37,7 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Locations Conventions. Require Stacklayout. Require Import OptionMonad Asm. +Require Import Lia. Require Export Asm. Local Open Scope option_monad_scope. @@ -437,7 +438,7 @@ Qed. Lemma size_positive (b:bblock): size b > 0. Proof. unfold size. destruct b as [hd bdy ex cor]. cbn. - destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega); + destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia); unfold non_empty_bblockb in cor; simpl in cor. inversion cor. Qed. diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 6f7d39fa..11219928 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -19,6 +19,7 @@ Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock IterList. Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops. +Require Import Lia. Module MB := Machblock. Module AB := Asmblock. @@ -71,7 +72,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. - omega. + lia. Qed. Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), @@ -298,8 +299,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -389,7 +390,7 @@ Lemma mbsize_eqz: Proof. intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H. remember (length _) as a. remember (length_opt _) as b. - assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H. + assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H. inv H0. inv H1. destruct bdy; destruct ex; auto. all: try discriminate. Qed. @@ -1452,11 +1453,11 @@ Proof. rewrite Pregmap.gso; auto. rewrite V; auto. } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3'). exploit exec_straight_steps_2; eauto using functions_transl. - simpl fn_blocks. simpl fn_blocks in g. omega. constructor. + simpl fn_blocks. simpl fn_blocks in g. lia. constructor. intros (ofs' & X & Y). left; exists (State rs3' m3'); split. eapply exec_straight_steps_1; eauto. - simpl fn_blocks. simpl fn_blocks in g. omega. + simpl fn_blocks. simpl fn_blocks in g. lia. constructor. econstructor; eauto. rewrite X; econstructor; eauto. @@ -1495,7 +1496,7 @@ Local Transparent destroyed_at_function_entry. - (* return *) inv MS. inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 03d863a3..004cfd5c 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -38,6 +38,7 @@ Require Import Asmblockgen. Require Import Conventions1. Require Import Axioms. Require Import Asmblockprops. +Require Import Lia. Module MB:=Machblock. Module AB:=Asmblock. @@ -395,7 +396,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop := Lemma code_tail_pos: forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. Proof. - induction 1. omega. generalize (size_positive bi); intros; omega. + induction 1. lia. generalize (size_positive bi); intros; lia. Qed. Lemma find_bblock_tail: @@ -405,10 +406,10 @@ Lemma find_bblock_tail: Proof. induction c1; simpl; intros. inversion H. - destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega. + destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia. destruct (zeq pos 0). subst pos. - inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. - inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega. + inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia. + inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia. eauto. Qed. @@ -422,13 +423,13 @@ Proof. induction 1; intros. - subst; eauto. - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto. - omega. + lia. Qed. Lemma size_blocks_pos c: 0 <= size_blocks c. Proof. - induction c as [| a l ]; simpl; try omega. - generalize (size_positive a); omega. + induction c as [| a l ]; simpl; try lia. + generalize (size_positive a); lia. Qed. Remark code_tail_positive: @@ -436,15 +437,15 @@ Remark code_tail_positive: code_tail ofs fn c -> 0 <= ofs. Proof. induction 1; intros; simpl. - - omega. - - generalize (size_positive bi). omega. + - lia. + - generalize (size_positive bi). lia. Qed. Remark code_tail_size: forall fn ofs c, code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c. Proof. - induction 1; intros; simpl; try omega. + induction 1; intros; simpl; try lia. Qed. Remark code_tail_bounds fn ofs c: @@ -453,7 +454,7 @@ Proof. intro H; exploit code_tail_size; eauto. generalize (code_tail_positive _ _ _ H), (size_blocks_pos c). - omega. + lia. Qed. Local Hint Resolve code_tail_next: core. @@ -470,8 +471,8 @@ Proof. intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr. - rewrite Ptrofs.unsigned_repr; eauto. - omega. - - rewrite Ptrofs.unsigned_repr; omega. + lia. + - rewrite Ptrofs.unsigned_repr; lia. Qed. (** The [find_label] function returns the code tail starting at the @@ -505,12 +506,12 @@ Proof. simpl; intros until c'. case (is_label lbl a). - intros. inv H. exists pos. split; auto. split. - replace (pos - pos) with 0 by omega. constructor. constructor; try omega. - generalize (size_blocks_pos c). generalize (size_positive a). omega. + replace (pos - pos) with 0 by lia. constructor. constructor; try lia. + generalize (size_blocks_pos c). generalize (size_positive a). lia. - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega. - constructor. auto. generalize (size_positive a). omega. + replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia. + constructor. auto. generalize (size_positive a). lia. Qed. (** Predictor for return addresses in generated Asm code. @@ -589,7 +590,7 @@ Proof. exists (Ptrofs.repr ofs). red; intros. rewrite Ptrofs.unsigned_repr. congruence. exploit code_tail_bounds; eauto. - intros; apply transf_function_len in TF. omega. + intros; apply transf_function_len in TF. lia. + exists Ptrofs.zero; red; intros. congruence. Qed. @@ -613,7 +614,7 @@ Inductive transl_code_at_pc (ge: MB.genv): Remark code_tail_no_bigger: forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. Proof. - induction 1; simpl; omega. + induction 1; simpl; lia. Qed. Remark code_tail_unique: @@ -621,8 +622,8 @@ Remark code_tail_unique: code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. Proof. induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia. f_equal. eauto. Qed. diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 48840602..a5084b5f 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -21,6 +21,7 @@ Require Import Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. +Require Import Lia. Local Open Scope error_monad_scope. @@ -171,7 +172,7 @@ Proof. induction tc. - intros. simpl in H. discriminate. - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. - + inv H. assert (k = k') by omega. subst. reflexivity. + + inv H. assert (k = k') by lia. subst. reflexivity. + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto. Qed. -- cgit