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 --- riscV/RTLpathSE_simplify.v | 14 +++++++------- riscV/ValueAOp.v | 4 ++-- 2 files changed, 9 insertions(+), 9 deletions(-) (limited to 'riscV') diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 6a0297e9..2669d4bc 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -524,7 +524,7 @@ Remark ltu_12_wordsize: Proof. unfold Int.iwordsize, Int.zwordsize. simpl. unfold Int.ltu. apply zlt_true. - rewrite !Int.unsigned_repr; try cbn; try omega. + rewrite !Int.unsigned_repr; try cbn; try lia. Qed. (* Signed longs *) @@ -575,14 +575,14 @@ Proof. intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. specialize (Int.eq_spec n (Int.repr Int.max_signed)). rewrite EQMAX; simpl; intros. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. Qed. Lemma cmpl_ltle_add_one: forall v n, @@ -593,14 +593,14 @@ Proof. intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)). rewrite EQMAX; simpl; intros. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. Qed. Remark lt_maxsgn_false_int: forall i, diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 97f3ff61..ca0834db 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -13,7 +13,7 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op RTL ValueDomain. -Require Import Zbits. +Require Import Zbits Lia. (** Value analysis for RISC V operators *) @@ -390,7 +390,7 @@ Proof. assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)). { destruct ob; simpl; auto with va. - destruct b; constructor; try omega. + destruct b; constructor; try lia. change 1 with (usize Int.one). apply is_uns_usize. red; intros. apply Int.bits_zero. } -- cgit