From 965520037392fa6c523348e3ff9dff5b9d5c2313 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Fri, 18 Feb 2022 16:49:08 +0100 Subject: Remove deprecated and some warnings --- src/Misc.v | 24 ++++++++++++------------ src/State.v | 6 +++--- src/bva/BVList.v | 8 ++++---- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/Misc.v b/src/Misc.v index 5ea1d14..0317bda 100644 --- a/src/Misc.v +++ b/src/Misc.v @@ -89,20 +89,20 @@ Qed. Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true. Proof. intros x;rewrite ltb_spec, to_Z_0;assert (W:=to_Z_bounded x);split. - intros Hd;assert ([|x|] <> 0)%Z;[ | omega]. + intros Hd;assert ([|x|] <> 0)%Z;[ | lia]. intros Heq;elim Hd;apply to_Z_inj;trivial. intros Hlt Heq;elimtype False. - assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | omega]. + assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | lia]. Qed. Lemma ltb_0 : forall x, ~ (x < 0 = true). Proof. - intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);omega. + intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);lia. Qed. Lemma not_ltb_refl : forall i, ~(i < i = true). Proof. - intros;rewrite ltb_spec;omega. + intros;rewrite ltb_spec;lia. Qed. Lemma ltb_trans : forall x y z, x < y = true -> y < z = true -> x < z = true. @@ -114,7 +114,7 @@ Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y)). Proof. intros. apply eq_true_iff_eq. - rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;omega. + rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;lia. Qed. Lemma leb_ltb_trans : forall x y z, x <= y = true -> y < z = true -> x < z = true. @@ -125,7 +125,7 @@ Qed. Lemma to_Z_add_1 : forall x y, x < y = true -> [|x+1|] = ([|x|] + 1)%Z. Proof. intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y); - rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;omega. + rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;lia. Qed. Lemma to_Z_add_1_wB : forall x, ([|x|] < wB - 1)%Z -> [|x + 1|] = ([|x|] + 1)%Z. @@ -135,7 +135,7 @@ Qed. Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true). Proof. - intros n m; rewrite ltb_spec, leb_spec;omega. + intros n m; rewrite ltb_spec, leb_spec;lia. Qed. Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x). @@ -143,7 +143,7 @@ Proof. intros x y;apply Bool.eq_true_iff_eq;split;intros. apply Bool.eq_true_not_negb;apply leb_not_gtb;trivial. rewrite Bool.negb_true_iff, <- Bool.not_true_iff_false in H. - rewrite leb_spec; rewrite ltb_spec in H;omega. + rewrite leb_spec; rewrite ltb_spec in H;lia. Qed. Lemma ltb_negb_geb : forall x y, x < y = negb (y <= x). @@ -154,7 +154,7 @@ Qed. Lemma to_Z_sub_gt : forall x y, y <= x = true -> [|x - y|] = ([|x|] - [|y|])%Z. Proof. intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y); - rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;omega. + rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;lia. Qed. Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z. @@ -249,15 +249,15 @@ Proof. assert (W1 : [|n|] <> 0%Z) by (intros Heq;apply n0;apply to_Z_inj;trivial). assert (W2 := to_Z_bounded n);clear n0. assert (W3 : [|n-1|] = ([|n|] - 1)%Z). - rewrite sub_spec, to_Z_1, Zmod_small;trivial;omega. + rewrite sub_spec, to_Z_1, Zmod_small;trivial;lia. assert (H1 : n = (n-1)+1). apply to_Z_inj;rewrite add_spec, W3. - rewrite Zmod_small;rewrite to_Z_1; omega. + rewrite Zmod_small;rewrite to_Z_1; lia. case_eq ((n-1) < digits); intro l. rewrite ltb_spec in l. rewrite H1, <- !bit_half, H; trivial; rewrite ltb_spec; trivial. assert ((digits <= n) = true). - rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;omega. + rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;lia. rewrite !bit_M;trivial. Qed. diff --git a/src/State.v b/src/State.v index 4e133c6..8b899f1 100644 --- a/src/State.v +++ b/src/State.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc Ring. +Require Import List Bool Int63 Psatz Ring63 PArray Misc Ring. (* Require Import AxiomesInt. *) @@ -674,8 +674,8 @@ Module S. rewrite foldi_lt_r. apply C.resolve_correct; [ apply Hv | ring_simplify (i + 1 - 1); exact Hc ]. rewrite ltb_spec, to_Z_add_1_wB, to_Z_1. - rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); omega. - rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); omega. + rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); lia. + rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); lia. Qed. (* Weakening *) diff --git a/src/bva/BVList.v b/src/bva/BVList.v index 025bbd2..4c28ece 100644 --- a/src/bva/BVList.v +++ b/src/bva/BVList.v @@ -589,7 +589,7 @@ Definition ult_list (x y: list bool) := (ult_list_big_endian (List.rev x) (List.rev y)). -Fixpoint slt_list_big_endian (x y: list bool) := +Definition slt_list_big_endian (x y: list bool) := match x, y with | nil, _ => false | _ , nil => false @@ -2103,7 +2103,7 @@ Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. simpl. easy. - intros. - case b in *. simpl. rewrite IHa. simpl. omega. + case b in *. simpl. rewrite IHa. simpl. lia. simpl. case (k - 1