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 --- scheduling/postpass_lib/Machblock.v | 7 ++++--- scheduling/postpass_lib/Machblockgenproof.v | 21 +++++++++++---------- 2 files changed, 15 insertions(+), 13 deletions(-) (limited to 'scheduling/postpass_lib') diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v index 404c2a96..c8eadbd7 100644 --- a/scheduling/postpass_lib/Machblock.v +++ b/scheduling/postpass_lib/Machblock.v @@ -29,6 +29,7 @@ Require Import Conventions. Require Stacklayout. Require Import Mach. Require Import Linking. +Require Import Lia. (** * Abstract Syntax *) @@ -87,9 +88,9 @@ Lemma size_null b: Proof. destruct b as [h b e]. cbn. unfold size. cbn. intros H. - assert (length h = 0%nat) as Hh; [ omega |]. - assert (length b = 0%nat) as Hb; [ omega |]. - assert (length_opt e = 0%nat) as He; [ omega|]. + assert (length h = 0%nat) as Hh; [ lia |]. + assert (length b = 0%nat) as Hb; [ lia |]. + assert (length_opt e = 0%nat) as He; [ lia|]. repeat split. destruct h; try (cbn in Hh; discriminate); auto. destruct b; try (cbn in Hb; discriminate); auto. diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v index d121a54b..1d6c6e18 100644 --- a/scheduling/postpass_lib/Machblockgenproof.v +++ b/scheduling/postpass_lib/Machblockgenproof.v @@ -30,6 +30,7 @@ Require Import Linking. Require Import Machblock. Require Import Machblockgen. Require Import ForwardSimulationBlock. +Require Import Lia. Ltac subst_is_trans_code H := rewrite is_trans_code_inv in H; @@ -318,12 +319,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. Proof. - unfold add_label, size; cbn; omega. + unfold add_label, size; cbn; lia. Qed. Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. Proof. - intro H. unfold add_basic, size; rewrite H; cbn. omega. + intro H. unfold add_basic, size; rewrite H; cbn. lia. Qed. @@ -341,13 +342,13 @@ Proof. remember (trans_code (i::c)) as bl. rewrite <- is_trans_code_inv in Heqbl. inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl. - - rewrite size_add_to_newblock; omega. + - rewrite size_add_to_newblock; lia. - rewrite size_add_label; subst_is_trans_code H. - omega. + lia. - rewrite size_add_basic; auto. subst_is_trans_code H. - omega. + lia. Qed. Local Hint Resolve dist_end_block_code_simu_mid_block: core. @@ -357,9 +358,9 @@ Lemma size_nonzero c b bl: is_trans_code c (b :: bl) -> size b <> 0. Proof. intros H; inversion H; subst. - - rewrite size_add_to_newblock; omega. - - rewrite size_add_label; omega. - - rewrite size_add_basic; auto; omega. + - rewrite size_add_to_newblock; lia. + - rewrite size_add_label; lia. + - rewrite size_add_basic; auto; lia. Qed. Inductive is_header: list label -> Mach.code -> Mach.code -> Prop := @@ -633,7 +634,7 @@ Proof. unfold dist_end_block_code. subst_is_trans_code Heqtc. lapply (size_nonzero c b bl); auto. - omega. + lia. } rewrite X in H; unfold size in H. (* decomposition of starN in 3 parts: header + body + exit *) @@ -697,7 +698,7 @@ Proof. apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state). (* simu_mid_block *) - intros s1 t s1' H1 H2. - destruct H1; cbn in * |- *; omega || (intuition auto); + destruct H1; cbn in * |- *; lia || (intuition auto); destruct H2; eapply cfi_dist_end_block; cbn; eauto. (* public_preserved *) - apply senv_preserved. -- cgit