diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-29 11:12:07 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-29 11:12:07 +0200 |
commit | 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d (patch) | |
tree | c59a30ef47d86bcc3be8ae186b4305b09fb411fe /kvx/Asmblockgenproof0.v | |
parent | 9a0bf569fab7398abd46bd07d2ee777fe745f591 (diff) | |
download | compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.tar.gz compcert-kvx-7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d.zip |
replacing omega with lia in some file
Diffstat (limited to 'kvx/Asmblockgenproof0.v')
-rw-r--r-- | kvx/Asmblockgenproof0.v | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/kvx/Asmblockgenproof0.v b/kvx/Asmblockgenproof0.v index 12bb863a..83b574e7 100644 --- a/kvx/Asmblockgenproof0.v +++ b/kvx/Asmblockgenproof0.v @@ -37,6 +37,7 @@ Require Import Asmblockgen. Require Import Conventions1. Require Import Axioms. Require Import Asmblockprops. +Require Import Lia. Module MB:=Machblock. Module AB:=Asmblock. @@ -410,7 +411,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: @@ -420,10 +421,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. @@ -438,13 +439,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: @@ -452,15 +453,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: @@ -469,7 +470,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. @@ -486,8 +487,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. (** Predictor for return addresses in generated Asm code. @@ -566,7 +567,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. @@ -590,7 +591,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: @@ -598,8 +599,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. @@ -638,12 +639,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. (** Helper lemmas to reason about |