From 2e202e2b17cc3ae909628b7b3ae0b8ede3117d82 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 29 Dec 2020 14:44:33 +0100 Subject: Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le IEEE754_extra: clear unused context so that none of the context is picked up by tactics and ends as extra parameters to theorems int_round_odd_bits and int_round_odd_le Floats: simplify uses of int_round_odd_bits and int_round_odd_le accordingly. --- lib/Floats.v | 16 ++++++++-------- lib/IEEE754_extra.v | 10 +++++----- 2 files changed, 13 insertions(+), 13 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index b7769420..b9050017 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -894,7 +894,7 @@ Proof. } assert (EQ: Int64.signed n * 2 = int_round_odd (Int64.unsigned x) 1). { - symmetry. apply (int_round_odd_bits 53 1024). omega. + symmetry. apply int_round_odd_bits. omega. intros. rewrite NB2 by omega. replace i with 0 by omega. auto. rewrite NB2 by omega. rewrite dec_eq_false by omega. rewrite dec_eq_true. rewrite orb_comm. unfold Int64.testbit. change (2^1) with 2. @@ -915,7 +915,7 @@ Proof. compute_this Int64.min_signed; compute_this Int64.max_signed; compute_this Int64.modulus; xomega. - assert (2^63 <= int_round_odd (Int64.unsigned x) 1). - { change (2^63) with (int_round_odd (2^63) 1). apply (int_round_odd_le 0 0); omega. } + { change (2^63) with (int_round_odd (2^63) 1). apply int_round_odd_le; omega. } rewrite <- EQ in H1. compute_this (2^63). compute_this (2^53). xomega. - omega. Qed. @@ -1321,9 +1321,9 @@ Lemma of_long_round_odd: Proof. intros. rewrite <- (int_round_odd_plus 11) by omega. assert (-2^64 <= int_round_odd n 11). - { change (-2^64) with (int_round_odd (-2^64) 11). apply (int_round_odd_le 0 0); xomega. } + { change (-2^64) with (int_round_odd (-2^64) 11). apply int_round_odd_le; xomega. } assert (int_round_odd n 11 <= 2^64). - { change (2^64) with (int_round_odd (2^64) 11). apply (int_round_odd_le 0 0); xomega. } + { change (2^64) with (int_round_odd (2^64) 11). apply int_round_odd_le; xomega. } rewrite Bconv_BofZ. apply BofZ_round_odd with (p := 11). omega. @@ -1363,10 +1363,10 @@ Proof. set (n' := Z.land (Z.lor (Int64.unsigned n) (Z.land (Int64.unsigned n) 2047 + 2047)) (-2048)). assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; omega). assert (0 <= n'). - { rewrite <- H1. change 0 with (int_round_odd 0 11). apply (int_round_odd_le 0 0); omega. } + { rewrite <- H1. change 0 with (int_round_odd 0 11). apply int_round_odd_le; omega. } assert (n' < Int64.modulus). { apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11). - rewrite <- H1. apply (int_round_odd_le 0 0); omega. + rewrite <- H1. apply int_round_odd_le; omega. compute; auto. } rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega). f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'. @@ -1409,10 +1409,10 @@ Proof. set (n' := Z.land (Z.lor (Int64.signed n) (Z.land (Int64.signed n) 2047 + 2047)) (-2048)). assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; omega). assert (Int64.min_signed <= n'). - { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply (int_round_odd_le 0 0); omega. } + { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply int_round_odd_le; omega. } assert (n' <= Int64.max_signed). { apply Z.le_trans with (int_round_odd Int64.max_signed 11). - rewrite <- H1. apply (int_round_odd_le 0 0); omega. + rewrite <- H1. apply int_round_odd_le; omega. compute; intuition congruence. } rewrite <- (Int64.signed_repr n') by omega. f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'. diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 18313ec1..5e35a191 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -545,7 +545,7 @@ Lemma Zrnd_odd_int: Zrnd_odd (IZR n * bpow radix2 (-p)) * 2^p = int_round_odd n p. Proof. - intros. + clear. intros. assert (0 < 2^p) by (apply (Zpower_gt_0 radix2); omega). assert (n = (n / 2^p) * 2^p + n mod 2^p) by (rewrite Z.mul_comm; apply Z.div_mod; omega). assert (0 <= n mod 2^p < 2^p) by (apply Z_mod_lt; omega). @@ -586,7 +586,7 @@ Lemma int_round_odd_le: forall p x y, 0 <= p -> x <= y -> int_round_odd x p <= int_round_odd y p. Proof. - intros. + clear. intros. assert (Zrnd_odd (IZR x * bpow radix2 (-p)) <= Zrnd_odd (IZR y * bpow radix2 (-p))). { apply Zrnd_le. apply valid_rnd_odd. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le; auto. } @@ -598,7 +598,7 @@ Lemma int_round_odd_exact: forall p x, 0 <= p -> (2^p | x) -> int_round_odd x p = x. Proof. - intros. unfold int_round_odd. apply Znumtheory.Zdivide_mod in H0. + clear. intros. unfold int_round_odd. apply Znumtheory.Zdivide_mod in H0. rewrite H0. simpl. rewrite Z.mul_comm. symmetry. apply Z_div_exact_2. apply Z.lt_gt. apply (Zpower_gt_0 radix2). auto. auto. Qed. @@ -644,7 +644,7 @@ Lemma int_round_odd_shifts: int_round_odd x p = Z.shiftl (if Z.eqb (x mod 2^p) 0 then Z.shiftr x p else Z.lor (Z.shiftr x p) 1) p. Proof. - intros. + clear. intros. unfold int_round_odd. rewrite Z.shiftl_mul_pow2 by auto. f_equal. rewrite Z.shiftr_div_pow2 by auto. destruct (x mod 2^p =? 0) eqn:E. auto. @@ -662,7 +662,7 @@ Lemma int_round_odd_bits: (forall i, p < i -> Z.testbit y i = Z.testbit x i) -> int_round_odd x p = y. Proof. - intros until p; intros PPOS BELOW AT ABOVE. + clear. intros until p; intros PPOS BELOW AT ABOVE. rewrite int_round_odd_shifts by auto. apply Z.bits_inj'. intros. generalize (Zcompare_spec n p); intros SPEC; inversion SPEC. -- cgit From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- lib/Coqlib.v | 112 +++--- lib/Decidableplus.v | 6 +- lib/Floats.v | 210 +++++------ lib/IEEE754_extra.v | 260 ++++++------- lib/Integers.v | 1040 +++++++++++++++++++++++++-------------------------- lib/Intv.v | 44 +-- lib/IntvSets.v | 84 ++--- lib/Iteration.v | 4 +- lib/Maps.v | 2 +- lib/Ordered.v | 8 +- lib/Parmov.v | 2 +- lib/Postorder.v | 4 +- lib/UnionFind.v | 6 +- lib/Zbits.v | 266 ++++++------- 14 files changed, 1022 insertions(+), 1026 deletions(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 02c5d07f..948f128e 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -22,6 +22,7 @@ Require Export ZArith. Require Export Znumtheory. Require Export List. Require Export Bool. +Require Export Lia. Global Set Asymmetric Patterns. @@ -45,11 +46,7 @@ Ltac decEq := cut (A <> B); [intro; congruence | try discriminate] end. -Ltac byContradiction := - cut False; [contradiction|idtac]. - -Ltac omegaContradiction := - cut False; [contradiction|omega]. +Ltac byContradiction := exfalso. Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q. Proof. auto. Qed. @@ -180,8 +177,7 @@ Proof (Pos.lt_irrefl). Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. -Ltac xomega := unfold Plt, Ple in *; zify; omega. -Ltac xomegaContradiction := exfalso; xomega. +Ltac extlia := unfold Plt, Ple in *; lia. (** Peano recursion over positive numbers. *) @@ -284,7 +280,7 @@ Lemma zlt_true: Proof. intros. case (zlt x y); intros. auto. - omegaContradiction. + extlia. Qed. Lemma zlt_false: @@ -292,7 +288,7 @@ Lemma zlt_false: x >= y -> (if zlt x y then a else b) = b. Proof. intros. case (zlt x y); intros. - omegaContradiction. + extlia. auto. Qed. @@ -304,7 +300,7 @@ Lemma zle_true: Proof. intros. case (zle x y); intros. auto. - omegaContradiction. + extlia. Qed. Lemma zle_false: @@ -312,7 +308,7 @@ Lemma zle_false: x > y -> (if zle x y then a else b) = b. Proof. intros. case (zle x y); intros. - omegaContradiction. + extlia. auto. Qed. @@ -323,54 +319,54 @@ Proof. reflexivity. Qed. Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0. Proof. - induction n. rewrite two_power_nat_O. omega. - rewrite two_power_nat_S. omega. + induction n. rewrite two_power_nat_O. lia. + rewrite two_power_nat_S. lia. Qed. Lemma two_power_nat_two_p: forall x, two_power_nat x = two_p (Z.of_nat x). Proof. induction x. auto. - rewrite two_power_nat_S. rewrite Nat2Z.inj_succ. rewrite two_p_S. omega. omega. + rewrite two_power_nat_S. rewrite Nat2Z.inj_succ. rewrite two_p_S. lia. lia. Qed. Lemma two_p_monotone: forall x y, 0 <= x <= y -> two_p x <= two_p y. Proof. intros. - replace (two_p x) with (two_p x * 1) by omega. - replace y with (x + (y - x)) by omega. - rewrite two_p_is_exp; try omega. + replace (two_p x) with (two_p x * 1) by lia. + replace y with (x + (y - x)) by lia. + rewrite two_p_is_exp; try lia. apply Zmult_le_compat_l. - assert (two_p (y - x) > 0). apply two_p_gt_ZERO. omega. omega. - assert (two_p x > 0). apply two_p_gt_ZERO. omega. omega. + assert (two_p (y - x) > 0). apply two_p_gt_ZERO. lia. lia. + assert (two_p x > 0). apply two_p_gt_ZERO. lia. lia. Qed. Lemma two_p_monotone_strict: forall x y, 0 <= x < y -> two_p x < two_p y. Proof. - intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; omega. - assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. omega. - replace y with (Z.succ (y - 1)) by omega. rewrite two_p_S. omega. omega. + intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; lia. + assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. lia. + replace y with (Z.succ (y - 1)) by lia. rewrite two_p_S. lia. lia. Qed. Lemma two_p_strict: forall x, x >= 0 -> x < two_p x. Proof. intros x0 GT. pattern x0. apply natlike_ind. - simpl. omega. - intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). omega. - omega. + simpl. lia. + intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). lia. + lia. Qed. Lemma two_p_strict_2: forall x, x >= 0 -> 2 * x - 1 < two_p x. Proof. - intros. assert (x = 0 \/ x - 1 >= 0) by omega. destruct H0. + intros. assert (x = 0 \/ x - 1 >= 0) by lia. destruct H0. subst. vm_compute. auto. replace (two_p x) with (2 * two_p (x - 1)). - generalize (two_p_strict _ H0). omega. - rewrite <- two_p_S. decEq. omega. omega. + generalize (two_p_strict _ H0). lia. + rewrite <- two_p_S. decEq. lia. lia. Qed. (** Properties of [Zmin] and [Zmax] *) @@ -401,12 +397,12 @@ Qed. Lemma Zmax_bound_l: forall x y z, x <= y -> x <= Z.max y z. Proof. - intros. generalize (Z.le_max_l y z). omega. + intros. generalize (Z.le_max_l y z). lia. Qed. Lemma Zmax_bound_r: forall x y z, x <= z -> x <= Z.max y z. Proof. - intros. generalize (Z.le_max_r y z). omega. + intros. generalize (Z.le_max_r y z). lia. Qed. (** Properties of Euclidean division and modulus. *) @@ -416,7 +412,7 @@ Lemma Zmod_unique: x = a * y + b -> 0 <= b < y -> x mod y = b. Proof. intros. subst x. rewrite Z.add_comm. - rewrite Z_mod_plus. apply Z.mod_small. auto. omega. + rewrite Z_mod_plus. apply Z.mod_small. auto. lia. Qed. Lemma Zdiv_unique: @@ -424,14 +420,14 @@ Lemma Zdiv_unique: x = a * y + b -> 0 <= b < y -> x / y = a. Proof. intros. subst x. rewrite Z.add_comm. - rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega. + rewrite Z_div_plus. rewrite (Zdiv_small b y H0). lia. lia. Qed. Lemma Zdiv_Zdiv: forall a b c, b > 0 -> c > 0 -> (a / b) / c = a / (b * c). Proof. - intros. apply Z.div_div; omega. + intros. apply Z.div_div; lia. Qed. Lemma Zdiv_interval_1: @@ -445,14 +441,14 @@ Proof. set (q := a/b) in *. set (r := a mod b) in *. split. assert (lo < (q + 1)). - apply Zmult_lt_reg_r with b. omega. - apply Z.le_lt_trans with a. omega. + apply Zmult_lt_reg_r with b. lia. + apply Z.le_lt_trans with a. lia. replace ((q + 1) * b) with (b * q + b) by ring. - omega. - omega. - apply Zmult_lt_reg_r with b. omega. + lia. + lia. + apply Zmult_lt_reg_r with b. lia. replace (q * b) with (b * q) by ring. - omega. + lia. Qed. Lemma Zdiv_interval_2: @@ -462,13 +458,13 @@ Lemma Zdiv_interval_2: Proof. intros. assert (lo <= a / b < hi+1). - apply Zdiv_interval_1. omega. omega. auto. - assert (lo * b <= lo * 1) by (apply Z.mul_le_mono_nonpos_l; omega). + apply Zdiv_interval_1. lia. lia. auto. + assert (lo * b <= lo * 1) by (apply Z.mul_le_mono_nonpos_l; lia). replace (lo * 1) with lo in H3 by ring. - assert ((hi + 1) * 1 <= (hi + 1) * b) by (apply Z.mul_le_mono_nonneg_l; omega). + assert ((hi + 1) * 1 <= (hi + 1) * b) by (apply Z.mul_le_mono_nonneg_l; lia). replace ((hi + 1) * 1) with (hi + 1) in H4 by ring. - omega. - omega. + lia. + lia. Qed. Lemma Zmod_recombine: @@ -476,7 +472,7 @@ Lemma Zmod_recombine: a > 0 -> b > 0 -> x mod (a * b) = ((x/b) mod a) * b + (x mod b). Proof. - intros. rewrite (Z.mul_comm a b). rewrite Z.rem_mul_r by omega. ring. + intros. rewrite (Z.mul_comm a b). rewrite Z.rem_mul_r by lia. ring. Qed. (** Properties of divisibility. *) @@ -486,9 +482,9 @@ Lemma Zdivide_interval: 0 < c -> 0 <= a < b -> (c | a) -> (c | b) -> 0 <= a <= b - c. Proof. intros. destruct H1 as [x EQ1]. destruct H2 as [y EQ2]. subst. destruct H0. - split. omega. exploit Zmult_lt_reg_r; eauto. intros. + split. lia. exploit Zmult_lt_reg_r; eauto. intros. replace (y * c - c) with ((y - 1) * c) by ring. - apply Zmult_le_compat_r; omega. + apply Zmult_le_compat_r; lia. Qed. (** Conversion from [Z] to [nat]. *) @@ -503,8 +499,8 @@ Lemma Z_to_nat_max: forall z, Z.of_nat (Z.to_nat z) = Z.max z 0. Proof. intros. destruct (zle 0 z). -- rewrite Z2Nat.id by auto. xomega. -- rewrite Z_to_nat_neg by omega. xomega. +- rewrite Z2Nat.id by auto. extlia. +- rewrite Z_to_nat_neg by lia. extlia. Qed. (** Alignment: [align n amount] returns the smallest multiple of [amount] @@ -519,8 +515,8 @@ Proof. generalize (Z_div_mod_eq (x + y - 1) y H). intro. replace ((x + y - 1) / y * y) with ((x + y - 1) - (x + y - 1) mod y). - generalize (Z_mod_lt (x + y - 1) y H). omega. - rewrite Z.mul_comm. omega. + generalize (Z_mod_lt (x + y - 1) y H). lia. + rewrite Z.mul_comm. lia. Qed. Lemma align_divides: forall x y, y > 0 -> (y | align x y). @@ -599,8 +595,8 @@ Remark list_length_z_aux_shift: list_length_z_aux l n = list_length_z_aux l m + (n - m). Proof. induction l; intros; simpl. - omega. - replace (n - m) with (Z.succ n - Z.succ m) by omega. auto. + lia. + replace (n - m) with (Z.succ n - Z.succ m) by lia. auto. Qed. Definition list_length_z (A: Type) (l: list A) : Z := @@ -611,15 +607,15 @@ Lemma list_length_z_cons: list_length_z (hd :: tl) = list_length_z tl + 1. Proof. intros. unfold list_length_z. simpl. - rewrite (list_length_z_aux_shift tl 1 0). omega. + rewrite (list_length_z_aux_shift tl 1 0). lia. Qed. Lemma list_length_z_pos: forall (A: Type) (l: list A), list_length_z l >= 0. Proof. - induction l; simpl. unfold list_length_z; simpl. omega. - rewrite list_length_z_cons. omega. + induction l; simpl. unfold list_length_z; simpl. lia. + rewrite list_length_z_cons. lia. Qed. Lemma list_length_z_map: @@ -663,8 +659,8 @@ Proof. induction l; simpl; intros. discriminate. rewrite list_length_z_cons. destruct (zeq n 0). - generalize (list_length_z_pos l); omega. - exploit IHl; eauto. omega. + generalize (list_length_z_pos l); lia. + exploit IHl; eauto. lia. Qed. (** Properties of [List.incl] (list inclusion). *) diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 66dffb3a..73f080b6 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -126,14 +126,14 @@ Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { Decidable_witness := Z.geb x y }. Next Obligation. - rewrite Z.geb_le. intuition omega. + rewrite Z.geb_le. intuition lia. Qed. Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { Decidable_witness := Z.gtb x y }. Next Obligation. - rewrite Z.gtb_lt. intuition omega. + rewrite Z.gtb_lt. intuition lia. Qed. Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { @@ -146,7 +146,7 @@ Next Obligation. destruct (Z.eq_dec x 0). subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity. assert (k = y / x). - { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. } + { apply Zdiv_unique_full with 0. red; lia. rewrite EQ; ring. } congruence. Qed. diff --git a/lib/Floats.v b/lib/Floats.v index b9050017..9d0d1668 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -108,7 +108,7 @@ Proof. { apply Digits.Zdigits_le_Zpower. rewrite <- H. rewrite Z.abs_eq; tauto. } destruct (zeq p' 0). - rewrite e. simpl; auto. -- rewrite Z2Pos.id by omega. omega. +- rewrite Z2Pos.id by lia. lia. Qed. (** Transform a Nan payload to a quiet Nan payload. *) @@ -117,7 +117,7 @@ Definition quiet_nan_64_payload (p: positive) := Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 51 1%positive))) 52%nat). Lemma quiet_nan_64_proof: forall p, nan_pl 53 (quiet_nan_64_payload p) = true. -Proof. intros; apply normalized_nan; auto; omega. Qed. +Proof. intros; apply normalized_nan; auto; lia. Qed. Definition quiet_nan_64 (sp: bool * positive) : {x :float | is_nan _ _ x = true} := let (s, p) := sp in @@ -129,7 +129,7 @@ Definition quiet_nan_32_payload (p: positive) := Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 22 1%positive))) 23%nat). Lemma quiet_nan_32_proof: forall p, nan_pl 24 (quiet_nan_32_payload p) = true. -Proof. intros; apply normalized_nan; auto; omega. Qed. +Proof. intros; apply normalized_nan; auto; lia. Qed. Definition quiet_nan_32 (sp: bool * positive) : {x :float32 | is_nan _ _ x = true} := let (s, p) := sp in @@ -163,7 +163,7 @@ Proof. rewrite Z.ltb_lt in *. unfold Pos.shiftl_nat, nat_rect, Digits.digits2_pos. fold (Digits.digits2_pos p). - zify; omega. + zify; lia. Qed. Definition expand_nan s p H : {x | is_nan _ _ x = true} := @@ -336,7 +336,7 @@ Ltac smart_omega := compute_this Int64.modulus; compute_this Int64.half_modulus; compute_this Int64.max_unsigned; compute_this (Z.pow_pos 2 1024); compute_this (Z.pow_pos 2 53); compute_this (Z.pow_pos 2 52); compute_this (Z.pow_pos 2 32); - zify; omega. + zify; lia. (** Commutativity properties of addition and multiplication. *) @@ -432,7 +432,7 @@ Proof. intros; unfold of_bits, to_bits, bits_of_b64, b64_of_bits. rewrite Int64.unsigned_repr, binary_float_of_bits_of_binary_float; [reflexivity|]. generalize (bits_of_binary_float_range 52 11 __ __ f). - change (2^(52+11+1)) with (Int64.max_unsigned + 1). omega. + change (2^(52+11+1)) with (Int64.max_unsigned + 1). lia. Qed. Theorem to_of_bits: @@ -476,7 +476,7 @@ Proof. rewrite BofZ_plus by auto. f_equal. unfold Int.ltu in H. destruct zlt in H; try discriminate. - unfold y, Int.sub. rewrite Int.signed_repr. omega. + unfold y, Int.sub. rewrite Int.signed_repr. lia. compute_this (Int.unsigned ox8000_0000); smart_omega. Qed. @@ -498,8 +498,8 @@ Proof. change (Int.and ox7FFF_FFFF ox8000_0000) with Int.zero. rewrite ! Int.and_zero; auto. } assert (RNG: 0 <= Int.unsigned lo < two_p 31). - { unfold lo. change ox7FFF_FFFF with (Int.repr (two_p 31 - 1)). rewrite <- Int.zero_ext_and by omega. - apply Int.zero_ext_range. compute_this Int.zwordsize. omega. } + { unfold lo. change ox7FFF_FFFF with (Int.repr (two_p 31 - 1)). rewrite <- Int.zero_ext_and by lia. + apply Int.zero_ext_range. compute_this Int.zwordsize. lia. } assert (B: forall i, 0 <= i < Int.zwordsize -> Int.testbit ox8000_0000 i = if zeq i 31 then true else false). { intros; unfold Int.testbit. change (Int.unsigned ox8000_0000) with (2^31). destruct (zeq i 31). subst i; auto. apply Z.pow2_bits_false; auto. } @@ -512,12 +512,12 @@ Proof. assert (SU: - Int.signed hi = Int.unsigned hi). { destruct EITHER as [EQ|EQ]; rewrite EQ; reflexivity. } unfold Z.sub; rewrite SU, <- E. - unfold Int.add; rewrite Int.unsigned_repr, Int.signed_eq_unsigned. omega. - - assert (Int.max_signed = two_p 31 - 1) by reflexivity. omega. + unfold Int.add; rewrite Int.unsigned_repr, Int.signed_eq_unsigned. lia. + - assert (Int.max_signed = two_p 31 - 1) by reflexivity. lia. - assert (Int.unsigned hi = 0 \/ Int.unsigned hi = two_p 31) by (destruct EITHER as [EQ|EQ]; rewrite EQ; [left|right]; reflexivity). assert (Int.max_unsigned = two_p 31 + two_p 31 - 1) by reflexivity. - omega. + lia. Qed. Theorem to_intu_to_int_1: @@ -540,14 +540,14 @@ Proof. { rewrite ZofB_correct in C. destruct (is_finite _ _ x) eqn:FINx; congruence. } destruct (zeq p 0). subst p; smart_omega. - destruct (ZofB_range_pos 53 1024 __ __ x p C) as [P Q]. omega. + destruct (ZofB_range_pos 53 1024 __ __ x p C) as [P Q]. lia. assert (CMP: Bcompare _ _ x y = Some Lt). { unfold cmp, cmp_of_comparison, compare in H. destruct (Bcompare _ _ x y) as [[]|]; auto; discriminate. } rewrite Bcompare_correct in CMP by auto. inv CMP. apply Rcompare_Lt_inv in H1. rewrite EQy in H1. assert (p < Int.unsigned ox8000_0000). { apply lt_IZR. apply Rle_lt_trans with (1 := P) (2 := H1). } - change Int.max_signed with (Int.unsigned ox8000_0000 - 1). omega. + change Int.max_signed with (Int.unsigned ox8000_0000 - 1). lia. Qed. Theorem to_intu_to_int_2: @@ -579,7 +579,7 @@ Proof. compute_this (Int.unsigned ox8000_0000). smart_omega. apply Rge_le; auto. } - unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by omega. auto. + unfold to_int; rewrite EQ. simpl. unfold Int.sub. rewrite Int.unsigned_repr by lia. auto. Qed. (** Conversions from ints to floats can be defined as bitwise manipulations @@ -598,8 +598,8 @@ Proof. - f_equal. rewrite Int64.ofwords_add'. reflexivity. - apply split_join_bits. generalize (Int.unsigned_range x). - compute_this Int.modulus; compute_this (2^52); omega. - compute_this (2^11); omega. + compute_this Int.modulus; compute_this (2^52); lia. + compute_this (2^11); lia. Qed. Lemma from_words_value: @@ -637,7 +637,7 @@ Theorem of_intu_from_words: Proof. intros. pose proof (Int.unsigned_range x). rewrite ! from_words_eq. unfold sub. rewrite BofZ_minus. - unfold of_intu. apply (f_equal (BofZ 53 1024 __ __)). rewrite Int.unsigned_zero. omega. + unfold of_intu. apply (f_equal (BofZ 53 1024 __ __)). rewrite Int.unsigned_zero. lia. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; rewrite Int.unsigned_zero; smart_omega. Qed. @@ -664,7 +664,7 @@ Proof. rewrite ! from_words_eq. rewrite ox8000_0000_signed_unsigned. change (Int.unsigned ox8000_0000) with Int.half_modulus. unfold sub. rewrite BofZ_minus. - unfold of_int. apply f_equal. omega. + unfold of_int. apply f_equal. lia. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. Qed. @@ -680,8 +680,8 @@ Proof. - f_equal. rewrite Int64.ofwords_add'. reflexivity. - apply split_join_bits. generalize (Int.unsigned_range x). - compute_this Int.modulus; compute_this (2^52); omega. - compute_this (2^11); omega. + compute_this Int.modulus; compute_this (2^52); lia. + compute_this (2^11); lia. Qed. Lemma from_words_value': @@ -711,11 +711,11 @@ Proof. destruct (BofZ_representable 53 1024 __ __ (2^84 + Int.unsigned x * 2^32)) as (D & E & F). replace (2^84 + Int.unsigned x * 2^32) with ((2^52 + Int.unsigned x) * 2^32) by ring. - apply integer_representable_n2p; auto. smart_omega. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. apply B2R_Bsign_inj; auto. - rewrite A, D. rewrite <- IZR_Zpower by omega. rewrite <- plus_IZR. auto. + rewrite A, D. rewrite <- IZR_Zpower by lia. rewrite <- plus_IZR. auto. rewrite C, F. symmetry. apply Zlt_bool_false. - compute_this (2^84); compute_this (2^32); omega. + compute_this (2^84); compute_this (2^32); lia. Qed. Theorem of_longu_from_words: @@ -742,12 +742,12 @@ Proof. rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add'. fold xh; fold xl. compute_this (two_p 32); compute_this p20; ring. apply integer_representable_n2p; auto. - compute_this p20; smart_omega. omega. omega. + compute_this p20; smart_omega. lia. lia. apply integer_representable_n; auto; smart_omega. replace (2^84 + xh * 2^32) with ((2^52 + xh) * 2^32) by ring. - apply integer_representable_n2p; auto. smart_omega. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. change (2^84 + p20 * 2^32) with ((2^52 + 1048576) * 2^32). - apply integer_representable_n2p; auto. omega. omega. + apply integer_representable_n2p; auto. lia. lia. Qed. Theorem of_long_from_words: @@ -776,15 +776,15 @@ Proof. rewrite <- (Int64.ofwords_recompose l) at 1. rewrite Int64.ofwords_add''. fold xh; fold xl. compute_this (two_p 32); ring. apply integer_representable_n2p; auto. - compute_this (2^20); smart_omega. omega. omega. + compute_this (2^20); smart_omega. lia. lia. apply integer_representable_n; auto; smart_omega. replace (2^84 + (xh + Int.half_modulus) * 2^32) with ((2^52 + xh + Int.half_modulus) * 2^32) by (compute_this Int.half_modulus; ring). - apply integer_representable_n2p; auto. smart_omega. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. change (2^84 + p * 2^32) with ((2^52 + p) * 2^32). apply integer_representable_n2p; auto. - compute_this p; smart_omega. omega. + compute_this p; smart_omega. lia. Qed. (** Conversions from 64-bit integers can be expressed in terms of @@ -806,7 +806,7 @@ Proof. assert (DECOMP: x = yh * 2^32 + yl). { unfold x. rewrite <- (Int64.ofwords_recompose l). apply Int64.ofwords_add'. } rewrite BofZ_mult. rewrite BofZ_plus. rewrite DECOMP; auto. - apply integer_representable_n2p; auto. smart_omega. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. @@ -829,7 +829,7 @@ Proof. assert (DECOMP: x = yh * 2^32 + yl). { unfold x. rewrite <- (Int64.ofwords_recompose l), Int64.ofwords_add''. auto. } rewrite BofZ_mult. rewrite BofZ_plus. rewrite DECOMP; auto. - apply integer_representable_n2p; auto. smart_omega. omega. omega. + apply integer_representable_n2p; auto. smart_omega. lia. lia. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto; smart_omega. apply integer_representable_n; auto. compute; intuition congruence. @@ -871,53 +871,53 @@ Proof. { intros; unfold n; autorewrite with ints; auto. rewrite Int64.unsigned_one. rewrite Int64.bits_one. compute_this Int64.zwordsize. destruct (zeq i 0); simpl proj_sumbool. - rewrite zlt_true by omega. rewrite andb_true_r. subst i; auto. + rewrite zlt_true by lia. rewrite andb_true_r. subst i; auto. rewrite andb_false_r, orb_false_r. - destruct (zeq i 63). subst i. apply zlt_false; omega. - apply zlt_true; omega. } + destruct (zeq i 63). subst i. apply zlt_false; lia. + apply zlt_true; lia. } assert (NB2: forall i, 0 <= i -> Z.testbit (Int64.signed n * 2^1) i = if zeq i 0 then false else if zeq i 1 then Int64.testbit x 1 || Int64.testbit x 0 else Int64.testbit x i). - { intros. rewrite Z.mul_pow2_bits by omega. destruct (zeq i 0). - apply Z.testbit_neg_r; omega. - rewrite Int64.bits_signed by omega. compute_this Int64.zwordsize. + { intros. rewrite Z.mul_pow2_bits by lia. destruct (zeq i 0). + apply Z.testbit_neg_r; lia. + rewrite Int64.bits_signed by lia. compute_this Int64.zwordsize. destruct (zlt (i-1) 64). - rewrite NB by omega. destruct (zeq i 1). + rewrite NB by lia. destruct (zeq i 1). subst. rewrite dec_eq_true by auto. auto. - rewrite dec_eq_false by omega. destruct (zeq (i - 1) 63). - symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; omega. - f_equal; omega. - rewrite NB by omega. rewrite dec_eq_false by omega. rewrite dec_eq_true by auto. - rewrite dec_eq_false by omega. symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; omega. + rewrite dec_eq_false by lia. destruct (zeq (i - 1) 63). + symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; lia. + f_equal; lia. + rewrite NB by lia. rewrite dec_eq_false by lia. rewrite dec_eq_true by auto. + rewrite dec_eq_false by lia. symmetry. apply Int64.bits_above. compute_this Int64.zwordsize; lia. } assert (EQ: Int64.signed n * 2 = int_round_odd (Int64.unsigned x) 1). { - symmetry. apply int_round_odd_bits. omega. - intros. rewrite NB2 by omega. replace i with 0 by omega. auto. - rewrite NB2 by omega. rewrite dec_eq_false by omega. rewrite dec_eq_true. + symmetry. apply int_round_odd_bits. lia. + intros. rewrite NB2 by lia. replace i with 0 by lia. auto. + rewrite NB2 by lia. rewrite dec_eq_false by lia. rewrite dec_eq_true. rewrite orb_comm. unfold Int64.testbit. change (2^1) with 2. destruct (Z.testbit (Int64.unsigned x) 0) eqn:B0; - [rewrite Z.testbit_true in B0 by omega|rewrite Z.testbit_false in B0 by omega]; + [rewrite Z.testbit_true in B0 by lia|rewrite Z.testbit_false in B0 by lia]; change (2^0) with 1 in B0; rewrite Zdiv_1_r in B0; rewrite B0; auto. - intros. rewrite NB2 by omega. rewrite ! dec_eq_false by omega. auto. + intros. rewrite NB2 by lia. rewrite ! dec_eq_false by lia. auto. } unfold mul, of_long, of_longu. rewrite BofZ_mult_2p. - change (2^1) with 2. rewrite EQ. apply BofZ_round_odd with (p := 1). -+ omega. ++ lia. + apply Z.le_trans with Int64.modulus; trivial. smart_omega. -+ omega. -+ apply Z.le_trans with (2^63). compute; intuition congruence. xomega. ++ lia. ++ apply Z.le_trans with (2^63). compute; intuition congruence. extlia. - apply Z.le_trans with Int64.modulus; trivial. pose proof (Int64.signed_range n). compute_this Int64.min_signed; compute_this Int64.max_signed; - compute_this Int64.modulus; xomega. + compute_this Int64.modulus; extlia. - assert (2^63 <= int_round_odd (Int64.unsigned x) 1). - { change (2^63) with (int_round_odd (2^63) 1). apply int_round_odd_le; omega. } - rewrite <- EQ in H1. compute_this (2^63). compute_this (2^53). xomega. -- omega. + { change (2^63) with (int_round_odd (2^63) 1). apply int_round_odd_le; lia. } + rewrite <- EQ in H1. compute_this (2^63). compute_this (2^53). extlia. +- lia. Qed. (** Conversions to/from 32-bit integers can be implemented by going through 64-bit integers. *) @@ -931,8 +931,8 @@ Proof. intros. exploit ZofB_range_inversion; eauto. intros (A & B & C). unfold ZofB_range; rewrite C. replace (min2 <=? n) with true. replace (n <=? max2) with true. auto. - symmetry; apply Z.leb_le; omega. - symmetry; apply Z.leb_le; omega. + symmetry; apply Z.leb_le; lia. + symmetry; apply Z.leb_le; lia. Qed. Theorem to_int_to_long: @@ -954,7 +954,7 @@ Proof. exploit ZofB_range_inversion; eauto. intros (A & B & C). replace (ZofB_range 53 1024 f 0 Int64.max_unsigned) with (Some z). simpl. rewrite Int.unsigned_repr; auto. - symmetry; eapply ZofB_range_widen; eauto. omega. compute; congruence. + symmetry; eapply ZofB_range_widen; eauto. lia. compute; congruence. Qed. Theorem to_intu_to_long: @@ -1183,7 +1183,7 @@ Theorem cmp_double: forall f1 f2 c, cmp c f1 f2 = Float.cmp c (to_double f1) (to_double f2). Proof. unfold cmp, Float.cmp; intros. f_equal. symmetry. apply Bcompare_Bconv_widen. - red; omega. omega. omega. + red; lia. lia. lia. Qed. (** Properties of conversions to/from in-memory representation. @@ -1195,7 +1195,7 @@ Proof. intros; unfold of_bits, to_bits, bits_of_b32, b32_of_bits. rewrite Int.unsigned_repr, binary_float_of_bits_of_binary_float; [reflexivity|]. generalize (bits_of_binary_float_range 23 8 __ __ f). - change (2^(23+8+1)) with (Int.max_unsigned + 1). omega. + change (2^(23+8+1)) with (Int.max_unsigned + 1). lia. Qed. Theorem to_of_bits: @@ -1235,7 +1235,7 @@ Proof. unfold to_int in H. destruct (ZofB_range _ _ f Int.min_signed Int.max_signed) as [n'|] eqn:E; inv H. unfold Float.to_int, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. Theorem to_intu_double: @@ -1245,7 +1245,7 @@ Proof. unfold to_intu in H. destruct (ZofB_range _ _ f 0 Int.max_unsigned) as [n'|] eqn:E; inv H. unfold Float.to_intu, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. Theorem to_long_double: @@ -1255,7 +1255,7 @@ Proof. unfold to_long in H. destruct (ZofB_range _ _ f Int64.min_signed Int64.max_signed) as [n'|] eqn:E; inv H. unfold Float.to_long, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. Theorem to_longu_double: @@ -1265,7 +1265,7 @@ Proof. unfold to_longu in H. destruct (ZofB_range _ _ f 0 Int64.max_unsigned) as [n'|] eqn:E; inv H. unfold Float.to_longu, to_double, Float.of_single. - erewrite ZofB_range_Bconv; eauto. auto. omega. omega. omega. omega. + erewrite ZofB_range_Bconv; eauto. auto. lia. lia. lia. lia. Qed. (** Conversions from 64-bit integers to single-precision floats can be expressed @@ -1280,37 +1280,37 @@ Proof. intros. assert (POS: 0 < 2^p) by (apply (Zpower_gt_0 radix2); auto). assert (A: Z.land n (2^p-1) = n mod 2^p). - { rewrite <- Z.land_ones by auto. f_equal. rewrite Z.ones_equiv. omega. } + { rewrite <- Z.land_ones by auto. f_equal. rewrite Z.ones_equiv. lia. } rewrite A. assert (B: 0 <= n mod 2^p < 2^p). - { apply Z_mod_lt. omega. } + { apply Z_mod_lt. lia. } set (m := n mod 2^p + (2^p-1)) in *. assert (C: m / 2^p = if zeq (n mod 2^p) 0 then 0 else 1). { unfold m. destruct (zeq (n mod 2^p) 0). - rewrite e. apply Z.div_small. omega. - eapply Coqlib.Zdiv_unique with (n mod 2^p - 1). ring. omega. } + rewrite e. apply Z.div_small. lia. + eapply Coqlib.Zdiv_unique with (n mod 2^p - 1). ring. lia. } assert (D: Z.testbit m p = if zeq (n mod 2^p) 0 then false else true). { destruct (zeq (n mod 2^p) 0). apply Z.testbit_false; auto. rewrite C; auto. apply Z.testbit_true; auto. rewrite C; auto. } assert (E: forall i, p < i -> Z.testbit m i = false). - { intros. apply Z.testbit_false. omega. + { intros. apply Z.testbit_false. lia. replace (m / 2^i) with 0. auto. symmetry. apply Z.div_small. - unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega. - change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega. - apply Zpower_le. omega. } + unfold m. split. lia. apply Z.lt_le_trans with (2 * 2^p). lia. + change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by lia. + apply Zpower_le. lia. } assert (F: forall i, 0 <= i -> Z.testbit (-2^p) i = if zlt i p then false else true). { intros. rewrite Z.bits_opp by auto. rewrite <- Z.ones_equiv. destruct (zlt i p). - rewrite Z.ones_spec_low by omega. auto. - rewrite Z.ones_spec_high by omega. auto. } + rewrite Z.ones_spec_low by lia. auto. + rewrite Z.ones_spec_high by lia. auto. } apply int_round_odd_bits; auto. - - intros. rewrite Z.land_spec, F, zlt_true by omega. apply andb_false_r. - - rewrite Z.land_spec, Z.lor_spec, D, F, zlt_false, andb_true_r by omega. + - intros. rewrite Z.land_spec, F, zlt_true by lia. apply andb_false_r. + - rewrite Z.land_spec, Z.lor_spec, D, F, zlt_false, andb_true_r by lia. destruct (Z.eqb (n mod 2^p) 0) eqn:Z. rewrite Z.eqb_eq in Z. rewrite Z, zeq_true. apply orb_false_r. rewrite Z.eqb_neq in Z. rewrite zeq_false by auto. apply orb_true_r. - - intros. rewrite Z.land_spec, Z.lor_spec, E, F, zlt_false, andb_true_r by omega. + - intros. rewrite Z.land_spec, Z.lor_spec, E, F, zlt_false, andb_true_r by lia. apply orb_false_r. Qed. @@ -1319,22 +1319,22 @@ Lemma of_long_round_odd: 2^36 <= Z.abs n < 2^64 -> BofZ 24 128 __ __ n = Bconv _ _ 24 128 __ __ conv_nan mode_NE (BofZ 53 1024 __ __ (Z.land (Z.lor n ((Z.land n 2047) + 2047)) (-2048))). Proof. - intros. rewrite <- (int_round_odd_plus 11) by omega. + intros. rewrite <- (int_round_odd_plus 11) by lia. assert (-2^64 <= int_round_odd n 11). - { change (-2^64) with (int_round_odd (-2^64) 11). apply int_round_odd_le; xomega. } + { change (-2^64) with (int_round_odd (-2^64) 11). apply int_round_odd_le; extlia. } assert (int_round_odd n 11 <= 2^64). - { change (2^64) with (int_round_odd (2^64) 11). apply int_round_odd_le; xomega. } + { change (2^64) with (int_round_odd (2^64) 11). apply int_round_odd_le; extlia. } rewrite Bconv_BofZ. apply BofZ_round_odd with (p := 11). - omega. - apply Z.le_trans with (2^64). omega. compute; intuition congruence. - omega. + lia. + apply Z.le_trans with (2^64). lia. compute; intuition congruence. + lia. exact (proj1 H). - unfold int_round_odd. apply integer_representable_n2p_wide. auto. omega. + unfold int_round_odd. apply integer_representable_n2p_wide. auto. lia. unfold int_round_odd in H0, H1. split; (apply Zmult_le_reg_r with (2^11); [compute; auto | assumption]). - omega. - omega. + lia. + lia. Qed. Theorem of_longu_double_1: @@ -1343,7 +1343,7 @@ Theorem of_longu_double_1: of_longu n = of_double (Float.of_longu n). Proof. intros. symmetry; apply Bconv_BofZ. apply integer_representable_n; auto. - pose proof (Int64.unsigned_range n); omega. + pose proof (Int64.unsigned_range n); lia. Qed. Theorem of_longu_double_2: @@ -1361,14 +1361,14 @@ Proof. unfold of_double, Float.to_single. instantiate (1 := Float.to_single_nan). f_equal. unfold Float.of_longu. f_equal. set (n' := Z.land (Z.lor (Int64.unsigned n) (Z.land (Int64.unsigned n) 2047 + 2047)) (-2048)). - assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; omega). + assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; lia). assert (0 <= n'). - { rewrite <- H1. change 0 with (int_round_odd 0 11). apply int_round_odd_le; omega. } + { rewrite <- H1. change 0 with (int_round_odd 0 11). apply int_round_odd_le; lia. } assert (n' < Int64.modulus). { apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11). - rewrite <- H1. apply int_round_odd_le; omega. + rewrite <- H1. apply int_round_odd_le; lia. compute; auto. } - rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega). + rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; lia). f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'. rewrite Z.land_spec, Z.lor_spec. f_equal. f_equal. unfold Int64.testbit. rewrite Int64.add_unsigned. @@ -1377,11 +1377,11 @@ Proof. Int64.unsigned (Int64.repr 2047))) i). rewrite Int64.testbit_repr by auto. f_equal. f_equal. unfold Int64.and. symmetry. apply Int64.unsigned_repr. change 2047 with (Z.ones 11). - rewrite Z.land_ones by omega. + rewrite Z.land_ones by lia. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. - assert (2^11 < Int64.max_unsigned) by (compute; auto). omega. + assert (2^11 < Int64.max_unsigned) by (compute; auto). lia. apply Int64.same_bits_eqm; auto. exists (-1); auto. - split. xomega. change (2^64) with Int64.modulus. xomega. + split. extlia. change (2^64) with Int64.modulus. extlia. Qed. Theorem of_long_double_1: @@ -1389,7 +1389,7 @@ Theorem of_long_double_1: Z.abs (Int64.signed n) <= 2^53 -> of_long n = of_double (Float.of_long n). Proof. - intros. symmetry; apply Bconv_BofZ. apply integer_representable_n; auto. xomega. + intros. symmetry; apply Bconv_BofZ. apply integer_representable_n; auto. extlia. Qed. Theorem of_long_double_2: @@ -1407,34 +1407,34 @@ Proof. unfold of_double, Float.to_single. instantiate (1 := Float.to_single_nan). f_equal. unfold Float.of_long. f_equal. set (n' := Z.land (Z.lor (Int64.signed n) (Z.land (Int64.signed n) 2047 + 2047)) (-2048)). - assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; omega). + assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; lia). assert (Int64.min_signed <= n'). - { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply int_round_odd_le; omega. } + { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply int_round_odd_le; lia. } assert (n' <= Int64.max_signed). { apply Z.le_trans with (int_round_odd Int64.max_signed 11). - rewrite <- H1. apply int_round_odd_le; omega. + rewrite <- H1. apply int_round_odd_le; lia. compute; intuition congruence. } - rewrite <- (Int64.signed_repr n') by omega. + rewrite <- (Int64.signed_repr n') by lia. f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'. rewrite Z.land_spec, Z.lor_spec. f_equal. f_equal. - rewrite Int64.bits_signed by omega. rewrite zlt_true by omega. auto. + rewrite Int64.bits_signed by lia. rewrite zlt_true by lia. auto. unfold Int64.testbit. rewrite Int64.add_unsigned. fold (Int64.testbit (Int64.repr (Int64.unsigned (Int64.and n (Int64.repr 2047)) + Int64.unsigned (Int64.repr 2047))) i). rewrite Int64.testbit_repr by auto. f_equal. f_equal. unfold Int64.and. change (Int64.unsigned (Int64.repr 2047)) with 2047. - change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega. + change 2047 with (Z.ones 11). rewrite ! Z.land_ones by lia. rewrite Int64.unsigned_repr. apply eqmod_mod_eq. - apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega. + apply Z.lt_gt. apply (Zpower_gt_0 radix2); lia. apply eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. exists (2^(64-11)); auto. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. - assert (2^11 < Int64.max_unsigned) by (compute; auto). omega. + assert (2^11 < Int64.max_unsigned) by (compute; auto). lia. apply Int64.same_bits_eqm; auto. exists (-1); auto. split. auto. assert (-2^64 < Int64.min_signed) by (compute; auto). assert (Int64.max_signed < 2^64) by (compute; auto). - xomega. + extlia. Qed. End Float32. diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 5e35a191..580d4f90 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -119,7 +119,7 @@ Definition integer_representable (n: Z): Prop := Let int_upper_bound_eq: 2^emax - 2^(emax - prec) = (2^prec - 1) * 2^(emax - prec). Proof. red in prec_gt_0_. - ring_simplify. rewrite <- (Zpower_plus radix2) by omega. f_equal. f_equal. omega. + ring_simplify. rewrite <- (Zpower_plus radix2) by lia. f_equal. f_equal. lia. Qed. Lemma integer_representable_n2p: @@ -130,14 +130,14 @@ Proof. intros; split. - red in prec_gt_0_. replace (Z.abs (n * 2^p)) with (Z.abs n * 2^p). rewrite int_upper_bound_eq. - apply Zmult_le_compat. zify; omega. apply (Zpower_le radix2); omega. - zify; omega. apply (Zpower_ge_0 radix2). + apply Zmult_le_compat. zify; lia. apply (Zpower_le radix2); lia. + zify; lia. apply (Zpower_ge_0 radix2). rewrite Z.abs_mul. f_equal. rewrite Z.abs_eq. auto. apply (Zpower_ge_0 radix2). - apply generic_format_FLT. exists (Float radix2 n p). unfold F2R; simpl. rewrite <- IZR_Zpower by auto. apply mult_IZR. - simpl; zify; omega. - unfold emin, Fexp; red in prec_gt_0_; omega. + simpl; zify; lia. + unfold emin, Fexp; red in prec_gt_0_; lia. Qed. Lemma integer_representable_2p: @@ -149,19 +149,19 @@ Proof. - red in prec_gt_0_. rewrite Z.abs_eq by (apply (Zpower_ge_0 radix2)). apply Z.le_trans with (2^(emax-1)). - apply (Zpower_le radix2); omega. + apply (Zpower_le radix2); lia. assert (2^emax = 2^(emax-1)*2). - { change 2 with (2^1) at 3. rewrite <- (Zpower_plus radix2) by omega. - f_equal. omega. } + { change 2 with (2^1) at 3. rewrite <- (Zpower_plus radix2) by lia. + f_equal. lia. } assert (2^(emax - prec) <= 2^(emax - 1)). - { apply (Zpower_le radix2). omega. } - omega. + { apply (Zpower_le radix2). lia. } + lia. - red in prec_gt_0_. apply generic_format_FLT. exists (Float radix2 1 p). unfold F2R; simpl. - rewrite Rmult_1_l. rewrite <- IZR_Zpower. auto. omega. - simpl Z.abs. change 1 with (2^0). apply (Zpower_lt radix2). omega. auto. - unfold emin, Fexp; omega. + rewrite Rmult_1_l. rewrite <- IZR_Zpower. auto. lia. + simpl Z.abs. change 1 with (2^0). apply (Zpower_lt radix2). lia. auto. + unfold emin, Fexp; lia. Qed. Lemma integer_representable_opp: @@ -178,12 +178,12 @@ Lemma integer_representable_n2p_wide: Proof. intros. red in prec_gt_0_. destruct (Z.eq_dec n (2^prec)); [idtac | destruct (Z.eq_dec n (-2^prec))]. -- rewrite e. rewrite <- (Zpower_plus radix2) by omega. - apply integer_representable_2p. omega. +- rewrite e. rewrite <- (Zpower_plus radix2) by lia. + apply integer_representable_2p. lia. - rewrite e. rewrite <- Zopp_mult_distr_l. apply integer_representable_opp. - rewrite <- (Zpower_plus radix2) by omega. - apply integer_representable_2p. omega. -- apply integer_representable_n2p; omega. + rewrite <- (Zpower_plus radix2) by lia. + apply integer_representable_2p. lia. +- apply integer_representable_n2p; lia. Qed. Lemma integer_representable_n: @@ -191,7 +191,7 @@ Lemma integer_representable_n: Proof. red in prec_gt_0_. intros. replace n with (n * 2^0) by (change (2^0) with 1; ring). - apply integer_representable_n2p_wide. auto. omega. omega. + apply integer_representable_n2p_wide. auto. lia. lia. Qed. Lemma round_int_no_overflow: @@ -205,14 +205,14 @@ Proof. apply round_le_generic. apply fexp_correct; auto. apply valid_rnd_N. apply generic_format_FLT. exists (Float radix2 (2^prec-1) (emax-prec)). rewrite int_upper_bound_eq. unfold F2R; simpl. - rewrite <- IZR_Zpower by omega. rewrite <- mult_IZR. auto. - assert (0 < 2^prec) by (apply (Zpower_gt_0 radix2); omega). - unfold Fnum; simpl; zify; omega. - unfold emin, Fexp; omega. + rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR. auto. + assert (0 < 2^prec) by (apply (Zpower_gt_0 radix2); lia). + unfold Fnum; simpl; zify; lia. + unfold emin, Fexp; lia. rewrite <- abs_IZR. apply IZR_le. auto. - rewrite <- IZR_Zpower by omega. apply IZR_lt. simpl. - assert (0 < 2^(emax-prec)) by (apply (Zpower_gt_0 radix2); omega). - omega. + rewrite <- IZR_Zpower by lia. apply IZR_lt. simpl. + assert (0 < 2^(emax-prec)) by (apply (Zpower_gt_0 radix2); lia). + lia. apply fexp_correct. auto. Qed. @@ -299,8 +299,8 @@ Proof. { apply round_le_generic. apply fexp_correct. auto. apply valid_rnd_N. apply (integer_representable_opp 1). apply (integer_representable_2p 0). - red in prec_gt_0_; omega. - apply IZR_le; omega. + red in prec_gt_0_; lia. + apply IZR_le; lia. } lra. Qed. @@ -335,7 +335,7 @@ Proof. rewrite R, W, C, F. rewrite Rcompare_IZR. unfold Z.ltb at 3. generalize (Zcompare_spec (p + q) 0); intros SPEC; inversion SPEC; auto. - assert (EITHER: 0 <= p \/ 0 <= q) by omega. + assert (EITHER: 0 <= p \/ 0 <= q) by lia. destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2]; apply Zlt_bool_false; auto. - intros P (U & V). @@ -343,8 +343,8 @@ Proof. rewrite P, U, C. f_equal. rewrite C, F in V. generalize (Zlt_bool_spec p 0) (Zlt_bool_spec q 0). rewrite <- V. intros SPEC1 SPEC2; inversion SPEC1; inversion SPEC2; try congruence; symmetry. - apply Zlt_bool_true; omega. - apply Zlt_bool_false; omega. + apply Zlt_bool_true; lia. + apply Zlt_bool_false; lia. Qed. Theorem BofZ_minus: @@ -365,7 +365,7 @@ Proof. rewrite R, W, C, F. rewrite Rcompare_IZR. unfold Z.ltb at 3. generalize (Zcompare_spec (p - q) 0); intros SPEC; inversion SPEC; auto. - assert (EITHER: 0 <= p \/ q < 0) by omega. + assert (EITHER: 0 <= p \/ q < 0) by lia. destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2]. rewrite Zlt_bool_false; auto. rewrite Zlt_bool_true; auto. @@ -375,8 +375,8 @@ Proof. generalize (Zlt_bool_spec p 0) (Zlt_bool_spec q 0). rewrite V. intros SPEC1 SPEC2; inversion SPEC1; inversion SPEC2; symmetry. rewrite <- H3 in H1; discriminate. - apply Zlt_bool_true; omega. - apply Zlt_bool_false; omega. + apply Zlt_bool_true; lia. + apply Zlt_bool_false; lia. rewrite <- H3 in H1; discriminate. Qed. @@ -389,10 +389,10 @@ Proof. intros. assert (SIGN: xorb (p 0%R) by (apply (IZR_neq _ _ n)). destruct (BofZ_finite x H) as (A & B & C). destruct (BofZ_representable (2^p)) as (D & E & F). @@ -432,16 +432,16 @@ Proof. cexp radix2 fexp (IZR x) + p). { unfold cexp, fexp. rewrite mult_IZR. - change (2^p) with (radix2^p). rewrite IZR_Zpower by omega. + change (2^p) with (radix2^p). rewrite IZR_Zpower by lia. rewrite mag_mult_bpow by auto. assert (prec + 1 <= mag radix2 (IZR x)). { rewrite <- (mag_abs radix2 (IZR x)). rewrite <- (mag_bpow radix2 prec). apply mag_le. - apply bpow_gt_0. rewrite <- IZR_Zpower by (red in prec_gt_0_;omega). + apply bpow_gt_0. rewrite <- IZR_Zpower by (red in prec_gt_0_;lia). rewrite <- abs_IZR. apply IZR_le; auto. } unfold FLT_exp. - unfold emin; red in prec_gt_0_; zify; omega. + unfold emin; red in prec_gt_0_; zify; lia. } assert (forall m, round radix2 fexp m (IZR x) * IZR (2^p) = round radix2 fexp m (IZR (x * 2^p)))%R. @@ -451,11 +451,11 @@ Proof. set (a := IZR x); set (b := bpow radix2 (- cexp radix2 fexp a)). replace (a * IZR (2^p) * (b * bpow radix2 (-p)))%R with (a * b)%R. unfold F2R; simpl. rewrite Rmult_assoc. f_equal. - rewrite bpow_plus. f_equal. apply (IZR_Zpower radix2). omega. + rewrite bpow_plus. f_equal. apply (IZR_Zpower radix2). lia. transitivity ((a * b) * (IZR (2^p) * bpow radix2 (-p)))%R. rewrite (IZR_Zpower radix2). rewrite <- bpow_plus. - replace (p + -p) with 0 by omega. change (bpow radix2 0) with 1%R. ring. - omega. + replace (p + -p) with 0 by lia. change (bpow radix2 0) with 1%R. ring. + lia. ring. } assert (forall m x, @@ -468,11 +468,11 @@ Proof. } assert (xorb (x xO) n) = 2 ^ (Z.of_nat n)). { induction n. reflexivity. simpl nat_rect. transitivity (2 * Z.pos (nat_rect _ xH (fun _ => xO) n)). reflexivity. - rewrite Nat2Z.inj_succ. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega. + rewrite Nat2Z.inj_succ. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by lia. change (2 ^ 1) with 2. ring. } red in prec_gt_0_. - unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite REC. - rewrite Zabs2Nat.id_abs. rewrite Z.abs_eq by omega. auto. + unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by lia. rewrite REC. + rewrite Zabs2Nat.id_abs. rewrite Z.abs_eq by lia. auto. Qed. Remark Bexact_inverse_mantissa_digits2_pos: @@ -1013,11 +1013,11 @@ Proof. assert (DIGITS: forall n, digits2_pos (nat_rect _ xH (fun _ => xO) n) = Pos.of_nat (n+1)). { induction n; simpl. auto. rewrite IHn. destruct n; auto. } red in prec_gt_0_. - unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite DIGITS. - rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by omega. + unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by lia. rewrite DIGITS. + rewrite Zabs2Nat.abs_nat_nonneg, Z2Nat.inj_sub by lia. destruct prec; try discriminate. rewrite Nat.sub_add. simpl. rewrite Pos2Nat.id. auto. - simpl. zify; omega. + simpl. zify; lia. Qed. Remark bounded_Bexact_inverse: @@ -1028,8 +1028,8 @@ Proof. rewrite <- Zeq_is_eq_bool. rewrite <- Zle_is_le_bool. rewrite Bexact_inverse_mantissa_digits2_pos. split. -- intros; split. unfold FLT_exp. unfold emin in H. zify; omega. omega. -- intros [A B]. unfold FLT_exp in A. unfold emin. zify; omega. +- intros; split. unfold FLT_exp. unfold emin in H. zify; lia. lia. +- intros [A B]. unfold FLT_exp in A. unfold emin. zify; lia. Qed. Program Definition Bexact_inverse (f: binary_float) : option binary_float := @@ -1045,7 +1045,7 @@ Program Definition Bexact_inverse (f: binary_float) : option binary_float := end. Next Obligation. rewrite <- bounded_Bexact_inverse in B. rewrite <- bounded_Bexact_inverse. - unfold emin in *. omega. + unfold emin in *. lia. Qed. Lemma Bexact_inverse_correct: @@ -1067,9 +1067,9 @@ Proof with (try discriminate). rewrite <- ! cond_Ropp_mult_l. red in prec_gt_0_. replace (IZR (2 ^ (prec - 1))) with (bpow radix2 (prec - 1)) - by (symmetry; apply (IZR_Zpower radix2); omega). + by (symmetry; apply (IZR_Zpower radix2); lia). rewrite <- ! bpow_plus. - replace (prec - 1 + e') with (- (prec - 1 + e)) by (unfold e'; omega). + replace (prec - 1 + e') with (- (prec - 1 + e)) by (unfold e'; lia). rewrite bpow_opp. unfold cond_Ropp; destruct s; auto. rewrite Ropp_inv_permute. auto. apply Rgt_not_eq. apply bpow_gt_0. split. simpl. apply F2R_neq_0. destruct s; simpl in H; discriminate. @@ -1163,9 +1163,9 @@ Proof. assert (C: 0 <= Z.log2_up base) by apply Z.log2_up_nonneg. destruct (Z.log2_spec base) as [D E]; auto. destruct (Z.log2_up_spec base) as [F G]. apply radix_gt_1. - assert (K: 0 <= 2 ^ Z.log2 base) by (apply Z.pow_nonneg; omega). - rewrite ! (Z.mul_comm n). rewrite ! Z.pow_mul_r by omega. - split; apply Z.pow_le_mono_l; omega. + assert (K: 0 <= 2 ^ Z.log2 base) by (apply Z.pow_nonneg; lia). + rewrite ! (Z.mul_comm n). rewrite ! Z.pow_mul_r by lia. + split; apply Z.pow_le_mono_l; lia. Qed. Lemma bpow_log_pos: @@ -1174,8 +1174,8 @@ Lemma bpow_log_pos: (bpow radix2 (n * Z.log2 base)%Z <= bpow base n)%R. Proof. intros. rewrite <- ! IZR_Zpower. apply IZR_le; apply Zpower_log; auto. - omega. - rewrite Z.mul_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg. + lia. + rewrite Z.mul_comm; apply Zmult_gt_0_le_0_compat. lia. apply Z.log2_nonneg. Qed. Lemma bpow_log_neg: @@ -1183,10 +1183,10 @@ Lemma bpow_log_neg: n < 0 -> (bpow base n <= bpow radix2 (n * Z.log2 base)%Z)%R. Proof. - intros. set (m := -n). replace n with (-m) by (unfold m; omega). + intros. set (m := -n). replace n with (-m) by (unfold m; lia). rewrite ! Z.mul_opp_l, ! bpow_opp. apply Rinv_le. apply bpow_gt_0. - apply bpow_log_pos. unfold m; omega. + apply bpow_log_pos. unfold m; lia. Qed. (** Overflow and underflow conditions. *) @@ -1203,12 +1203,12 @@ Proof. rewrite <- (Rmult_1_l (bpow radix2 emax)). apply Rmult_le_compat. apply Rle_0_1. apply bpow_ge_0. - apply IZR_le. zify; omega. + apply IZR_le. zify; lia. eapply Rle_trans. eapply bpow_le. eassumption. apply bpow_log_pos; auto. apply generic_format_FLT. exists (Float radix2 1 emax). unfold F2R; simpl. ring. simpl. apply (Zpower_gt_1 radix2); auto. - simpl. unfold emin; red in prec_gt_0_; omega. + simpl. unfold emin; red in prec_gt_0_; lia. Qed. Lemma round_NE_underflows: @@ -1221,10 +1221,10 @@ Proof. assert (A: round radix2 fexp (round_mode mode_NE) eps = 0%R). { unfold round. simpl. assert (E: cexp radix2 fexp eps = emin). - { unfold cexp, eps. rewrite mag_bpow. unfold fexp, FLT_exp. zify; red in prec_gt_0_; omega. } + { unfold cexp, eps. rewrite mag_bpow. unfold fexp, FLT_exp. zify; red in prec_gt_0_; lia. } unfold scaled_mantissa; rewrite E. assert (P: (eps * bpow radix2 (-emin) = / 2)%R). - { unfold eps. rewrite <- bpow_plus. replace (emin - 1 + -emin) with (-1) by omega. auto. } + { unfold eps. rewrite <- bpow_plus. replace (emin - 1 + -emin) with (-1) by lia. auto. } rewrite P. unfold Znearest. assert (F: Zfloor (/ 2)%R = 0). { apply Zfloor_imp. simpl. lra. } @@ -1244,18 +1244,18 @@ Lemma round_integer_underflow: round radix2 fexp (round_mode mode_NE) (IZR (Zpos m) * bpow base e) = 0%R. Proof. intros. apply round_NE_underflows. split. -- apply Rmult_le_pos. apply IZR_le. zify; omega. apply bpow_ge_0. +- apply Rmult_le_pos. apply IZR_le. zify; lia. apply bpow_ge_0. - apply Rle_trans with (bpow radix2 (Z.log2_up (Z.pos m) + e * Z.log2 base)). + rewrite bpow_plus. apply Rmult_le_compat. - apply IZR_le; zify; omega. + apply IZR_le; zify; lia. apply bpow_ge_0. rewrite <- IZR_Zpower. apply IZR_le. destruct (Z.eq_dec (Z.pos m) 1). - rewrite e0. simpl. omega. - apply Z.log2_up_spec. zify; omega. + rewrite e0. simpl. lia. + apply Z.log2_up_spec. zify; lia. apply Z.log2_up_nonneg. apply bpow_log_neg. auto. -+ apply bpow_le. omega. ++ apply bpow_le. lia. Qed. (** Correctness of Bparse *) @@ -1281,20 +1281,20 @@ Proof. - (* e = Zpos e *) destruct (Z.ltb_spec (Z.pos e * Z.log2 (Z.pos b)) emax). + (* no overflow *) - rewrite pos_pow_spec. rewrite <- IZR_Zpower by (zify; omega). rewrite <- mult_IZR. + rewrite pos_pow_spec. rewrite <- IZR_Zpower by (zify; lia). rewrite <- mult_IZR. replace false with (Z.pos m * Z.pos b ^ Z.pos e 0. Proof. - unfold zwordsize, wordsize. generalize WS.wordsize_not_zero. omega. + unfold zwordsize, wordsize. generalize WS.wordsize_not_zero. lia. Qed. Remark modulus_power: modulus = two_p zwordsize. @@ -83,12 +83,12 @@ Qed. Remark modulus_gt_one: modulus > 1. Proof. rewrite modulus_power. apply Z.lt_gt. apply (two_p_monotone_strict 0). - generalize wordsize_pos; omega. + generalize wordsize_pos; lia. Qed. Remark modulus_pos: modulus > 0. Proof. - generalize modulus_gt_one; omega. + generalize modulus_gt_one; lia. Qed. Hint Resolve modulus_pos: ints. @@ -321,16 +321,16 @@ Proof. unfold half_modulus. rewrite modulus_power. set (ws1 := zwordsize - 1). replace (zwordsize) with (Z.succ ws1). - rewrite two_p_S. rewrite Z.mul_comm. apply Z_div_mult. omega. - unfold ws1. generalize wordsize_pos; omega. - unfold ws1. omega. + rewrite two_p_S. rewrite Z.mul_comm. apply Z_div_mult. lia. + unfold ws1. generalize wordsize_pos; lia. + unfold ws1. lia. Qed. Remark half_modulus_modulus: modulus = 2 * half_modulus. Proof. rewrite half_modulus_power. rewrite modulus_power. - rewrite <- two_p_S. apply f_equal. omega. - generalize wordsize_pos; omega. + rewrite <- two_p_S. apply f_equal. lia. + generalize wordsize_pos; lia. Qed. (** Relative positions, from greatest to smallest: @@ -346,38 +346,38 @@ Qed. Remark half_modulus_pos: half_modulus > 0. Proof. - rewrite half_modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega. + rewrite half_modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; lia. Qed. Remark min_signed_neg: min_signed < 0. Proof. - unfold min_signed. generalize half_modulus_pos. omega. + unfold min_signed. generalize half_modulus_pos. lia. Qed. Remark max_signed_pos: max_signed >= 0. Proof. - unfold max_signed. generalize half_modulus_pos. omega. + unfold max_signed. generalize half_modulus_pos. lia. Qed. Remark wordsize_max_unsigned: zwordsize <= max_unsigned. Proof. assert (zwordsize < modulus). rewrite modulus_power. apply two_p_strict. - generalize wordsize_pos. omega. - unfold max_unsigned. omega. + generalize wordsize_pos. lia. + unfold max_unsigned. lia. Qed. Remark two_wordsize_max_unsigned: 2 * zwordsize - 1 <= max_unsigned. Proof. assert (2 * zwordsize - 1 < modulus). - rewrite modulus_power. apply two_p_strict_2. generalize wordsize_pos; omega. - unfold max_unsigned; omega. + rewrite modulus_power. apply two_p_strict_2. generalize wordsize_pos; lia. + unfold max_unsigned; lia. Qed. Remark max_signed_unsigned: max_signed < max_unsigned. Proof. unfold max_signed, max_unsigned. rewrite half_modulus_modulus. - generalize half_modulus_pos. omega. + generalize half_modulus_pos. lia. Qed. Lemma unsigned_repr_eq: @@ -495,7 +495,7 @@ Qed. Theorem unsigned_range: forall i, 0 <= unsigned i < modulus. Proof. - destruct i. simpl. omega. + destruct i. simpl. lia. Qed. Hint Resolve unsigned_range: ints. @@ -503,7 +503,7 @@ Theorem unsigned_range_2: forall i, 0 <= unsigned i <= max_unsigned. Proof. intro; unfold max_unsigned. - generalize (unsigned_range i). omega. + generalize (unsigned_range i). lia. Qed. Hint Resolve unsigned_range_2: ints. @@ -513,16 +513,16 @@ Proof. intros. unfold signed. generalize (unsigned_range i). set (n := unsigned i). intros. case (zlt n half_modulus); intro. - unfold max_signed. generalize min_signed_neg. omega. + unfold max_signed. generalize min_signed_neg. lia. unfold min_signed, max_signed. - rewrite half_modulus_modulus in *. omega. + rewrite half_modulus_modulus in *. lia. Qed. Theorem repr_unsigned: forall i, repr (unsigned i) = i. Proof. destruct i; simpl. unfold repr. apply mkint_eq. - rewrite Z_mod_modulus_eq. apply Z.mod_small; omega. + rewrite Z_mod_modulus_eq. apply Z.mod_small; lia. Qed. Hint Resolve repr_unsigned: ints. @@ -545,7 +545,7 @@ Theorem unsigned_repr: forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z. Proof. intros. rewrite unsigned_repr_eq. - apply Z.mod_small. unfold max_unsigned in H. omega. + apply Z.mod_small. unfold max_unsigned in H. lia. Qed. Hint Resolve unsigned_repr: ints. @@ -554,25 +554,25 @@ Theorem signed_repr: Proof. intros. unfold signed. destruct (zle 0 z). replace (unsigned (repr z)) with z. - rewrite zlt_true. auto. unfold max_signed in H. omega. - symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega. + rewrite zlt_true. auto. unfold max_signed in H. lia. + symmetry. apply unsigned_repr. generalize max_signed_unsigned. lia. pose (z' := z + modulus). replace (repr z) with (repr z'). replace (unsigned (repr z')) with z'. - rewrite zlt_false. unfold z'. omega. + rewrite zlt_false. unfold z'. lia. unfold z'. unfold min_signed in H. - rewrite half_modulus_modulus. omega. + rewrite half_modulus_modulus. lia. symmetry. apply unsigned_repr. unfold z', max_unsigned. unfold min_signed, max_signed in H. - rewrite half_modulus_modulus. omega. - apply eqm_samerepr. unfold z'; red. exists 1. omega. + rewrite half_modulus_modulus. lia. + apply eqm_samerepr. unfold z'; red. exists 1. lia. Qed. Theorem signed_eq_unsigned: forall x, unsigned x <= max_signed -> signed x = unsigned x. Proof. intros. unfold signed. destruct (zlt (unsigned x) half_modulus). - auto. unfold max_signed in H. omegaContradiction. + auto. unfold max_signed in H. extlia. Qed. Theorem signed_positive: @@ -580,7 +580,7 @@ Theorem signed_positive: Proof. intros. unfold signed, max_signed. generalize (unsigned_range x) half_modulus_modulus half_modulus_pos; intros. - destruct (zlt (unsigned x) half_modulus); omega. + destruct (zlt (unsigned x) half_modulus); lia. Qed. (** ** Properties of zero, one, minus one *) @@ -592,11 +592,11 @@ Qed. Theorem unsigned_one: unsigned one = 1. Proof. - unfold one; rewrite unsigned_repr_eq. apply Z.mod_small. split. omega. + unfold one; rewrite unsigned_repr_eq. apply Z.mod_small. split. lia. unfold modulus. replace wordsize with (S(Init.Nat.pred wordsize)). rewrite two_power_nat_S. generalize (two_power_nat_pos (Init.Nat.pred wordsize)). - omega. - generalize wordsize_pos. unfold zwordsize. omega. + lia. + generalize wordsize_pos. unfold zwordsize. lia. Qed. Theorem unsigned_mone: unsigned mone = modulus - 1. @@ -604,25 +604,25 @@ Proof. unfold mone; rewrite unsigned_repr_eq. replace (-1) with ((modulus - 1) + (-1) * modulus). rewrite Z_mod_plus_full. apply Z.mod_small. - generalize modulus_pos. omega. omega. + generalize modulus_pos. lia. lia. Qed. Theorem signed_zero: signed zero = 0. Proof. - unfold signed. rewrite unsigned_zero. apply zlt_true. generalize half_modulus_pos; omega. + unfold signed. rewrite unsigned_zero. apply zlt_true. generalize half_modulus_pos; lia. Qed. Theorem signed_one: zwordsize > 1 -> signed one = 1. Proof. intros. unfold signed. rewrite unsigned_one. apply zlt_true. - change 1 with (two_p 0). rewrite half_modulus_power. apply two_p_monotone_strict. omega. + change 1 with (two_p 0). rewrite half_modulus_power. apply two_p_monotone_strict. lia. Qed. Theorem signed_mone: signed mone = -1. Proof. unfold signed. rewrite unsigned_mone. - rewrite zlt_false. omega. - rewrite half_modulus_modulus. generalize half_modulus_pos. omega. + rewrite zlt_false. lia. + rewrite half_modulus_modulus. generalize half_modulus_pos. lia. Qed. Theorem one_not_zero: one <> zero. @@ -636,7 +636,7 @@ Theorem unsigned_repr_wordsize: unsigned iwordsize = zwordsize. Proof. unfold iwordsize; rewrite unsigned_repr_eq. apply Z.mod_small. - generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. + generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; lia. Qed. (** ** Properties of equality *) @@ -695,7 +695,7 @@ Proof. Qed. Theorem add_commut: forall x y, add x y = add y x. -Proof. intros; unfold add. decEq. omega. Qed. +Proof. intros; unfold add. decEq. lia. Qed. Theorem add_zero: forall x, add x zero = x. Proof. @@ -729,7 +729,7 @@ Theorem add_neg_zero: forall x, add x (neg x) = zero. Proof. intros; unfold add, neg, zero. apply eqm_samerepr. replace 0 with (unsigned x + (- (unsigned x))). - auto with ints. omega. + auto with ints. lia. Qed. Theorem unsigned_add_carry: @@ -741,8 +741,8 @@ Proof. rewrite unsigned_repr_eq. generalize (unsigned_range x) (unsigned_range y). intros. destruct (zlt (unsigned x + unsigned y) modulus). - rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. - rewrite unsigned_one. apply Zmod_unique with 1. omega. omega. + rewrite unsigned_zero. apply Zmod_unique with 0. lia. lia. + rewrite unsigned_one. apply Zmod_unique with 1. lia. lia. Qed. Corollary unsigned_add_either: @@ -753,8 +753,8 @@ Proof. intros. rewrite unsigned_add_carry. unfold add_carry. rewrite unsigned_zero. rewrite Z.add_0_r. destruct (zlt (unsigned x + unsigned y) modulus). - rewrite unsigned_zero. left; omega. - rewrite unsigned_one. right; omega. + rewrite unsigned_zero. left; lia. + rewrite unsigned_one. right; lia. Qed. (** ** Properties of negation *) @@ -773,7 +773,7 @@ Theorem neg_involutive: forall x, neg (neg x) = x. Proof. intros; unfold neg. apply eqm_repr_eq. eapply eqm_trans. apply eqm_neg. - apply eqm_unsigned_repr_l. apply eqm_refl. apply eqm_refl2. omega. + apply eqm_unsigned_repr_l. apply eqm_refl. apply eqm_refl2. lia. Qed. Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y). @@ -783,7 +783,7 @@ Proof. auto with ints. replace (- (unsigned x + unsigned y)) with ((- unsigned x) + (- unsigned y)). - auto with ints. omega. + auto with ints. lia. Qed. (** ** Properties of subtraction *) @@ -791,7 +791,7 @@ Qed. Theorem sub_zero_l: forall x, sub x zero = x. Proof. intros; unfold sub. rewrite unsigned_zero. - replace (unsigned x - 0) with (unsigned x) by omega. apply repr_unsigned. + replace (unsigned x - 0) with (unsigned x) by lia. apply repr_unsigned. Qed. Theorem sub_zero_r: forall x, sub zero x = neg x. @@ -807,7 +807,7 @@ Qed. Theorem sub_idem: forall x, sub x x = zero. Proof. - intros; unfold sub. unfold zero. decEq. omega. + intros; unfold sub. unfold zero. decEq. lia. Qed. Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y. @@ -850,8 +850,8 @@ Proof. rewrite unsigned_repr_eq. generalize (unsigned_range x) (unsigned_range y). intros. destruct (zlt (unsigned x - unsigned y) 0). - rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega. - rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. + rewrite unsigned_one. apply Zmod_unique with (-1). lia. lia. + rewrite unsigned_zero. apply Zmod_unique with 0. lia. lia. Qed. (** ** Properties of multiplication *) @@ -878,9 +878,9 @@ Theorem mul_mone: forall x, mul x mone = neg x. Proof. intros; unfold mul, neg. rewrite unsigned_mone. apply eqm_samerepr. - replace (-unsigned x) with (0 - unsigned x) by omega. + replace (-unsigned x) with (0 - unsigned x) by lia. replace (unsigned x * (modulus - 1)) with (unsigned x * modulus - unsigned x) by ring. - apply eqm_sub. exists (unsigned x). omega. apply eqm_refl. + apply eqm_sub. exists (unsigned x). lia. apply eqm_refl. Qed. Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z). @@ -955,7 +955,7 @@ Proof. generalize (unsigned_range y); intro. assert (unsigned y <> 0). red; intro. elim H. rewrite <- (repr_unsigned y). unfold zero. congruence. - unfold y'. omega. + unfold y'. lia. auto with ints. Qed. @@ -1025,7 +1025,7 @@ Proof. assert (Z.quot x' one = x'). symmetry. apply Zquot_unique_full with 0. red. change (Z.abs one) with 1. - destruct (zle 0 x'). left. omega. right. omega. + destruct (zle 0 x'). left. lia. right. lia. unfold one; ring. congruence. Qed. @@ -1053,12 +1053,12 @@ Proof. assert (unsigned d <> 0). { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. } assert (0 < D). - { unfold D. generalize (unsigned_range d); intros. omega. } + { unfold D. generalize (unsigned_range d); intros. lia. } assert (0 <= Q <= max_unsigned). { unfold Q. apply Zdiv_interval_2. rewrite <- E1; apply unsigned_range_2. - omega. unfold max_unsigned; generalize modulus_pos; omega. omega. } - omega. + lia. unfold max_unsigned; generalize modulus_pos; lia. lia. } + lia. Qed. Lemma unsigned_signed: @@ -1067,8 +1067,8 @@ Proof. intros. unfold lt. rewrite signed_zero. unfold signed. generalize (unsigned_range n). rewrite half_modulus_modulus. intros. destruct (zlt (unsigned n) half_modulus). -- rewrite zlt_false by omega. auto. -- rewrite zlt_true by omega. ring. +- rewrite zlt_false by lia. auto. +- rewrite zlt_true by lia. ring. Qed. Theorem divmods2_divs_mods: @@ -1096,24 +1096,24 @@ Proof. - (* D = 1 *) rewrite e. rewrite Z.quot_1_r; auto. - (* D = -1 *) - rewrite e. change (-1) with (Z.opp 1). rewrite Z.quot_opp_r by omega. + rewrite e. change (-1) with (Z.opp 1). rewrite Z.quot_opp_r by lia. rewrite Z.quot_1_r. assert (N <> min_signed). { red; intros; destruct H0. + elim H0. rewrite <- (repr_signed n). rewrite <- H2. rewrite H4. auto. + elim H0. rewrite <- (repr_signed d). unfold D in e; rewrite e; auto. } - unfold min_signed, max_signed in *. omega. + unfold min_signed, max_signed in *. lia. - (* |D| > 1 *) assert (Z.abs (Z.quot N D) < half_modulus). - { rewrite <- Z.quot_abs by omega. apply Zquot_lt_upper_bound. - xomega. xomega. + { rewrite <- Z.quot_abs by lia. apply Zquot_lt_upper_bound. + extlia. extlia. apply Z.le_lt_trans with (half_modulus * 1). - rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega. - apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. } + rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; extlia. + apply Zmult_lt_compat_l. generalize half_modulus_pos; lia. extlia. } rewrite Z.abs_lt in H4. - unfold min_signed, max_signed; omega. + unfold min_signed, max_signed; lia. } - unfold proj_sumbool; rewrite ! zle_true by omega; simpl. + unfold proj_sumbool; rewrite ! zle_true by lia; simpl. unfold Q, R; rewrite H2; auto. Qed. @@ -1164,7 +1164,7 @@ Qed. Lemma bits_mone: forall i, 0 <= i < zwordsize -> testbit mone i = true. Proof. - intros. unfold mone. rewrite testbit_repr; auto. apply Ztestbit_m1. omega. + intros. unfold mone. rewrite testbit_repr; auto. apply Ztestbit_m1. lia. Qed. Hint Rewrite bits_zero bits_mone : ints. @@ -1181,7 +1181,7 @@ Proof. unfold zwordsize, ws1, wordsize. destruct WS.wordsize as [] eqn:E. elim WS.wordsize_not_zero; auto. - rewrite Nat2Z.inj_succ. simpl. omega. + rewrite Nat2Z.inj_succ. simpl. lia. assert (half_modulus = two_power_nat ws1). rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power. rewrite H; rewrite H0. @@ -1195,11 +1195,11 @@ Lemma bits_signed: Proof. intros. destruct (zlt i zwordsize). - - apply same_bits_eqm. apply eqm_signed_unsigned. omega. + - apply same_bits_eqm. apply eqm_signed_unsigned. lia. - unfold signed. rewrite sign_bit_of_unsigned. destruct (zlt (unsigned x) half_modulus). + apply Ztestbit_above with wordsize. apply unsigned_range. auto. + apply Ztestbit_above_neg with wordsize. - fold modulus. generalize (unsigned_range x). omega. auto. + fold modulus. generalize (unsigned_range x). lia. auto. Qed. Lemma bits_le: @@ -1207,9 +1207,9 @@ Lemma bits_le: (forall i, 0 <= i < zwordsize -> testbit x i = true -> testbit y i = true) -> unsigned x <= unsigned y. Proof. - intros. apply Ztestbit_le. generalize (unsigned_range y); omega. + intros. apply Ztestbit_le. generalize (unsigned_range y); lia. intros. fold (testbit y i). destruct (zlt i zwordsize). - apply H. omega. auto. + apply H. lia. auto. fold (testbit x i) in H1. rewrite bits_above in H1; auto. congruence. Qed. @@ -1477,10 +1477,10 @@ Lemma unsigned_not: forall x, unsigned (not x) = max_unsigned - unsigned x. Proof. intros. transitivity (unsigned (repr(-unsigned x - 1))). - f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega. + f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. lia. rewrite unsigned_repr_eq. apply Zmod_unique with (-1). - unfold max_unsigned. omega. - generalize (unsigned_range x). unfold max_unsigned. omega. + unfold max_unsigned. lia. + generalize (unsigned_range x). unfold max_unsigned. lia. Qed. Theorem not_neg: @@ -1490,9 +1490,9 @@ Proof. rewrite <- (repr_unsigned x) at 1. unfold add. rewrite !testbit_repr; auto. transitivity (Z.testbit (-unsigned x - 1) i). - symmetry. apply Z_one_complement. omega. + symmetry. apply Z_one_complement. lia. apply same_bits_eqm; auto. - replace (-unsigned x - 1) with (-unsigned x + (-1)) by omega. + replace (-unsigned x - 1) with (-unsigned x + (-1)) by lia. apply eqm_add. unfold neg. apply eqm_unsigned_repr. rewrite unsigned_mone. exists (-1). ring. @@ -1534,9 +1534,9 @@ Proof. replace (unsigned (xor b one)) with (1 - unsigned b). destruct (zlt (unsigned x - unsigned y - unsigned b)). rewrite zlt_true. rewrite xor_zero_l; auto. - unfold max_unsigned; omega. + unfold max_unsigned; lia. rewrite zlt_false. rewrite xor_idem; auto. - unfold max_unsigned; omega. + unfold max_unsigned; lia. destruct H; subst b. rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto. rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto. @@ -1555,16 +1555,16 @@ Proof. rewrite (Zdecomp x) in *. rewrite (Zdecomp y) in *. transitivity (Z.testbit (Zshiftin (Z.odd x || Z.odd y) (Z.div2 x + Z.div2 y)) i). - f_equal. rewrite !Zshiftin_spec. - exploit (EXCL 0). omega. rewrite !Ztestbit_shiftin_base. intros. + exploit (EXCL 0). lia. rewrite !Ztestbit_shiftin_base. intros. Opaque Z.mul. destruct (Z.odd x); destruct (Z.odd y); simpl in *; discriminate || ring. - rewrite !Ztestbit_shiftin; auto. destruct (zeq i 0). + auto. - + apply IND. omega. intros. - exploit (EXCL (Z.succ j)). omega. + + apply IND. lia. intros. + exploit (EXCL (Z.succ j)). lia. rewrite !Ztestbit_shiftin_succ. auto. - omega. omega. + lia. lia. Qed. Theorem add_is_or: @@ -1573,10 +1573,10 @@ Theorem add_is_or: add x y = or x y. Proof. bit_solve. unfold add. rewrite testbit_repr; auto. - apply Z_add_is_or. omega. + apply Z_add_is_or. lia. intros. assert (testbit (and x y) j = testbit zero j) by congruence. - autorewrite with ints in H2. assumption. omega. + autorewrite with ints in H2. assumption. lia. Qed. Theorem xor_is_or: @@ -1622,7 +1622,7 @@ Proof. intros. unfold shl. rewrite testbit_repr; auto. destruct (zlt i (unsigned y)). apply Z.shiftl_spec_low. auto. - apply Z.shiftl_spec_high. omega. omega. + apply Z.shiftl_spec_high. lia. lia. Qed. Lemma bits_shru: @@ -1636,7 +1636,7 @@ Proof. destruct (zlt (i + unsigned y) zwordsize). auto. apply bits_above; auto. - omega. + lia. Qed. Lemma bits_shr: @@ -1647,15 +1647,15 @@ Lemma bits_shr: Proof. intros. unfold shr. rewrite testbit_repr; auto. rewrite Z.shiftr_spec. apply bits_signed. - generalize (unsigned_range y); omega. - omega. + generalize (unsigned_range y); lia. + lia. Qed. Hint Rewrite bits_shl bits_shru bits_shr: ints. Theorem shl_zero: forall x, shl x zero = x. Proof. - bit_solve. rewrite unsigned_zero. rewrite zlt_false. f_equal; omega. omega. + bit_solve. rewrite unsigned_zero. rewrite zlt_false. f_equal; lia. lia. Qed. Lemma bitwise_binop_shl: @@ -1667,7 +1667,7 @@ Proof. intros. apply same_bits_eq; intros. rewrite H; auto. rewrite !bits_shl; auto. destruct (zlt i (unsigned n)); auto. - rewrite H; auto. generalize (unsigned_range n); omega. + rewrite H; auto. generalize (unsigned_range n); lia. Qed. Theorem and_shl: @@ -1695,7 +1695,7 @@ Lemma ltu_inv: forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y. Proof. unfold ltu; intros. destruct (zlt (unsigned x) (unsigned y)). - split; auto. generalize (unsigned_range x); omega. + split; auto. generalize (unsigned_range x); lia. discriminate. Qed. @@ -1716,15 +1716,15 @@ Proof. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. assert (unsigned (add y z) = unsigned y + unsigned z). unfold add. apply unsigned_repr. - generalize two_wordsize_max_unsigned; omega. + generalize two_wordsize_max_unsigned; lia. apply same_bits_eq; intros. rewrite bits_shl; auto. destruct (zlt i (unsigned z)). - - rewrite bits_shl; auto. rewrite zlt_true. auto. omega. + - rewrite bits_shl; auto. rewrite zlt_true. auto. lia. - rewrite bits_shl. destruct (zlt (i - unsigned z) (unsigned y)). - + rewrite bits_shl; auto. rewrite zlt_true. auto. omega. - + rewrite bits_shl; auto. rewrite zlt_false. f_equal. omega. omega. - + omega. + + rewrite bits_shl; auto. rewrite zlt_true. auto. lia. + + rewrite bits_shl; auto. rewrite zlt_false. f_equal. lia. lia. + + lia. Qed. Theorem sub_ltu: @@ -1734,12 +1734,12 @@ Theorem sub_ltu: Proof. intros. generalize (ltu_inv x y H). intros . - split. omega. omega. + split. lia. lia. Qed. Theorem shru_zero: forall x, shru x zero = x. Proof. - bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega. + bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; lia. lia. Qed. Lemma bitwise_binop_shru: @@ -1751,7 +1751,7 @@ Proof. intros. apply same_bits_eq; intros. rewrite H; auto. rewrite !bits_shru; auto. destruct (zlt (i + unsigned n) zwordsize); auto. - rewrite H; auto. generalize (unsigned_range n); omega. + rewrite H; auto. generalize (unsigned_range n); lia. Qed. Theorem and_shru: @@ -1786,20 +1786,20 @@ Proof. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. assert (unsigned (add y z) = unsigned y + unsigned z). unfold add. apply unsigned_repr. - generalize two_wordsize_max_unsigned; omega. + generalize two_wordsize_max_unsigned; lia. apply same_bits_eq; intros. rewrite bits_shru; auto. destruct (zlt (i + unsigned z) zwordsize). - rewrite bits_shru. destruct (zlt (i + unsigned z + unsigned y) zwordsize). - + rewrite bits_shru; auto. rewrite zlt_true. f_equal. omega. omega. - + rewrite bits_shru; auto. rewrite zlt_false. auto. omega. - + omega. - - rewrite bits_shru; auto. rewrite zlt_false. auto. omega. + + rewrite bits_shru; auto. rewrite zlt_true. f_equal. lia. lia. + + rewrite bits_shru; auto. rewrite zlt_false. auto. lia. + + lia. + - rewrite bits_shru; auto. rewrite zlt_false. auto. lia. Qed. Theorem shr_zero: forall x, shr x zero = x. Proof. - bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega. + bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; lia. lia. Qed. Lemma bitwise_binop_shr: @@ -1811,8 +1811,8 @@ Proof. rewrite H; auto. rewrite !bits_shr; auto. rewrite H; auto. destruct (zlt (i + unsigned n) zwordsize). - generalize (unsigned_range n); omega. - omega. + generalize (unsigned_range n); lia. + lia. Qed. Theorem and_shr: @@ -1847,15 +1847,15 @@ Proof. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. assert (unsigned (add y z) = unsigned y + unsigned z). unfold add. apply unsigned_repr. - generalize two_wordsize_max_unsigned; omega. + generalize two_wordsize_max_unsigned; lia. apply same_bits_eq; intros. rewrite !bits_shr; auto. f_equal. destruct (zlt (i + unsigned z) zwordsize). - rewrite H4. replace (i + (unsigned y + unsigned z)) with (i + unsigned z + unsigned y) by omega. auto. + rewrite H4. replace (i + (unsigned y + unsigned z)) with (i + unsigned z + unsigned y) by lia. auto. rewrite (zlt_false _ (i + unsigned (add y z))). - destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega. - omega. - destruct (zlt (i + unsigned z) zwordsize); omega. + destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); lia. + lia. + destruct (zlt (i + unsigned z) zwordsize); lia. Qed. Theorem and_shr_shru: @@ -1865,7 +1865,7 @@ Proof. intros. apply same_bits_eq; intros. rewrite bits_and; auto. rewrite bits_shr; auto. rewrite !bits_shru; auto. destruct (zlt (i + unsigned z) zwordsize). - - rewrite bits_and; auto. generalize (unsigned_range z); omega. + - rewrite bits_and; auto. generalize (unsigned_range z); lia. - apply andb_false_r. Qed. @@ -1891,17 +1891,17 @@ Proof. rewrite sign_bit_of_unsigned. unfold lt. rewrite signed_zero. unfold signed. destruct (zlt (unsigned x) half_modulus). - rewrite zlt_false. auto. generalize (unsigned_range x); omega. + rewrite zlt_false. auto. generalize (unsigned_range x); lia. rewrite zlt_true. unfold one; rewrite testbit_repr; auto. - generalize (unsigned_range x); omega. - omega. + generalize (unsigned_range x); lia. + lia. rewrite zlt_false. unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false. destruct (lt x zero). rewrite unsigned_one. simpl Z.div2. rewrite Z.testbit_0_l; auto. rewrite unsigned_zero. simpl Z.div2. rewrite Z.testbit_0_l; auto. - auto. omega. omega. - generalize wordsize_max_unsigned; omega. + auto. lia. lia. + generalize wordsize_max_unsigned; lia. Qed. Theorem shr_lt_zero: @@ -1912,13 +1912,13 @@ Proof. rewrite bits_shr; auto. rewrite unsigned_repr. transitivity (testbit x (zwordsize - 1)). - f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega. + f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); lia. rewrite sign_bit_of_unsigned. unfold lt. rewrite signed_zero. unfold signed. destruct (zlt (unsigned x) half_modulus). - rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega. - rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega. - generalize wordsize_max_unsigned; omega. + rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); lia. + rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); lia. + generalize wordsize_max_unsigned; lia. Qed. (** ** Properties of rotations *) @@ -1935,20 +1935,20 @@ Proof. exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. fold j. intros RANGE. rewrite testbit_repr; auto. - rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega. + rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: lia. destruct (zlt i j). - rewrite Z.shiftl_spec_low; auto. simpl. unfold testbit. f_equal. symmetry. apply Zmod_unique with (-k - 1). rewrite EQ. ring. - omega. + lia. - rewrite Z.shiftl_spec_high. fold (testbit x (i + (zwordsize - j))). rewrite bits_above. rewrite orb_false_r. fold (testbit x (i - j)). f_equal. symmetry. apply Zmod_unique with (-k). rewrite EQ. ring. - omega. omega. omega. omega. + lia. lia. lia. lia. Qed. Lemma bits_ror: @@ -1963,20 +1963,20 @@ Proof. exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. fold j. intros RANGE. rewrite testbit_repr; auto. - rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega. + rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: lia. destruct (zlt (i + j) zwordsize). - rewrite Z.shiftl_spec_low; auto. rewrite orb_false_r. unfold testbit. f_equal. symmetry. apply Zmod_unique with k. rewrite EQ. ring. - omega. omega. + lia. lia. - rewrite Z.shiftl_spec_high. fold (testbit x (i + j)). rewrite bits_above. simpl. unfold testbit. f_equal. symmetry. apply Zmod_unique with (k + 1). rewrite EQ. ring. - omega. omega. omega. omega. + lia. lia. lia. lia. Qed. Hint Rewrite bits_rol bits_ror: ints. @@ -1993,8 +1993,8 @@ Proof. - rewrite andb_false_r; auto. - generalize (unsigned_range n); intros. rewrite bits_mone. rewrite andb_true_r. f_equal. - symmetry. apply Z.mod_small. omega. - omega. + symmetry. apply Z.mod_small. lia. + lia. Qed. Theorem shru_rolm: @@ -2009,9 +2009,9 @@ Proof. - generalize (unsigned_range n); intros. rewrite bits_mone. rewrite andb_true_r. f_equal. unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize. - symmetry. apply Zmod_unique with (-1). ring. omega. - rewrite unsigned_repr_wordsize. generalize wordsize_max_unsigned. omega. - omega. + symmetry. apply Zmod_unique with (-1). ring. lia. + rewrite unsigned_repr_wordsize. generalize wordsize_max_unsigned. lia. + lia. - rewrite andb_false_r; auto. Qed. @@ -2065,11 +2065,11 @@ Proof. apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. apply wordsize_pos. apply eqmod_refl. - replace (i - M - N) with (i - (M + N)) by omega. + replace (i - M - N) with (i - (M + N)) by lia. apply eqmod_sub. apply eqmod_refl. apply eqmod_trans with (Z.modulo (unsigned n + unsigned m) zwordsize). - replace (M + N) with (N + M) by omega. apply eqmod_mod. apply wordsize_pos. + replace (M + N) with (N + M) by lia. apply eqmod_mod. apply wordsize_pos. unfold modu, add. fold M; fold N. rewrite unsigned_repr_wordsize. assert (forall a, eqmod zwordsize a (unsigned (repr a))). intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption. @@ -2116,7 +2116,7 @@ Proof. unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize. apply eqmod_mod_eq. apply wordsize_pos. exists 1. ring. rewrite unsigned_repr_wordsize. - generalize wordsize_pos; generalize wordsize_max_unsigned; omega. + generalize wordsize_pos; generalize wordsize_max_unsigned; lia. Qed. Theorem ror_rol_neg: @@ -2124,9 +2124,9 @@ Theorem ror_rol_neg: Proof. intros. apply same_bits_eq; intros. rewrite bits_ror by auto. rewrite bits_rol by auto. - f_equal. apply eqmod_mod_eq. omega. + f_equal. apply eqmod_mod_eq. lia. apply eqmod_trans with (i - (- unsigned y)). - apply eqmod_refl2; omega. + apply eqmod_refl2; lia. apply eqmod_sub. apply eqmod_refl. apply eqmod_divides with modulus. apply eqm_unsigned_repr. auto. @@ -2149,8 +2149,8 @@ Proof. assert (unsigned (add y z) = zwordsize). rewrite H1. apply unsigned_repr_wordsize. unfold add in H5. rewrite unsigned_repr in H5. - omega. - generalize two_wordsize_max_unsigned; omega. + lia. + generalize two_wordsize_max_unsigned; lia. - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. apply Z.mod_small; auto. Qed. @@ -2166,10 +2166,10 @@ Proof. destruct (Z_is_power2 (unsigned n)) as [i|] eqn:E; inv H. assert (0 <= i < zwordsize). { apply Z_is_power2_range with (unsigned n). - generalize wordsize_pos; omega. + generalize wordsize_pos; lia. rewrite <- modulus_power. apply unsigned_range. auto. } - rewrite unsigned_repr; auto. generalize wordsize_max_unsigned; omega. + rewrite unsigned_repr; auto. generalize wordsize_max_unsigned; lia. Qed. Lemma is_power2_rng: @@ -2203,10 +2203,10 @@ Remark two_p_range: 0 <= two_p n <= max_unsigned. Proof. intros. split. - assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega. + assert (two_p n > 0). apply two_p_gt_ZERO. lia. lia. generalize (two_p_monotone_strict _ _ H). unfold zwordsize; rewrite <- two_power_nat_two_p. - unfold max_unsigned, modulus. omega. + unfold max_unsigned, modulus. lia. Qed. Lemma is_power2_two_p: @@ -2214,7 +2214,7 @@ Lemma is_power2_two_p: is_power2 (repr (two_p n)) = Some (repr n). Proof. intros. unfold is_power2. rewrite unsigned_repr. - rewrite Z_is_power2_complete by omega; auto. + rewrite Z_is_power2_complete by lia; auto. apply two_p_range. auto. Qed. @@ -2228,7 +2228,7 @@ Lemma shl_mul_two_p: Proof. intros. unfold shl, mul. apply eqm_samerepr. rewrite Zshiftl_mul_two_p. auto with ints. - generalize (unsigned_range y); omega. + generalize (unsigned_range y); lia. Qed. Theorem shl_mul: @@ -2264,19 +2264,19 @@ Proof. rewrite shl_mul_two_p. unfold mul. apply eqm_unsigned_repr_l. apply eqm_mult; auto with ints. apply eqm_unsigned_repr_l. apply eqm_refl2. rewrite unsigned_repr. auto. - generalize wordsize_max_unsigned; omega. + generalize wordsize_max_unsigned; lia. - bit_solve. rewrite unsigned_repr. destruct (zlt i n). + auto. + replace (testbit y i) with false. apply andb_false_r. symmetry. unfold testbit. - assert (EQ: Z.of_nat (Z.to_nat n) = n) by (apply Z2Nat.id; omega). + assert (EQ: Z.of_nat (Z.to_nat n) = n) by (apply Z2Nat.id; lia). apply Ztestbit_above with (Z.to_nat n). rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0. - generalize (unsigned_range y); omega. + generalize (unsigned_range y); lia. rewrite EQ; auto. - + generalize wordsize_max_unsigned; omega. + + generalize wordsize_max_unsigned; lia. Qed. (** Unsigned right shifts and unsigned divisions by powers of 2. *) @@ -2287,7 +2287,7 @@ Lemma shru_div_two_p: Proof. intros. unfold shru. rewrite Zshiftr_div_two_p. auto. - generalize (unsigned_range y); omega. + generalize (unsigned_range y); lia. Qed. Theorem divu_pow2: @@ -2307,7 +2307,7 @@ Lemma shr_div_two_p: Proof. intros. unfold shr. rewrite Zshiftr_div_two_p. auto. - generalize (unsigned_range y); omega. + generalize (unsigned_range y); lia. Qed. Theorem divs_pow2: @@ -2360,24 +2360,24 @@ Proof. set (uy := unsigned y). assert (0 <= uy < zwordsize - 1). generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. - generalize wordsize_pos wordsize_max_unsigned; omega. + generalize wordsize_pos wordsize_max_unsigned; lia. rewrite shr_div_two_p. unfold shrx. unfold divs. assert (shl one y = repr (two_p uy)). transitivity (mul one (repr (two_p uy))). symmetry. apply mul_pow2. replace y with (repr uy). - apply is_power2_two_p. omega. apply repr_unsigned. + apply is_power2_two_p. lia. apply repr_unsigned. rewrite mul_commut. apply mul_one. - assert (two_p uy > 0). apply two_p_gt_ZERO. omega. + assert (two_p uy > 0). apply two_p_gt_ZERO. lia. assert (two_p uy < half_modulus). rewrite half_modulus_power. apply two_p_monotone_strict. auto. assert (two_p uy < modulus). - rewrite modulus_power. apply two_p_monotone_strict. omega. + rewrite modulus_power. apply two_p_monotone_strict. lia. assert (unsigned (shl one y) = two_p uy). - rewrite H1. apply unsigned_repr. unfold max_unsigned. omega. + rewrite H1. apply unsigned_repr. unfold max_unsigned. lia. assert (signed (shl one y) = two_p uy). rewrite H1. apply signed_repr. - unfold max_signed. generalize min_signed_neg. omega. + unfold max_signed. generalize min_signed_neg. lia. rewrite H6. rewrite Zquot_Zdiv; auto. unfold lt. rewrite signed_zero. @@ -2386,10 +2386,10 @@ Proof. assert (signed (sub (shl one y) one) = two_p uy - 1). unfold sub. rewrite H5. rewrite unsigned_one. apply signed_repr. - generalize min_signed_neg. unfold max_signed. omega. - rewrite H7. rewrite signed_repr. f_equal. f_equal. omega. + generalize min_signed_neg. unfold max_signed. lia. + rewrite H7. rewrite signed_repr. f_equal. f_equal. lia. generalize (signed_range x). intros. - assert (two_p uy - 1 <= max_signed). unfold max_signed. omega. omega. + assert (two_p uy - 1 <= max_signed). unfold max_signed. lia. lia. Qed. Theorem shrx_shr_2: @@ -2404,19 +2404,19 @@ Proof. generalize (unsigned_range y); fold uy; intros. assert (0 <= uy < zwordsize - 1). generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. - generalize wordsize_pos wordsize_max_unsigned; omega. + generalize wordsize_pos wordsize_max_unsigned; lia. assert (two_p uy < modulus). - rewrite modulus_power. apply two_p_monotone_strict. omega. + rewrite modulus_power. apply two_p_monotone_strict. lia. f_equal. rewrite shl_mul_two_p. fold uy. rewrite mul_commut. rewrite mul_one. unfold sub. rewrite unsigned_one. rewrite unsigned_repr. rewrite unsigned_repr_wordsize. fold uy. apply same_bits_eq; intros. rewrite bits_shru by auto. - rewrite testbit_repr by auto. rewrite Ztestbit_two_p_m1 by omega. - rewrite unsigned_repr by (generalize wordsize_max_unsigned; omega). + rewrite testbit_repr by auto. rewrite Ztestbit_two_p_m1 by lia. + rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia). destruct (zlt i uy). - rewrite zlt_true by omega. rewrite bits_mone by omega. auto. - rewrite zlt_false by omega. auto. - assert (two_p uy > 0) by (apply two_p_gt_ZERO; omega). unfold max_unsigned; omega. + rewrite zlt_true by lia. rewrite bits_mone by lia. auto. + rewrite zlt_false by lia. auto. + assert (two_p uy > 0) by (apply two_p_gt_ZERO; lia). unfold max_unsigned; lia. - replace (shru zero (sub iwordsize y)) with zero. rewrite add_zero; auto. bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto. @@ -2434,23 +2434,23 @@ Proof. set (uy := unsigned y). assert (0 <= uy < zwordsize - 1). generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. - generalize wordsize_pos wordsize_max_unsigned; omega. + generalize wordsize_pos wordsize_max_unsigned; lia. assert (shl one y = repr (two_p uy)). rewrite shl_mul_two_p. rewrite mul_commut. apply mul_one. assert (and x (sub (shl one y) one) = modu x (repr (two_p uy))). symmetry. rewrite H1. apply modu_and with (logn := y). rewrite is_power2_two_p. unfold uy. rewrite repr_unsigned. auto. - omega. + lia. rewrite H2. rewrite H1. repeat rewrite shr_div_two_p. fold sx. fold uy. - assert (two_p uy > 0). apply two_p_gt_ZERO. omega. + assert (two_p uy > 0). apply two_p_gt_ZERO. lia. assert (two_p uy < modulus). - rewrite modulus_power. apply two_p_monotone_strict. omega. + rewrite modulus_power. apply two_p_monotone_strict. lia. assert (two_p uy < half_modulus). rewrite half_modulus_power. apply two_p_monotone_strict. auto. assert (two_p uy < modulus). - rewrite modulus_power. apply two_p_monotone_strict. omega. + rewrite modulus_power. apply two_p_monotone_strict. lia. assert (sub (repr (two_p uy)) one = repr (two_p uy - 1)). unfold sub. apply eqm_samerepr. apply eqm_sub. apply eqm_sym; apply eqm_unsigned_repr. rewrite unsigned_one. apply eqm_refl. @@ -2463,17 +2463,17 @@ Proof. fold eqm. unfold sx. apply eqm_sym. apply eqm_signed_unsigned. unfold modulus. rewrite two_power_nat_two_p. exists (two_p (zwordsize - uy)). rewrite <- two_p_is_exp. - f_equal. fold zwordsize; omega. omega. omega. + f_equal. fold zwordsize; lia. lia. lia. rewrite H8. rewrite Zdiv_shift; auto. unfold add. apply eqm_samerepr. apply eqm_add. apply eqm_unsigned_repr. destruct (zeq (sx mod two_p uy) 0); simpl. rewrite unsigned_zero. apply eqm_refl. rewrite unsigned_one. apply eqm_refl. - generalize (Z_mod_lt (unsigned x) (two_p uy) H3). unfold max_unsigned. omega. - unfold max_unsigned; omega. - generalize (signed_range x). fold sx. intros. split. omega. unfold max_signed. omega. - generalize min_signed_neg. unfold max_signed. omega. + generalize (Z_mod_lt (unsigned x) (two_p uy) H3). unfold max_unsigned. lia. + unfold max_unsigned; lia. + generalize (signed_range x). fold sx. intros. split. lia. unfold max_signed. lia. + generalize min_signed_neg. unfold max_signed. lia. Qed. (** Connections between [shr] and [shru]. *) @@ -2492,14 +2492,14 @@ Lemma and_positive: forall x y, signed y >= 0 -> signed (and x y) >= 0. Proof. intros. - assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega. + assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; lia. generalize (sign_bit_of_unsigned y). rewrite zlt_true; auto. intros A. generalize (sign_bit_of_unsigned (and x y)). rewrite bits_and. rewrite A. rewrite andb_false_r. unfold signed. destruct (zlt (unsigned (and x y)) half_modulus). - intros. generalize (unsigned_range (and x y)); omega. + intros. generalize (unsigned_range (and x y)); lia. congruence. - generalize wordsize_pos; omega. + generalize wordsize_pos; lia. Qed. Theorem shr_and_is_shru_and: @@ -2526,7 +2526,7 @@ Lemma bits_sign_ext: testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1). Proof. intros. unfold sign_ext. - rewrite testbit_repr; auto. apply Zsign_ext_spec. omega. + rewrite testbit_repr; auto. apply Zsign_ext_spec. lia. Qed. Hint Rewrite bits_zero_ext bits_sign_ext: ints. @@ -2535,13 +2535,13 @@ Theorem zero_ext_above: forall n x, n >= zwordsize -> zero_ext n x = x. Proof. intros. apply same_bits_eq; intros. - rewrite bits_zero_ext. apply zlt_true. omega. omega. + rewrite bits_zero_ext. apply zlt_true. lia. lia. Qed. Theorem zero_ext_below: forall n x, n <= 0 -> zero_ext n x = zero. Proof. - intros. bit_solve. destruct (zlt i n); auto. apply bits_below; omega. omega. + intros. bit_solve. destruct (zlt i n); auto. apply bits_below; lia. lia. Qed. Theorem sign_ext_above: @@ -2549,13 +2549,13 @@ Theorem sign_ext_above: Proof. intros. apply same_bits_eq; intros. unfold sign_ext; rewrite testbit_repr; auto. - rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. + rewrite Zsign_ext_spec. rewrite zlt_true. auto. lia. lia. Qed. Theorem sign_ext_below: forall n x, n <= 0 -> sign_ext n x = zero. Proof. - intros. bit_solve. apply bits_below. destruct (zlt i n); omega. + intros. bit_solve. apply bits_below. destruct (zlt i n); lia. Qed. Theorem zero_ext_and: @@ -2577,8 +2577,8 @@ Proof. fold (testbit (zero_ext n x) i). destruct (zlt i zwordsize). rewrite bits_zero_ext; auto. - rewrite bits_above. rewrite zlt_false; auto. omega. omega. - omega. + rewrite bits_above. rewrite zlt_false; auto. lia. lia. + lia. Qed. Theorem zero_ext_widen: @@ -2586,7 +2586,7 @@ Theorem zero_ext_widen: zero_ext n' (zero_ext n x) = zero_ext n x. Proof. bit_solve. destruct (zlt i n). - apply zlt_true. omega. + apply zlt_true. lia. destruct (zlt i n'); auto. tauto. tauto. Qed. @@ -2599,9 +2599,9 @@ Proof. bit_solve. destruct (zlt i n'). auto. rewrite (zlt_false _ i n). - destruct (zlt (n' - 1) n); f_equal; omega. - omega. - destruct (zlt i n'); omega. + destruct (zlt (n' - 1) n); f_equal; lia. + lia. + destruct (zlt i n'); lia. apply sign_ext_above; auto. Qed. @@ -2613,8 +2613,8 @@ Proof. bit_solve. destruct (zlt i n'). auto. - rewrite !zlt_false. auto. omega. omega. omega. - destruct (zlt i n'); omega. + rewrite !zlt_false. auto. lia. lia. lia. + destruct (zlt i n'); lia. apply sign_ext_above; auto. Qed. @@ -2623,9 +2623,9 @@ Theorem zero_ext_narrow: zero_ext n (zero_ext n' x) = zero_ext n x. Proof. bit_solve. destruct (zlt i n). - apply zlt_true. omega. + apply zlt_true. lia. auto. - omega. omega. omega. + lia. lia. lia. Qed. Theorem sign_ext_narrow: @@ -2633,9 +2633,9 @@ Theorem sign_ext_narrow: sign_ext n (sign_ext n' x) = sign_ext n x. Proof. intros. destruct (zlt n zwordsize). - bit_solve. destruct (zlt i n); f_equal; apply zlt_true; omega. - destruct (zlt i n); omega. - rewrite (sign_ext_above n'). auto. omega. + bit_solve. destruct (zlt i n); f_equal; apply zlt_true; lia. + destruct (zlt i n); lia. + rewrite (sign_ext_above n'). auto. lia. Qed. Theorem zero_sign_ext_narrow: @@ -2645,21 +2645,21 @@ Proof. intros. destruct (zlt n' zwordsize). bit_solve. destruct (zlt i n); auto. - rewrite zlt_true; auto. omega. - omega. omega. + rewrite zlt_true; auto. lia. + lia. lia. rewrite sign_ext_above; auto. Qed. Theorem zero_ext_idem: forall n x, 0 <= n -> zero_ext n (zero_ext n x) = zero_ext n x. Proof. - intros. apply zero_ext_widen. omega. + intros. apply zero_ext_widen. lia. Qed. Theorem sign_ext_idem: forall n x, 0 < n -> sign_ext n (sign_ext n x) = sign_ext n x. Proof. - intros. apply sign_ext_widen. omega. + intros. apply sign_ext_widen. lia. Qed. Theorem sign_ext_zero_ext: @@ -2669,15 +2669,15 @@ Proof. bit_solve. destruct (zlt i n). rewrite zlt_true; auto. - rewrite zlt_true; auto. omega. - destruct (zlt i n); omega. + rewrite zlt_true; auto. lia. + destruct (zlt i n); lia. rewrite zero_ext_above; auto. Qed. Theorem zero_ext_sign_ext: forall n x, 0 < n -> zero_ext n (sign_ext n x) = zero_ext n x. Proof. - intros. apply zero_sign_ext_narrow. omega. + intros. apply zero_sign_ext_narrow. lia. Qed. Theorem sign_ext_equal_if_zero_equal: @@ -2700,21 +2700,21 @@ Proof. apply same_bits_eq; intros. rewrite bits_shru by auto. fold Z. destruct (zlt Z Y). - assert (A: unsigned (sub y z) = Y - Z). - { apply unsigned_repr. generalize wordsize_max_unsigned; omega. } - symmetry; rewrite bits_shl, A by omega. + { apply unsigned_repr. generalize wordsize_max_unsigned; lia. } + symmetry; rewrite bits_shl, A by lia. destruct (zlt (i + Z) zwordsize). -+ rewrite bits_shl by omega. fold Y. - destruct (zlt i (Y - Z)); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. - rewrite bits_zero_ext by omega. rewrite zlt_true by omega. f_equal; omega. -+ rewrite bits_zero_ext by omega. rewrite ! zlt_false by omega. auto. ++ rewrite bits_shl by lia. fold Y. + destruct (zlt i (Y - Z)); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. + rewrite bits_zero_ext by lia. rewrite zlt_true by lia. f_equal; lia. ++ rewrite bits_zero_ext by lia. rewrite ! zlt_false by lia. auto. - assert (A: unsigned (sub z y) = Z - Y). - { apply unsigned_repr. generalize wordsize_max_unsigned; omega. } - rewrite bits_zero_ext, bits_shru, A by omega. - destruct (zlt (i + Z) zwordsize); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. - rewrite bits_shl by omega. fold Y. + { apply unsigned_repr. generalize wordsize_max_unsigned; lia. } + rewrite bits_zero_ext, bits_shru, A by lia. + destruct (zlt (i + Z) zwordsize); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. + rewrite bits_shl by lia. fold Y. destruct (zlt (i + Z) Y). -+ rewrite zlt_false by omega. auto. -+ rewrite zlt_true by omega. f_equal; omega. ++ rewrite zlt_false by lia. auto. ++ rewrite zlt_true by lia. f_equal; lia. Qed. Corollary zero_ext_shru_shl: @@ -2725,11 +2725,11 @@ Corollary zero_ext_shru_shl: Proof. intros. assert (A: unsigned y = zwordsize - n). - { unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega. } + { unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. lia. } assert (B: ltu y iwordsize = true). - { unfold ltu; rewrite A, unsigned_repr_wordsize. apply zlt_true; omega. } - rewrite shru_shl by auto. unfold ltu; rewrite zlt_false by omega. - rewrite sub_idem, shru_zero. f_equal. rewrite A; omega. + { unfold ltu; rewrite A, unsigned_repr_wordsize. apply zlt_true; lia. } + rewrite shru_shl by auto. unfold ltu; rewrite zlt_false by lia. + rewrite sub_idem, shru_zero. f_equal. rewrite A; lia. Qed. Theorem shr_shl: @@ -2741,26 +2741,26 @@ Proof. intros. apply ltu_iwordsize_inv in H; apply ltu_iwordsize_inv in H0. unfold ltu. set (Y := unsigned y) in *; set (Z := unsigned z) in *. apply same_bits_eq; intros. rewrite bits_shr by auto. fold Z. - rewrite bits_shl by (destruct (zlt (i + Z) zwordsize); omega). fold Y. + rewrite bits_shl by (destruct (zlt (i + Z) zwordsize); lia). fold Y. destruct (zlt Z Y). - assert (A: unsigned (sub y z) = Y - Z). - { apply unsigned_repr. generalize wordsize_max_unsigned; omega. } - rewrite bits_shl, A by omega. + { apply unsigned_repr. generalize wordsize_max_unsigned; lia. } + rewrite bits_shl, A by lia. destruct (zlt i (Y - Z)). -+ apply zlt_true. destruct (zlt (i + Z) zwordsize); omega. -+ rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega). - rewrite bits_sign_ext by omega. f_equal. ++ apply zlt_true. destruct (zlt (i + Z) zwordsize); lia. ++ rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); lia). + rewrite bits_sign_ext by lia. f_equal. destruct (zlt (i + Z) zwordsize). - rewrite zlt_true by omega. omega. - rewrite zlt_false by omega. omega. + rewrite zlt_true by lia. lia. + rewrite zlt_false by lia. lia. - assert (A: unsigned (sub z y) = Z - Y). - { apply unsigned_repr. generalize wordsize_max_unsigned; omega. } - rewrite bits_sign_ext by omega. - rewrite bits_shr by (destruct (zlt i (zwordsize - Z)); omega). - rewrite A. rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega). + { apply unsigned_repr. generalize wordsize_max_unsigned; lia. } + rewrite bits_sign_ext by lia. + rewrite bits_shr by (destruct (zlt i (zwordsize - Z)); lia). + rewrite A. rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); lia). f_equal. destruct (zlt i (zwordsize - Z)). -+ rewrite ! zlt_true by omega. omega. -+ rewrite ! zlt_false by omega. rewrite zlt_true by omega. omega. ++ rewrite ! zlt_true by lia. lia. ++ rewrite ! zlt_false by lia. rewrite zlt_true by lia. lia. Qed. Corollary sign_ext_shr_shl: @@ -2771,11 +2771,11 @@ Corollary sign_ext_shr_shl: Proof. intros. assert (A: unsigned y = zwordsize - n). - { unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega. } + { unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. lia. } assert (B: ltu y iwordsize = true). - { unfold ltu; rewrite A, unsigned_repr_wordsize. apply zlt_true; omega. } - rewrite shr_shl by auto. unfold ltu; rewrite zlt_false by omega. - rewrite sub_idem, shr_zero. f_equal. rewrite A; omega. + { unfold ltu; rewrite A, unsigned_repr_wordsize. apply zlt_true; lia. } + rewrite shr_shl by auto. unfold ltu; rewrite zlt_false by lia. + rewrite sub_idem, shr_zero. f_equal. rewrite A; lia. Qed. (** [zero_ext n x] is the unique integer congruent to [x] modulo [2^n] @@ -2784,14 +2784,14 @@ Qed. Lemma zero_ext_range: forall n x, 0 <= n < zwordsize -> 0 <= unsigned (zero_ext n x) < two_p n. Proof. - intros. rewrite zero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. omega. + intros. rewrite zero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. lia. Qed. Lemma eqmod_zero_ext: forall n x, 0 <= n < zwordsize -> eqmod (two_p n) (unsigned (zero_ext n x)) (unsigned x). Proof. intros. rewrite zero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod. - apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. Qed. (** [sign_ext n x] is the unique integer congruent to [x] modulo [2^n] @@ -2802,26 +2802,26 @@ Lemma sign_ext_range: Proof. intros. rewrite sign_ext_shr_shl; auto. set (X := shl x (repr (zwordsize - n))). - assert (two_p (n - 1) > 0) by (apply two_p_gt_ZERO; omega). + assert (two_p (n - 1) > 0) by (apply two_p_gt_ZERO; lia). assert (unsigned (repr (zwordsize - n)) = zwordsize - n). apply unsigned_repr. - split. omega. generalize wordsize_max_unsigned; omega. + split. lia. generalize wordsize_max_unsigned; lia. rewrite shr_div_two_p. rewrite signed_repr. rewrite H1. apply Zdiv_interval_1. - omega. omega. apply two_p_gt_ZERO; omega. + lia. lia. apply two_p_gt_ZERO; lia. replace (- two_p (n - 1) * two_p (zwordsize - n)) with (- (two_p (n - 1) * two_p (zwordsize - n))) by ring. rewrite <- two_p_is_exp. - replace (n - 1 + (zwordsize - n)) with (zwordsize - 1) by omega. + replace (n - 1 + (zwordsize - n)) with (zwordsize - 1) by lia. rewrite <- half_modulus_power. - generalize (signed_range X). unfold min_signed, max_signed. omega. - omega. omega. + generalize (signed_range X). unfold min_signed, max_signed. lia. + lia. lia. apply Zdiv_interval_2. apply signed_range. - generalize min_signed_neg; omega. - generalize max_signed_pos; omega. - rewrite H1. apply two_p_gt_ZERO. omega. + generalize min_signed_neg; lia. + generalize max_signed_pos; lia. + rewrite H1. apply two_p_gt_ZERO. lia. Qed. Lemma eqmod_sign_ext': @@ -2830,12 +2830,12 @@ Lemma eqmod_sign_ext': Proof. intros. set (N := Z.to_nat n). - assert (Z.of_nat N = n) by (apply Z2Nat.id; omega). + assert (Z.of_nat N = n) by (apply Z2Nat.id; lia). rewrite <- H0. rewrite <- two_power_nat_two_p. apply eqmod_same_bits; intros. rewrite H0 in H1. rewrite H0. fold (testbit (sign_ext n x) i). rewrite bits_sign_ext. - rewrite zlt_true. auto. omega. omega. + rewrite zlt_true. auto. lia. lia. Qed. Lemma eqmod_sign_ext: @@ -2846,7 +2846,7 @@ Proof. apply eqmod_divides with modulus. apply eqm_signed_unsigned. exists (two_p (zwordsize - n)). unfold modulus. rewrite two_power_nat_two_p. fold zwordsize. - rewrite <- two_p_is_exp. f_equal. omega. omega. omega. + rewrite <- two_p_is_exp. f_equal. lia. lia. lia. apply eqmod_sign_ext'; auto. Qed. @@ -2857,11 +2857,11 @@ Lemma shl_zero_ext: shl (zero_ext n x) m = zero_ext (n + unsigned m) (shl x m). Proof. intros. apply same_bits_eq; intros. - rewrite bits_zero_ext, ! bits_shl by omega. + rewrite bits_zero_ext, ! bits_shl by lia. destruct (zlt i (unsigned m)). -- rewrite zlt_true by omega; auto. -- rewrite bits_zero_ext by omega. - destruct (zlt (i - unsigned m) n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. +- rewrite zlt_true by lia; auto. +- rewrite bits_zero_ext by lia. + destruct (zlt (i - unsigned m) n); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. Qed. Lemma shl_sign_ext: @@ -2870,12 +2870,12 @@ Lemma shl_sign_ext: Proof. intros. generalize (unsigned_range m); intros. apply same_bits_eq; intros. - rewrite bits_sign_ext, ! bits_shl by omega. + rewrite bits_sign_ext, ! bits_shl by lia. destruct (zlt i (n + unsigned m)). - rewrite bits_shl by auto. destruct (zlt i (unsigned m)); auto. - rewrite bits_sign_ext by omega. f_equal. apply zlt_true. omega. -- rewrite zlt_false by omega. rewrite bits_shl by omega. rewrite zlt_false by omega. - rewrite bits_sign_ext by omega. f_equal. rewrite zlt_false by omega. omega. + rewrite bits_sign_ext by lia. f_equal. apply zlt_true. lia. +- rewrite zlt_false by lia. rewrite bits_shl by lia. rewrite zlt_false by lia. + rewrite bits_sign_ext by lia. f_equal. rewrite zlt_false by lia. lia. Qed. Lemma shru_zero_ext: @@ -2884,10 +2884,10 @@ Lemma shru_zero_ext: Proof. intros. bit_solve. - destruct (zlt (i + unsigned m) zwordsize). -* destruct (zlt i n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. +* destruct (zlt i n); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. * destruct (zlt i n); auto. -- generalize (unsigned_range m); omega. -- omega. +- generalize (unsigned_range m); lia. +- lia. Qed. Lemma shru_zero_ext_0: @@ -2896,8 +2896,8 @@ Lemma shru_zero_ext_0: Proof. intros. bit_solve. - destruct (zlt (i + unsigned m) zwordsize); auto. - apply zlt_false. omega. -- generalize (unsigned_range m); omega. + apply zlt_false. lia. +- generalize (unsigned_range m); lia. Qed. Lemma shr_sign_ext: @@ -2910,12 +2910,12 @@ Proof. rewrite bits_sign_ext, bits_shr. - f_equal. destruct (zlt i n), (zlt (i + unsigned m) zwordsize). -+ apply zlt_true; omega. -+ apply zlt_true; omega. -+ rewrite zlt_false by omega. rewrite zlt_true by omega. omega. -+ rewrite zlt_false by omega. rewrite zlt_true by omega. omega. -- destruct (zlt i n); omega. -- destruct (zlt (i + unsigned m) zwordsize); omega. ++ apply zlt_true; lia. ++ apply zlt_true; lia. ++ rewrite zlt_false by lia. rewrite zlt_true by lia. lia. ++ rewrite zlt_false by lia. rewrite zlt_true by lia. lia. +- destruct (zlt i n); lia. +- destruct (zlt (i + unsigned m) zwordsize); lia. Qed. Lemma zero_ext_shru_min: @@ -2924,10 +2924,10 @@ Lemma zero_ext_shru_min: Proof. intros. apply ltu_iwordsize_inv in H. apply Z.min_case_strong; intros; auto. - bit_solve; try omega. + bit_solve; try lia. destruct (zlt i (zwordsize - unsigned n)). - rewrite zlt_true by omega. auto. - destruct (zlt i s); auto. rewrite zlt_false by omega; auto. + rewrite zlt_true by lia. auto. + destruct (zlt i s); auto. rewrite zlt_false by lia; auto. Qed. Lemma sign_ext_shr_min: @@ -2939,12 +2939,12 @@ Proof. destruct (Z.min_spec (zwordsize - unsigned n) s) as [[A B] | [A B]]; rewrite B; auto. apply same_bits_eq; intros. rewrite ! bits_sign_ext by auto. destruct (zlt i (zwordsize - unsigned n)). - rewrite zlt_true by omega. auto. + rewrite zlt_true by lia. auto. assert (C: testbit (shr x n) (zwordsize - unsigned n - 1) = testbit x (zwordsize - 1)). - { rewrite bits_shr by omega. rewrite zlt_true by omega. f_equal; omega. } - rewrite C. destruct (zlt i s); rewrite bits_shr by omega. - rewrite zlt_false by omega. auto. - rewrite zlt_false by omega. auto. + { rewrite bits_shr by lia. rewrite zlt_true by lia. f_equal; lia. } + rewrite C. destruct (zlt i s); rewrite bits_shr by lia. + rewrite zlt_false by lia. auto. + rewrite zlt_false by lia. auto. Qed. Lemma shl_zero_ext_min: @@ -2955,10 +2955,10 @@ Proof. apply Z.min_case_strong; intros; auto. apply same_bits_eq; intros. rewrite ! bits_shl by auto. destruct (zlt i (unsigned n)); auto. - rewrite ! bits_zero_ext by omega. + rewrite ! bits_zero_ext by lia. destruct (zlt (i - unsigned n) s). - rewrite zlt_true by omega; auto. - rewrite zlt_false by omega; auto. + rewrite zlt_true by lia; auto. + rewrite zlt_false by lia; auto. Qed. Lemma shl_sign_ext_min: @@ -2970,10 +2970,10 @@ Proof. destruct (Z.min_spec (zwordsize - unsigned n) s) as [[A B] | [A B]]; rewrite B; auto. apply same_bits_eq; intros. rewrite ! bits_shl by auto. destruct (zlt i (unsigned n)); auto. - rewrite ! bits_sign_ext by omega. f_equal. + rewrite ! bits_sign_ext by lia. f_equal. destruct (zlt (i - unsigned n) s). - rewrite zlt_true by omega; auto. - omegaContradiction. + rewrite zlt_true by lia; auto. + extlia. Qed. (** ** Properties of [one_bits] (decomposition in sum of powers of two) *) @@ -2984,8 +2984,8 @@ Proof. assert (A: forall p, 0 <= p < zwordsize -> ltu (repr p) iwordsize = true). intros. unfold ltu, iwordsize. apply zlt_true. repeat rewrite unsigned_repr. tauto. - generalize wordsize_max_unsigned; omega. - generalize wordsize_max_unsigned; omega. + generalize wordsize_max_unsigned; lia. + generalize wordsize_max_unsigned; lia. unfold one_bits. intros. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. subst i. apply A. apply Z_one_bits_range with (unsigned x); auto. @@ -3015,7 +3015,7 @@ Proof. rewrite mul_one. apply eqm_unsigned_repr_r. rewrite unsigned_repr. auto with ints. generalize (H a (in_eq _ _)). change (Z.of_nat wordsize) with zwordsize. - generalize wordsize_max_unsigned. omega. + generalize wordsize_max_unsigned. lia. auto with ints. intros; apply H; auto with coqlib. Qed. @@ -3059,7 +3059,7 @@ Proof. apply eqm_sub. apply eqm_trans with (unsigned (repr (unsigned x + unsigned d))). eauto with ints. apply eqm_trans with (unsigned (repr (unsigned y + unsigned d))). eauto with ints. eauto with ints. eauto with ints. - omega. omega. + lia. lia. Qed. Lemma translate_ltu: @@ -3070,8 +3070,8 @@ Lemma translate_ltu: Proof. intros. unfold add. unfold ltu. repeat rewrite unsigned_repr; auto. case (zlt (unsigned x) (unsigned y)); intro. - apply zlt_true. omega. - apply zlt_false. omega. + apply zlt_true. lia. + apply zlt_false. lia. Qed. Theorem translate_cmpu: @@ -3092,8 +3092,8 @@ Lemma translate_lt: Proof. intros. repeat rewrite add_signed. unfold lt. repeat rewrite signed_repr; auto. case (zlt (signed x) (signed y)); intro. - apply zlt_true. omega. - apply zlt_false. omega. + apply zlt_true. lia. + apply zlt_false. lia. Qed. Theorem translate_cmp: @@ -3129,7 +3129,7 @@ Proof. intros. unfold ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate. rewrite signed_eq_unsigned. - generalize (unsigned_range x). omega. omega. + generalize (unsigned_range x). lia. lia. Qed. Theorem lt_sub_overflow: @@ -3143,30 +3143,30 @@ Proof. unfold min_signed, max_signed in *. generalize half_modulus_pos half_modulus_modulus; intros HM MM. destruct (zle 0 (X - Y)). -- unfold proj_sumbool at 1; rewrite zle_true at 1 by omega. simpl. - rewrite (zlt_false _ X) by omega. +- unfold proj_sumbool at 1; rewrite zle_true at 1 by lia. simpl. + rewrite (zlt_false _ X) by lia. destruct (zlt (X - Y) half_modulus). - + unfold proj_sumbool; rewrite zle_true by omega. - rewrite signed_repr. rewrite zlt_false by omega. apply xor_idem. - unfold min_signed, max_signed; omega. - + unfold proj_sumbool; rewrite zle_false by omega. + + unfold proj_sumbool; rewrite zle_true by lia. + rewrite signed_repr. rewrite zlt_false by lia. apply xor_idem. + unfold min_signed, max_signed; lia. + + unfold proj_sumbool; rewrite zle_false by lia. replace (signed (repr (X - Y))) with (X - Y - modulus). - rewrite zlt_true by omega. apply xor_idem. + rewrite zlt_true by lia. apply xor_idem. rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y). rewrite zlt_false; auto. - symmetry. apply Zmod_unique with 0; omega. -- unfold proj_sumbool at 2. rewrite zle_true at 1 by omega. rewrite andb_true_r. - rewrite (zlt_true _ X) by omega. + symmetry. apply Zmod_unique with 0; lia. +- unfold proj_sumbool at 2. rewrite zle_true at 1 by lia. rewrite andb_true_r. + rewrite (zlt_true _ X) by lia. destruct (zlt (X - Y) (-half_modulus)). - + unfold proj_sumbool; rewrite zle_false by omega. + + unfold proj_sumbool; rewrite zle_false by lia. replace (signed (repr (X - Y))) with (X - Y + modulus). - rewrite zlt_false by omega. apply xor_zero. + rewrite zlt_false by lia. apply xor_zero. rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus). - rewrite zlt_true by omega; auto. - symmetry. apply Zmod_unique with (-1); omega. - + unfold proj_sumbool; rewrite zle_true by omega. - rewrite signed_repr. rewrite zlt_true by omega. apply xor_zero_l. - unfold min_signed, max_signed; omega. + rewrite zlt_true by lia; auto. + symmetry. apply Zmod_unique with (-1); lia. + + unfold proj_sumbool; rewrite zle_true by lia. + rewrite signed_repr. rewrite zlt_true by lia. apply xor_zero_l. + unfold min_signed, max_signed; lia. Qed. Lemma signed_eq: @@ -3186,10 +3186,10 @@ Lemma not_lt: Proof. intros. unfold lt. rewrite signed_eq. unfold proj_sumbool. destruct (zlt (signed y) (signed x)). - rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + rewrite zlt_false. rewrite zeq_false. auto. lia. lia. destruct (zeq (signed x) (signed y)). - rewrite zlt_false. auto. omega. - rewrite zlt_true. auto. omega. + rewrite zlt_false. auto. lia. + rewrite zlt_true. auto. lia. Qed. Lemma lt_not: @@ -3203,10 +3203,10 @@ Lemma not_ltu: Proof. intros. unfold ltu, eq. destruct (zlt (unsigned y) (unsigned x)). - rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + rewrite zlt_false. rewrite zeq_false. auto. lia. lia. destruct (zeq (unsigned x) (unsigned y)). - rewrite zlt_false. auto. omega. - rewrite zlt_true. auto. omega. + rewrite zlt_false. auto. lia. + rewrite zlt_true. auto. lia. Qed. Lemma ltu_not: @@ -3238,7 +3238,7 @@ Proof. clear H3. generalize (unsigned_range ofs1) (unsigned_range ofs2). intros P Q. generalize (unsigned_add_either base ofs1) (unsigned_add_either base ofs2). - intros [C|C] [D|D]; omega. + intros [C|C] [D|D]; lia. Qed. (** ** Size of integers, in bits. *) @@ -3255,14 +3255,14 @@ Theorem bits_size_1: Proof. intros. destruct (zeq (unsigned x) 0). left. rewrite <- (repr_unsigned x). rewrite e; auto. - right. apply Ztestbit_size_1. generalize (unsigned_range x); omega. + right. apply Ztestbit_size_1. generalize (unsigned_range x); lia. Qed. Theorem bits_size_2: forall x i, size x <= i -> testbit x i = false. Proof. - intros. apply Ztestbit_size_2. generalize (unsigned_range x); omega. - fold (size x); omega. + intros. apply Ztestbit_size_2. generalize (unsigned_range x); lia. + fold (size x); lia. Qed. Theorem size_range: @@ -3270,9 +3270,9 @@ Theorem size_range: Proof. intros; split. apply Zsize_pos. destruct (bits_size_1 x). - subst x; unfold size; rewrite unsigned_zero; simpl. generalize wordsize_pos; omega. + subst x; unfold size; rewrite unsigned_zero; simpl. generalize wordsize_pos; lia. destruct (zle (size x) zwordsize); auto. - rewrite bits_above in H. congruence. omega. + rewrite bits_above in H. congruence. lia. Qed. Theorem bits_size_3: @@ -3285,7 +3285,7 @@ Proof. destruct (bits_size_1 x). subst x. unfold size; rewrite unsigned_zero; assumption. rewrite (H0 (Z.pred (size x))) in H1. congruence. - generalize (size_range x); omega. + generalize (size_range x); lia. Qed. Theorem bits_size_4: @@ -3299,14 +3299,14 @@ Proof. assert (size x <= n). apply bits_size_3; auto. destruct (zlt (size x) n). - rewrite bits_size_2 in H0. congruence. omega. - omega. + rewrite bits_size_2 in H0. congruence. lia. + lia. Qed. Theorem size_interval_1: forall x, 0 <= unsigned x < two_p (size x). Proof. - intros; apply Zsize_interval_1. generalize (unsigned_range x); omega. + intros; apply Zsize_interval_1. generalize (unsigned_range x); lia. Qed. Theorem size_interval_2: @@ -3320,9 +3320,9 @@ Theorem size_and: Proof. intros. assert (0 <= Z.min (size a) (size b)). - generalize (size_range a) (size_range b). zify; omega. + generalize (size_range a) (size_range b). zify; lia. apply bits_size_3. auto. intros. - rewrite bits_and by omega. + rewrite bits_and by lia. rewrite andb_false_iff. generalize (bits_size_2 a i). generalize (bits_size_2 b i). @@ -3335,9 +3335,9 @@ Proof. intros. generalize (size_interval_1 (and a b)); intros. assert (two_p (size (and a b)) <= two_p (Z.min (size a) (size b))). - apply two_p_monotone. split. generalize (size_range (and a b)); omega. + apply two_p_monotone. split. generalize (size_range (and a b)); lia. apply size_and. - omega. + lia. Qed. Theorem size_or: @@ -3345,17 +3345,17 @@ Theorem size_or: Proof. intros. generalize (size_range a) (size_range b); intros. destruct (bits_size_1 a). - subst a. rewrite size_zero. rewrite or_zero_l. zify; omega. + subst a. rewrite size_zero. rewrite or_zero_l. zify; lia. destruct (bits_size_1 b). - subst b. rewrite size_zero. rewrite or_zero. zify; omega. + subst b. rewrite size_zero. rewrite or_zero. zify; lia. zify. destruct H3 as [[P Q] | [P Q]]; subst. apply bits_size_4. tauto. rewrite bits_or. rewrite H2. apply orb_true_r. - omega. - intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. + lia. + intros. rewrite bits_or. rewrite !bits_size_2. auto. lia. lia. lia. apply bits_size_4. tauto. rewrite bits_or. rewrite H1. apply orb_true_l. destruct (zeq (size a) 0). unfold testbit in H1. rewrite Z.testbit_neg_r in H1. - congruence. omega. omega. - intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. + congruence. lia. lia. + intros. rewrite bits_or. rewrite !bits_size_2. auto. lia. lia. lia. Qed. Corollary or_interval: @@ -3369,12 +3369,12 @@ Theorem size_xor: Proof. intros. assert (0 <= Z.max (size a) (size b)). - generalize (size_range a) (size_range b). zify; omega. + generalize (size_range a) (size_range b). zify; lia. apply bits_size_3. auto. intros. rewrite bits_xor. rewrite !bits_size_2. auto. - zify; omega. - zify; omega. - omega. + zify; lia. + zify; lia. + lia. Qed. Corollary xor_interval: @@ -3383,9 +3383,9 @@ Proof. intros. generalize (size_interval_1 (xor a b)); intros. assert (two_p (size (xor a b)) <= two_p (Z.max (size a) (size b))). - apply two_p_monotone. split. generalize (size_range (xor a b)); omega. + apply two_p_monotone. split. generalize (size_range (xor a b)); lia. apply size_xor. - omega. + lia. Qed. End Make. @@ -3465,7 +3465,7 @@ Proof. intros. unfold shl'. rewrite testbit_repr; auto. destruct (zlt i (Int.unsigned y)). apply Z.shiftl_spec_low. auto. - apply Z.shiftl_spec_high. omega. omega. + apply Z.shiftl_spec_high. lia. lia. Qed. Lemma bits_shru': @@ -3479,7 +3479,7 @@ Proof. destruct (zlt (i + Int.unsigned y) zwordsize). auto. apply bits_above; auto. - omega. + lia. Qed. Lemma bits_shr': @@ -3490,8 +3490,8 @@ Lemma bits_shr': Proof. intros. unfold shr'. rewrite testbit_repr; auto. rewrite Z.shiftr_spec. apply bits_signed. - generalize (Int.unsigned_range y); omega. - omega. + generalize (Int.unsigned_range y); lia. + lia. Qed. Lemma shl'_mul_two_p: @@ -3500,7 +3500,7 @@ Lemma shl'_mul_two_p: Proof. intros. unfold shl', mul. apply eqm_samerepr. rewrite Zshiftl_mul_two_p. apply eqm_mult. apply eqm_refl. apply eqm_unsigned_repr. - generalize (Int.unsigned_range y); omega. + generalize (Int.unsigned_range y); lia. Qed. Lemma shl'_one_two_p: @@ -3551,7 +3551,7 @@ Proof. intros. apply Int.ltu_inv in H. change (Int.unsigned (Int.repr 63)) with 63 in H. set (y1 := Int64.repr (Int.unsigned y)). assert (U: unsigned y1 = Int.unsigned y). - { apply unsigned_repr. assert (63 < max_unsigned) by reflexivity. omega. } + { apply unsigned_repr. assert (63 < max_unsigned) by reflexivity. lia. } transitivity (shrx x y1). - unfold shrx', shrx, shl', shl. rewrite U; auto. - rewrite shrx_carry. @@ -3572,20 +3572,20 @@ Proof. assert (N1: 63 < max_unsigned) by reflexivity. assert (N2: 63 < Int.max_unsigned) by reflexivity. assert (A: unsigned z = Int.unsigned y). - { unfold z; apply unsigned_repr; omega. } + { unfold z; apply unsigned_repr; lia. } assert (B: unsigned (sub (repr 64) z) = Int.unsigned (Int.sub (Int.repr 64) y)). { unfold z. unfold sub, Int.sub. change (unsigned (repr 64)) with 64. change (Int.unsigned (Int.repr 64)) with 64. - rewrite (unsigned_repr (Int.unsigned y)) by omega. - rewrite unsigned_repr, Int.unsigned_repr by omega. + rewrite (unsigned_repr (Int.unsigned y)) by lia. + rewrite unsigned_repr, Int.unsigned_repr by lia. auto. } unfold shrx', shr', shru', shl'. rewrite <- A. change (Int.unsigned (Int.repr 63)) with (unsigned (repr 63)). rewrite <- B. apply shrx_shr_2. - unfold ltu. apply zlt_true. change (unsigned z < 63). rewrite A; omega. + unfold ltu. apply zlt_true. change (unsigned z < 63). rewrite A; lia. Qed. Remark int_ltu_2_inv: @@ -3606,11 +3606,11 @@ Proof. change (Int.unsigned iwordsize') with 64 in *. assert (128 < max_unsigned) by reflexivity. assert (128 < Int.max_unsigned) by reflexivity. - assert (Y: unsigned y' = Int.unsigned y) by (apply unsigned_repr; omega). - assert (Z: unsigned z' = Int.unsigned z) by (apply unsigned_repr; omega). + assert (Y: unsigned y' = Int.unsigned y) by (apply unsigned_repr; lia). + assert (Z: unsigned z' = Int.unsigned z) by (apply unsigned_repr; lia). assert (P: Int.unsigned (Int.add y z) = unsigned (add y' z')). - { unfold Int.add. rewrite Int.unsigned_repr by omega. - unfold add. rewrite unsigned_repr by omega. congruence. } + { unfold Int.add. rewrite Int.unsigned_repr by lia. + unfold add. rewrite unsigned_repr by lia. congruence. } intuition auto. apply zlt_true. rewrite Y; auto. apply zlt_true. rewrite Z; auto. @@ -3624,7 +3624,7 @@ Theorem or_ror': Int.add y z = iwordsize' -> ror x (repr (Int.unsigned z)) = or (shl' x y) (shru' x z). Proof. - intros. destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. rewrite H1; omega. + intros. destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. rewrite H1; lia. replace (shl' x y) with (shl x (repr (Int.unsigned y))). replace (shru' x z) with (shru x (repr (Int.unsigned z))). apply or_ror; auto. rewrite F, H1. reflexivity. @@ -3640,7 +3640,7 @@ Theorem shl'_shl': shl' (shl' x y) z = shl' x (Int.add y z). Proof. intros. apply Int.ltu_inv in H1. - destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. omega. + destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. lia. set (y' := repr (Int.unsigned y)) in *. set (z' := repr (Int.unsigned z)) in *. replace (shl' x y) with (shl x y'). @@ -3661,7 +3661,7 @@ Theorem shru'_shru': shru' (shru' x y) z = shru' x (Int.add y z). Proof. intros. apply Int.ltu_inv in H1. - destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. omega. + destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. lia. set (y' := repr (Int.unsigned y)) in *. set (z' := repr (Int.unsigned z)) in *. replace (shru' x y) with (shru x y'). @@ -3682,7 +3682,7 @@ Theorem shr'_shr': shr' (shr' x y) z = shr' x (Int.add y z). Proof. intros. apply Int.ltu_inv in H1. - destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. omega. + destruct (int_ltu_2_inv y z) as (A & B & C & D & E & F); auto. lia. set (y' := repr (Int.unsigned y)) in *. set (z' := repr (Int.unsigned z)) in *. replace (shr' x y) with (shr x y'). @@ -3707,21 +3707,21 @@ Proof. apply same_bits_eq; intros. rewrite bits_shru' by auto. fold Z. destruct (zlt Z Y). - assert (A: Int.unsigned (Int.sub y z) = Y - Z). - { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. } - symmetry; rewrite bits_shl', A by omega. + { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. lia. } + symmetry; rewrite bits_shl', A by lia. destruct (zlt (i + Z) zwordsize). -+ rewrite bits_shl' by omega. fold Y. - destruct (zlt i (Y - Z)); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. - rewrite bits_zero_ext by omega. rewrite zlt_true by omega. f_equal; omega. -+ rewrite bits_zero_ext by omega. rewrite ! zlt_false by omega. auto. ++ rewrite bits_shl' by lia. fold Y. + destruct (zlt i (Y - Z)); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. + rewrite bits_zero_ext by lia. rewrite zlt_true by lia. f_equal; lia. ++ rewrite bits_zero_ext by lia. rewrite ! zlt_false by lia. auto. - assert (A: Int.unsigned (Int.sub z y) = Z - Y). - { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. } - rewrite bits_zero_ext, bits_shru', A by omega. - destruct (zlt (i + Z) zwordsize); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. - rewrite bits_shl' by omega. fold Y. + { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. lia. } + rewrite bits_zero_ext, bits_shru', A by lia. + destruct (zlt (i + Z) zwordsize); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. + rewrite bits_shl' by lia. fold Y. destruct (zlt (i + Z) Y). -+ rewrite zlt_false by omega. auto. -+ rewrite zlt_true by omega. f_equal; omega. ++ rewrite zlt_false by lia. auto. ++ rewrite zlt_true by lia. f_equal; lia. Qed. Theorem shr'_shl': @@ -3734,26 +3734,26 @@ Proof. change (Int.unsigned iwordsize') with zwordsize in *. unfold Int.ltu. set (Y := Int.unsigned y) in *; set (Z := Int.unsigned z) in *. apply same_bits_eq; intros. rewrite bits_shr' by auto. fold Z. - rewrite bits_shl' by (destruct (zlt (i + Z) zwordsize); omega). fold Y. + rewrite bits_shl' by (destruct (zlt (i + Z) zwordsize); lia). fold Y. destruct (zlt Z Y). - assert (A: Int.unsigned (Int.sub y z) = Y - Z). - { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. } - rewrite bits_shl', A by omega. + { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. lia. } + rewrite bits_shl', A by lia. destruct (zlt i (Y - Z)). -+ apply zlt_true. destruct (zlt (i + Z) zwordsize); omega. -+ rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega). - rewrite bits_sign_ext by omega. f_equal. ++ apply zlt_true. destruct (zlt (i + Z) zwordsize); lia. ++ rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); lia). + rewrite bits_sign_ext by lia. f_equal. destruct (zlt (i + Z) zwordsize). - rewrite zlt_true by omega. omega. - rewrite zlt_false by omega. omega. + rewrite zlt_true by lia. lia. + rewrite zlt_false by lia. lia. - assert (A: Int.unsigned (Int.sub z y) = Z - Y). - { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. } - rewrite bits_sign_ext by omega. - rewrite bits_shr' by (destruct (zlt i (zwordsize - Z)); omega). - rewrite A. rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega). + { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. lia. } + rewrite bits_sign_ext by lia. + rewrite bits_shr' by (destruct (zlt i (zwordsize - Z)); lia). + rewrite A. rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); lia). f_equal. destruct (zlt i (zwordsize - Z)). -+ rewrite ! zlt_true by omega. omega. -+ rewrite ! zlt_false by omega. rewrite zlt_true by omega. omega. ++ rewrite ! zlt_true by lia. lia. ++ rewrite ! zlt_false by lia. rewrite zlt_true by lia. lia. Qed. Lemma shl'_zero_ext: @@ -3761,11 +3761,11 @@ Lemma shl'_zero_ext: shl' (zero_ext n x) m = zero_ext (n + Int.unsigned m) (shl' x m). Proof. intros. apply same_bits_eq; intros. - rewrite bits_zero_ext, ! bits_shl' by omega. + rewrite bits_zero_ext, ! bits_shl' by lia. destruct (zlt i (Int.unsigned m)). -- rewrite zlt_true by omega; auto. -- rewrite bits_zero_ext by omega. - destruct (zlt (i - Int.unsigned m) n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. +- rewrite zlt_true by lia; auto. +- rewrite bits_zero_ext by lia. + destruct (zlt (i - Int.unsigned m) n); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. Qed. Lemma shl'_sign_ext: @@ -3774,12 +3774,12 @@ Lemma shl'_sign_ext: Proof. intros. generalize (Int.unsigned_range m); intros. apply same_bits_eq; intros. - rewrite bits_sign_ext, ! bits_shl' by omega. + rewrite bits_sign_ext, ! bits_shl' by lia. destruct (zlt i (n + Int.unsigned m)). - rewrite bits_shl' by auto. destruct (zlt i (Int.unsigned m)); auto. - rewrite bits_sign_ext by omega. f_equal. apply zlt_true. omega. -- rewrite zlt_false by omega. rewrite bits_shl' by omega. rewrite zlt_false by omega. - rewrite bits_sign_ext by omega. f_equal. rewrite zlt_false by omega. omega. + rewrite bits_sign_ext by lia. f_equal. apply zlt_true. lia. +- rewrite zlt_false by lia. rewrite bits_shl' by lia. rewrite zlt_false by lia. + rewrite bits_sign_ext by lia. f_equal. rewrite zlt_false by lia. lia. Qed. Lemma shru'_zero_ext: @@ -3787,9 +3787,9 @@ Lemma shru'_zero_ext: shru' (zero_ext (n + Int.unsigned m) x) m = zero_ext n (shru' x m). Proof. intros. generalize (Int.unsigned_range m); intros. - bit_solve; [|omega]. rewrite bits_shru', bits_zero_ext, bits_shru' by omega. + bit_solve; [|lia]. rewrite bits_shru', bits_zero_ext, bits_shru' by lia. destruct (zlt (i + Int.unsigned m) zwordsize). -* destruct (zlt i n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto. +* destruct (zlt i n); [rewrite zlt_true by lia|rewrite zlt_false by lia]; auto. * destruct (zlt i n); auto. Qed. @@ -3798,9 +3798,9 @@ Lemma shru'_zero_ext_0: shru' (zero_ext n x) m = zero. Proof. intros. generalize (Int.unsigned_range m); intros. - bit_solve. rewrite bits_shru', bits_zero_ext by omega. + bit_solve. rewrite bits_shru', bits_zero_ext by lia. destruct (zlt (i + Int.unsigned m) zwordsize); auto. - apply zlt_false. omega. + apply zlt_false. lia. Qed. Lemma shr'_sign_ext: @@ -3813,12 +3813,12 @@ Proof. rewrite bits_sign_ext, bits_shr'. - f_equal. destruct (zlt i n), (zlt (i + Int.unsigned m) zwordsize). -+ apply zlt_true; omega. -+ apply zlt_true; omega. -+ rewrite zlt_false by omega. rewrite zlt_true by omega. omega. -+ rewrite zlt_false by omega. rewrite zlt_true by omega. omega. -- destruct (zlt i n); omega. -- destruct (zlt (i + Int.unsigned m) zwordsize); omega. ++ apply zlt_true; lia. ++ apply zlt_true; lia. ++ rewrite zlt_false by lia. rewrite zlt_true by lia. lia. ++ rewrite zlt_false by lia. rewrite zlt_true by lia. lia. +- destruct (zlt i n); lia. +- destruct (zlt (i + Int.unsigned m) zwordsize); lia. Qed. Lemma zero_ext_shru'_min: @@ -3827,10 +3827,10 @@ Lemma zero_ext_shru'_min: Proof. intros. apply Int.ltu_inv in H. change (Int.unsigned iwordsize') with zwordsize in H. apply Z.min_case_strong; intros; auto. - bit_solve; try omega. rewrite ! bits_shru' by omega. + bit_solve; try lia. rewrite ! bits_shru' by lia. destruct (zlt i (zwordsize - Int.unsigned n)). - rewrite zlt_true by omega. auto. - destruct (zlt i s); auto. rewrite zlt_false by omega; auto. + rewrite zlt_true by lia. auto. + destruct (zlt i s); auto. rewrite zlt_false by lia; auto. Qed. Lemma sign_ext_shr'_min: @@ -3842,12 +3842,12 @@ Proof. destruct (Z.min_spec (zwordsize - Int.unsigned n) s) as [[A B] | [A B]]; rewrite B; auto. apply same_bits_eq; intros. rewrite ! bits_sign_ext by auto. destruct (zlt i (zwordsize - Int.unsigned n)). - rewrite zlt_true by omega. auto. + rewrite zlt_true by lia. auto. assert (C: testbit (shr' x n) (zwordsize - Int.unsigned n - 1) = testbit x (zwordsize - 1)). - { rewrite bits_shr' by omega. rewrite zlt_true by omega. f_equal; omega. } - rewrite C. destruct (zlt i s); rewrite bits_shr' by omega. - rewrite zlt_false by omega. auto. - rewrite zlt_false by omega. auto. + { rewrite bits_shr' by lia. rewrite zlt_true by lia. f_equal; lia. } + rewrite C. destruct (zlt i s); rewrite bits_shr' by lia. + rewrite zlt_false by lia. auto. + rewrite zlt_false by lia. auto. Qed. Lemma shl'_zero_ext_min: @@ -3858,10 +3858,10 @@ Proof. apply Z.min_case_strong; intros; auto. apply same_bits_eq; intros. rewrite ! bits_shl' by auto. destruct (zlt i (Int.unsigned n)); auto. - rewrite ! bits_zero_ext by omega. + rewrite ! bits_zero_ext by lia. destruct (zlt (i - Int.unsigned n) s). - rewrite zlt_true by omega; auto. - rewrite zlt_false by omega; auto. + rewrite zlt_true by lia; auto. + rewrite zlt_false by lia; auto. Qed. Lemma shl'_sign_ext_min: @@ -3873,10 +3873,10 @@ Proof. destruct (Z.min_spec (zwordsize - Int.unsigned n) s) as [[A B] | [A B]]; rewrite B; auto. apply same_bits_eq; intros. rewrite ! bits_shl' by auto. destruct (zlt i (Int.unsigned n)); auto. - rewrite ! bits_sign_ext by omega. f_equal. + rewrite ! bits_sign_ext by lia. f_equal. destruct (zlt (i - Int.unsigned n) s). - rewrite zlt_true by omega; auto. - omegaContradiction. + rewrite zlt_true by lia; auto. + extlia. Qed. (** Powers of two with exponents given as 32-bit ints *) @@ -3897,8 +3897,8 @@ Proof. destruct (list_in_map_inv _ _ _ H) as [i0 [EQ IN]]. exploit Z_one_bits_range; eauto. fold zwordsize. intros R. unfold Int.ltu. rewrite EQ. rewrite Int.unsigned_repr. - change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. omega. - assert (zwordsize < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned iwordsize') with zwordsize. apply zlt_true. lia. + assert (zwordsize < Int.max_unsigned) by reflexivity. lia. Qed. Fixpoint int_of_one_bits' (l: list Int.int) : int := @@ -3917,7 +3917,7 @@ Proof. - auto. - rewrite IHl by eauto. apply eqm_samerepr; apply eqm_add. + rewrite shl'_one_two_p. rewrite Int.unsigned_repr. apply eqm_sym; apply eqm_unsigned_repr. - exploit (H a). auto. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. + exploit (H a). auto. assert (zwordsize < Int.max_unsigned) by reflexivity. lia. + apply eqm_sym; apply eqm_unsigned_repr. } intros. rewrite <- (repr_unsigned x) at 1. unfold one_bits'. rewrite REC. @@ -3936,7 +3936,7 @@ Proof. { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. } rewrite Int.unsigned_repr. auto. assert (zwordsize < Int.max_unsigned) by reflexivity. - omega. + lia. Qed. Theorem is_power2'_range: @@ -3955,11 +3955,11 @@ Proof. unfold is_power2'; intros. destruct (Z_one_bits wordsize (unsigned n) 0) as [ | i [ | ? ?]] eqn:B; inv H. rewrite (Z_one_bits_powerserie wordsize (unsigned n)) by (apply unsigned_range). - rewrite Int.unsigned_repr. rewrite B; simpl. omega. + rewrite Int.unsigned_repr. rewrite B; simpl. lia. assert (0 <= i < zwordsize). { apply Z_one_bits_range with (unsigned n). rewrite B; auto with coqlib. } assert (zwordsize < Int.max_unsigned) by reflexivity. - omega. + lia. Qed. Theorem mul_pow2': @@ -4003,7 +4003,7 @@ Proof. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. fold (testbit (shru n (repr Int.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Int.zwordsize)) with Int.zwordsize. - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_ofwords: @@ -4018,15 +4018,15 @@ Proof. rewrite testbit_repr; auto. rewrite !testbit_repr; auto. fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto. - omega. + lia. Qed. Lemma lo_ofwords: forall hi lo, loword (ofwords hi lo) = lo. Proof. intros. apply Int.same_bits_eq; intros. - rewrite bits_loword; auto. rewrite bits_ofwords. apply zlt_true. omega. - assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. + rewrite bits_loword; auto. rewrite bits_ofwords. apply zlt_true. lia. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. lia. Qed. Lemma hi_ofwords: @@ -4034,8 +4034,8 @@ Lemma hi_ofwords: Proof. intros. apply Int.same_bits_eq; intros. rewrite bits_hiword; auto. rewrite bits_ofwords. - rewrite zlt_false. f_equal. omega. omega. - assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. + rewrite zlt_false. f_equal. lia. lia. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. lia. Qed. Lemma ofwords_recompose: @@ -4043,9 +4043,9 @@ Lemma ofwords_recompose: Proof. intros. apply same_bits_eq; intros. rewrite bits_ofwords; auto. destruct (zlt i Int.zwordsize). - apply bits_loword. omega. - rewrite bits_hiword. f_equal. omega. - assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. + apply bits_loword. lia. + rewrite bits_hiword. f_equal. lia. + assert (zwordsize = 2 * Int.zwordsize) by reflexivity. lia. Qed. Lemma ofwords_add: @@ -4056,10 +4056,10 @@ Proof. apply eqm_sym; apply eqm_unsigned_repr. apply eqm_refl. apply eqm_sym; apply eqm_unsigned_repr. - change Int.zwordsize with 32; change zwordsize with 64; omega. + change Int.zwordsize with 32; change zwordsize with 64; lia. rewrite unsigned_repr. generalize (Int.unsigned_range lo). intros [A B]. exact B. assert (Int.max_unsigned < max_unsigned) by (compute; auto). - generalize (Int.unsigned_range_2 lo); omega. + generalize (Int.unsigned_range_2 lo); lia. Qed. Lemma ofwords_add': @@ -4070,7 +4070,7 @@ Proof. change (two_p 32) with Int.modulus. change Int.modulus with 4294967296. change max_unsigned with 18446744073709551615. - omega. + lia. Qed. Remark eqm_mul_2p32: @@ -4094,7 +4094,7 @@ Proof. change min_signed with (Int.min_signed * Int.modulus). change max_signed with (Int.max_signed * Int.modulus + Int.modulus - 1). change Int.modulus with 4294967296. - omega. + lia. apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. apply Int.eqm_signed_unsigned. apply eqm_refl. Qed. @@ -4109,7 +4109,7 @@ Proof. intros. apply Int64.same_bits_eq; intros. rewrite H by auto. rewrite ! bits_ofwords by auto. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. - destruct (zlt i Int.zwordsize); rewrite H0 by omega; auto. + destruct (zlt i Int.zwordsize); rewrite H0 by lia; auto. Qed. Lemma decompose_and: @@ -4154,21 +4154,21 @@ Proof. intros. assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). { unfold Int.sub. rewrite Int.unsigned_repr. auto. - rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } + rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; lia. } assert (zwordsize = 2 * Int.zwordsize) by reflexivity. apply Int64.same_bits_eq; intros. rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto. - destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by omega. + destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by lia. destruct (zlt i (Int.unsigned y)). auto. - rewrite bits_ofwords by omega. rewrite zlt_true by omega. auto. - rewrite zlt_false by omega. rewrite bits_ofwords by omega. - rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. - rewrite Int.bits_shru by omega. rewrite H0. + rewrite bits_ofwords by lia. rewrite zlt_true by lia. auto. + rewrite zlt_false by lia. rewrite bits_ofwords by lia. + rewrite Int.bits_or by lia. rewrite Int.bits_shl by lia. + rewrite Int.bits_shru by lia. rewrite H0. destruct (zlt (i - Int.unsigned y) (Int.zwordsize)). - rewrite zlt_true by omega. rewrite zlt_true by omega. - rewrite orb_false_l. f_equal. omega. - rewrite zlt_false by omega. rewrite zlt_false by omega. - rewrite orb_false_r. f_equal. omega. + rewrite zlt_true by lia. rewrite zlt_true by lia. + rewrite orb_false_l. f_equal. lia. + rewrite zlt_false by lia. rewrite zlt_false by lia. + rewrite orb_false_r. f_equal. lia. Qed. Lemma decompose_shl_2: @@ -4181,15 +4181,15 @@ Proof. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize). { unfold Int.sub. rewrite Int.unsigned_repr. auto. - rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } + rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). lia. } apply Int64.same_bits_eq; intros. rewrite bits_shl' by auto. symmetry. rewrite bits_ofwords by auto. - destruct (zlt i Int.zwordsize). rewrite zlt_true by omega. apply Int.bits_zero. - rewrite Int.bits_shl by omega. + destruct (zlt i Int.zwordsize). rewrite zlt_true by lia. apply Int.bits_zero. + rewrite Int.bits_shl by lia. destruct (zlt i (Int.unsigned y)). - rewrite zlt_true by omega. auto. - rewrite zlt_false by omega. - rewrite bits_ofwords by omega. rewrite zlt_true by omega. f_equal. omega. + rewrite zlt_true by lia. auto. + rewrite zlt_false by lia. + rewrite bits_ofwords by lia. rewrite zlt_true by lia. f_equal. lia. Qed. Lemma decompose_shru_1: @@ -4202,25 +4202,25 @@ Proof. intros. assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). { unfold Int.sub. rewrite Int.unsigned_repr. auto. - rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } + rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; lia. } assert (zwordsize = 2 * Int.zwordsize) by reflexivity. apply Int64.same_bits_eq; intros. rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto. destruct (zlt i Int.zwordsize). - rewrite zlt_true by omega. - rewrite bits_ofwords by omega. - rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. - rewrite Int.bits_shru by omega. rewrite H0. + rewrite zlt_true by lia. + rewrite bits_ofwords by lia. + rewrite Int.bits_or by lia. rewrite Int.bits_shl by lia. + rewrite Int.bits_shru by lia. rewrite H0. destruct (zlt (i + Int.unsigned y) (Int.zwordsize)). - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite orb_false_r. auto. - rewrite zlt_false by omega. - rewrite orb_false_l. f_equal. omega. - rewrite Int.bits_shru by omega. + rewrite zlt_false by lia. + rewrite orb_false_l. f_equal. lia. + rewrite Int.bits_shru by lia. destruct (zlt (i + Int.unsigned y) zwordsize). - rewrite bits_ofwords by omega. - rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. - rewrite zlt_false by omega. auto. + rewrite bits_ofwords by lia. + rewrite zlt_true by lia. rewrite zlt_false by lia. f_equal. lia. + rewrite zlt_false by lia. auto. Qed. Lemma decompose_shru_2: @@ -4233,16 +4233,16 @@ Proof. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize). { unfold Int.sub. rewrite Int.unsigned_repr. auto. - rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } + rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). lia. } apply Int64.same_bits_eq; intros. rewrite bits_shru' by auto. symmetry. rewrite bits_ofwords by auto. destruct (zlt i Int.zwordsize). - rewrite Int.bits_shru by omega. rewrite H1. + rewrite Int.bits_shru by lia. rewrite H1. destruct (zlt (i + Int.unsigned y) zwordsize). - rewrite zlt_true by omega. rewrite bits_ofwords by omega. - rewrite zlt_false by omega. f_equal; omega. - rewrite zlt_false by omega. auto. - rewrite zlt_false by omega. apply Int.bits_zero. + rewrite zlt_true by lia. rewrite bits_ofwords by lia. + rewrite zlt_false by lia. f_equal; lia. + rewrite zlt_false by lia. auto. + rewrite zlt_false by lia. apply Int.bits_zero. Qed. Lemma decompose_shr_1: @@ -4255,26 +4255,26 @@ Proof. intros. assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). { unfold Int.sub. rewrite Int.unsigned_repr. auto. - rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } + rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; lia. } assert (zwordsize = 2 * Int.zwordsize) by reflexivity. apply Int64.same_bits_eq; intros. rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto. destruct (zlt i Int.zwordsize). - rewrite zlt_true by omega. - rewrite bits_ofwords by omega. - rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. - rewrite Int.bits_shru by omega. rewrite H0. + rewrite zlt_true by lia. + rewrite bits_ofwords by lia. + rewrite Int.bits_or by lia. rewrite Int.bits_shl by lia. + rewrite Int.bits_shru by lia. rewrite H0. destruct (zlt (i + Int.unsigned y) (Int.zwordsize)). - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite orb_false_r. auto. - rewrite zlt_false by omega. - rewrite orb_false_l. f_equal. omega. - rewrite Int.bits_shr by omega. + rewrite zlt_false by lia. + rewrite orb_false_l. f_equal. lia. + rewrite Int.bits_shr by lia. destruct (zlt (i + Int.unsigned y) zwordsize). - rewrite bits_ofwords by omega. - rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. - rewrite zlt_false by omega. rewrite bits_ofwords by omega. - rewrite zlt_false by omega. f_equal. + rewrite bits_ofwords by lia. + rewrite zlt_true by lia. rewrite zlt_false by lia. f_equal. lia. + rewrite zlt_false by lia. rewrite bits_ofwords by lia. + rewrite zlt_false by lia. f_equal. Qed. Lemma decompose_shr_2: @@ -4288,24 +4288,24 @@ Proof. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. assert (Int.unsigned (Int.sub y Int.iwordsize) = Int.unsigned y - Int.zwordsize). { unfold Int.sub. rewrite Int.unsigned_repr. auto. - rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } + rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). lia. } apply Int64.same_bits_eq; intros. rewrite bits_shr' by auto. symmetry. rewrite bits_ofwords by auto. destruct (zlt i Int.zwordsize). - rewrite Int.bits_shr by omega. rewrite H1. + rewrite Int.bits_shr by lia. rewrite H1. destruct (zlt (i + Int.unsigned y) zwordsize). - rewrite zlt_true by omega. rewrite bits_ofwords by omega. - rewrite zlt_false by omega. f_equal; omega. - rewrite zlt_false by omega. rewrite bits_ofwords by omega. - rewrite zlt_false by omega. auto. - rewrite Int.bits_shr by omega. + rewrite zlt_true by lia. rewrite bits_ofwords by lia. + rewrite zlt_false by lia. f_equal; lia. + rewrite zlt_false by lia. rewrite bits_ofwords by lia. + rewrite zlt_false by lia. auto. + rewrite Int.bits_shr by lia. change (Int.unsigned (Int.sub Int.iwordsize Int.one)) with (Int.zwordsize - 1). destruct (zlt (i + Int.unsigned y) zwordsize); - rewrite bits_ofwords by omega. - symmetry. rewrite zlt_false by omega. f_equal. - destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. - symmetry. rewrite zlt_false by omega. f_equal. - destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. + rewrite bits_ofwords by lia. + symmetry. rewrite zlt_false by lia. f_equal. + destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); lia. + symmetry. rewrite zlt_false by lia. f_equal. + destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); lia. Qed. Lemma decompose_add: @@ -4442,14 +4442,14 @@ Proof. intros. unfold ltu. rewrite ! ofwords_add'. unfold Int.ltu, Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). rewrite e. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). - apply zlt_true; omega. - apply zlt_false; omega. + apply zlt_true; lia. + apply zlt_false; lia. change (two_p 32) with Int.modulus. generalize (Int.unsigned_range xl) (Int.unsigned_range yl). change Int.modulus with 4294967296. intros. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). - apply zlt_true; omega. - apply zlt_false; omega. + apply zlt_true; lia. + apply zlt_false; lia. Qed. Lemma decompose_leu: @@ -4461,8 +4461,8 @@ Proof. unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). auto. unfold Int.ltu. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). - rewrite zlt_false by omega; auto. - rewrite zlt_true by omega; auto. + rewrite zlt_false by lia; auto. + rewrite zlt_true by lia; auto. Qed. Lemma decompose_lt: @@ -4472,14 +4472,14 @@ Proof. intros. unfold lt. rewrite ! ofwords_add''. rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)). rewrite e. unfold Int.ltu. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). - apply zlt_true; omega. - apply zlt_false; omega. + apply zlt_true; lia. + apply zlt_false; lia. change (two_p 32) with Int.modulus. generalize (Int.unsigned_range xl) (Int.unsigned_range yl). change Int.modulus with 4294967296. intros. unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). - apply zlt_true; omega. - apply zlt_false; omega. + apply zlt_true; lia. + apply zlt_false; lia. Qed. Lemma decompose_le: @@ -4491,8 +4491,8 @@ Proof. rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)). auto. unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). - rewrite zlt_false by omega; auto. - rewrite zlt_true by omega; auto. + rewrite zlt_false by lia; auto. + rewrite zlt_true by lia; auto. Qed. (** Utility proofs for mixed 32bit and 64bit arithmetic *) @@ -4507,7 +4507,7 @@ Proof. change (wordsize) with 64%nat in *. change (Int.wordsize) with 32%nat in *. unfold two_power_nat. simpl. - omega. + lia. Qed. Remark int_unsigned_repr: @@ -4527,9 +4527,9 @@ Proof. rewrite unsigned_repr by apply int_unsigned_range. rewrite int_unsigned_repr. reflexivity. rewrite unsigned_repr by apply int_unsigned_range. rewrite int_unsigned_repr. generalize (int_unsigned_range y). - omega. + lia. generalize (Int.sub_ltu x y H). intros. - generalize (Int.unsigned_range_2 y). intros. omega. + generalize (Int.unsigned_range_2 y). intros. lia. Qed. End Int64. @@ -4687,7 +4687,7 @@ Lemma to_int_of_int: forall n, to_int (of_int n) = n. Proof. intros; unfold of_int, to_int. rewrite unsigned_repr. apply Int.repr_unsigned. - unfold max_unsigned. rewrite modulus_eq32. destruct (Int.unsigned_range n); omega. + unfold max_unsigned. rewrite modulus_eq32. destruct (Int.unsigned_range n); lia. Qed. End AGREE32. @@ -4797,7 +4797,7 @@ Lemma to_int64_of_int64: forall n, to_int64 (of_int64 n) = n. Proof. intros; unfold of_int64, to_int64. rewrite unsigned_repr. apply Int64.repr_unsigned. - unfold max_unsigned. rewrite modulus_eq64. destruct (Int64.unsigned_range n); omega. + unfold max_unsigned. rewrite modulus_eq64. destruct (Int64.unsigned_range n); lia. Qed. End AGREE64. diff --git a/lib/Intv.v b/lib/Intv.v index a11e619b..19943942 100644 --- a/lib/Intv.v +++ b/lib/Intv.v @@ -41,14 +41,14 @@ Lemma notin_range: forall x i, x < fst i \/ x >= snd i -> ~In x i. Proof. - unfold In; intros; omega. + unfold In; intros; lia. Qed. Lemma range_notin: forall x i, ~In x i -> fst i < snd i -> x < fst i \/ x >= snd i. Proof. - unfold In; intros; omega. + unfold In; intros; lia. Qed. (** * Emptyness *) @@ -60,26 +60,26 @@ Lemma empty_dec: Proof. unfold empty; intros. case (zle (snd i) (fst i)); intros. - left; omega. - right; omega. + left; lia. + right; lia. Qed. Lemma is_notempty: forall i, fst i < snd i -> ~empty i. Proof. - unfold empty; intros; omega. + unfold empty; intros; lia. Qed. Lemma empty_notin: forall x i, empty i -> ~In x i. Proof. - unfold empty, In; intros. omega. + unfold empty, In; intros. lia. Qed. Lemma in_notempty: forall x i, In x i -> ~empty i. Proof. - unfold empty, In; intros. omega. + unfold empty, In; intros. lia. Qed. (** * Disjointness *) @@ -109,7 +109,7 @@ Lemma disjoint_range: forall i j, snd i <= fst j \/ snd j <= fst i -> disjoint i j. Proof. - unfold disjoint, In; intros. omega. + unfold disjoint, In; intros. lia. Qed. Lemma range_disjoint: @@ -127,13 +127,13 @@ Proof. (* Case 1.1: i ends to the left of j, OK *) auto. (* Case 1.2: i ends to the right of j's start, not disjoint. *) - elim (H (fst j)). red; omega. red; omega. + elim (H (fst j)). red; lia. red; lia. (* Case 2: j starts to the left of i *) destruct (zle (snd j) (fst i)). (* Case 2.1: j ends to the left of i, OK *) auto. (* Case 2.2: j ends to the right of i's start, not disjoint. *) - elim (H (fst i)). red; omega. red; omega. + elim (H (fst i)). red; lia. red; lia. Qed. Lemma range_disjoint': @@ -141,7 +141,7 @@ Lemma range_disjoint': disjoint i j -> fst i < snd i -> fst j < snd j -> snd i <= fst j \/ snd j <= fst i. Proof. - intros. exploit range_disjoint; eauto. unfold empty; intuition omega. + intros. exploit range_disjoint; eauto. unfold empty; intuition lia. Qed. Lemma disjoint_dec: @@ -163,14 +163,14 @@ Lemma in_shift: forall x i delta, In x i -> In (x + delta) (shift i delta). Proof. - unfold shift, In; intros. simpl. omega. + unfold shift, In; intros. simpl. lia. Qed. Lemma in_shift_inv: forall x i delta, In x (shift i delta) -> In (x - delta) i. Proof. - unfold shift, In; simpl; intros. omega. + unfold shift, In; simpl; intros. lia. Qed. (** * Enumerating the elements of an interval *) @@ -182,7 +182,7 @@ Variable lo: Z. Function elements_rec (hi: Z) {wf (Zwf lo) hi} : list Z := if zlt lo hi then (hi-1) :: elements_rec (hi-1) else nil. Proof. - intros. red. omega. + intros. red. lia. apply Zwf_well_founded. Qed. @@ -192,8 +192,8 @@ Lemma In_elements_rec: Proof. intros. functional induction (elements_rec hi). simpl; split; intros. - destruct H. clear IHl. omega. rewrite IHl in H. clear IHl. omega. - destruct (zeq (hi - 1) x); auto. right. rewrite IHl. clear IHl. omega. + destruct H. clear IHl. lia. rewrite IHl in H. clear IHl. lia. + destruct (zeq (hi - 1) x); auto. right. rewrite IHl. clear IHl. lia. simpl; intuition. Qed. @@ -241,20 +241,20 @@ Program Fixpoint forall_rec (hi: Z) {wf (Zwf lo) hi}: left _ _ . Next Obligation. - red. omega. + red. lia. Qed. Next Obligation. - assert (x = hi - 1 \/ x < hi - 1) by omega. + assert (x = hi - 1 \/ x < hi - 1) by lia. destruct H2. congruence. auto. Qed. Next Obligation. - exists wildcard'; split; auto. omega. + exists wildcard'; split; auto. lia. Qed. Next Obligation. - exists (hi - 1); split; auto. omega. + exists (hi - 1); split; auto. lia. Qed. Next Obligation. - omegaContradiction. + extlia. Defined. End FORALL. @@ -276,7 +276,7 @@ Variable a: A. Function fold_rec (hi: Z) {wf (Zwf lo) hi} : A := if zlt lo hi then f (hi - 1) (fold_rec (hi - 1)) else a. Proof. - intros. red. omega. + intros. red. lia. apply Zwf_well_founded. Qed. diff --git a/lib/IntvSets.v b/lib/IntvSets.v index b97d9882..7250a9f6 100644 --- a/lib/IntvSets.v +++ b/lib/IntvSets.v @@ -59,7 +59,7 @@ Proof. + destruct (zle l x); simpl. * tauto. * split; intros. congruence. - exfalso. destruct H0. omega. exploit BELOW; eauto. omega. + exfalso. destruct H0. lia. exploit BELOW; eauto. lia. + rewrite IHok. intuition. Qed. @@ -74,14 +74,14 @@ Lemma contains_In: (contains l0 h0 s = true <-> (forall x, l0 <= x < h0 -> In x s)). Proof. induction 2; simpl. -- intuition. elim (H0 l0); omega. +- intuition. elim (H0 l0); lia. - destruct (zle h0 h); simpl. destruct (zle l l0); simpl. intuition. rewrite IHok. intuition. destruct (H3 x); auto. exfalso. - destruct (H3 l0). omega. omega. exploit BELOW; eauto. omega. + destruct (H3 l0). lia. lia. exploit BELOW; eauto. lia. rewrite IHok. intuition. destruct (H3 x); auto. exfalso. - destruct (H3 h). omega. omega. exploit BELOW; eauto. omega. + destruct (H3 h). lia. lia. exploit BELOW; eauto. lia. Qed. Fixpoint add (L H: Z) (s: t) {struct s} : t := @@ -103,9 +103,9 @@ Proof. destruct (zlt h0 l). simpl. tauto. rewrite IHok. intuition idtac. - assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto. - left; xomega. - left; xomega. + assert (l0 <= x < h0 \/ l <= x < h) by extlia. tauto. + left; extlia. + left; extlia. Qed. Lemma add_ok: @@ -115,11 +115,11 @@ Proof. constructor. auto. intros. inv H0. constructor. destruct (zlt h l0). constructor; auto. intros. rewrite In_add in H1; auto. - destruct H1. omega. auto. + destruct H1. lia. auto. destruct (zlt h0 l). - constructor. auto. simpl; intros. destruct H1. omega. exploit BELOW; eauto. omega. - constructor. omega. auto. auto. - apply IHok. xomega. + constructor. auto. simpl; intros. destruct H1. lia. exploit BELOW; eauto. lia. + constructor. lia. auto. auto. + apply IHok. extlia. Qed. Fixpoint remove (L H: Z) (s: t) {struct s} : t := @@ -141,22 +141,22 @@ Proof. induction 1; simpl. tauto. destruct (zlt h l0). - simpl. rewrite IHok. intuition omega. + simpl. rewrite IHok. intuition lia. destruct (zlt h0 l). - simpl. intuition. exploit BELOW; eauto. omega. + simpl. intuition. exploit BELOW; eauto. lia. destruct (zlt l l0). destruct (zlt h0 h); simpl. clear IHok. split. intros [A | [A | A]]. - split. omega. left; omega. - split. omega. left; omega. - split. exploit BELOW; eauto. omega. auto. + split. lia. left; lia. + split. lia. left; lia. + split. exploit BELOW; eauto. lia. auto. intros [A [B | B]]. - destruct (zlt x l0). left; omega. right; left; omega. + destruct (zlt x l0). left; lia. right; left; lia. auto. - intuition omega. + intuition lia. destruct (zlt h0 h); simpl. - intuition. exploit BELOW; eauto. omega. - rewrite IHok. intuition. omegaContradiction. + intuition. exploit BELOW; eauto. lia. + rewrite IHok. intuition. extlia. Qed. Lemma remove_ok: @@ -170,9 +170,9 @@ Proof. constructor; auto. destruct (zlt l l0). destruct (zlt h0 h). - constructor. omega. intros. inv H1. omega. exploit BELOW; eauto. omega. - constructor. omega. auto. auto. - constructor; auto. intros. rewrite In_remove in H1 by auto. destruct H1. exploit BELOW; eauto. omega. + constructor. lia. intros. inv H1. lia. exploit BELOW; eauto. lia. + constructor. lia. auto. auto. + constructor; auto. intros. rewrite In_remove in H1 by auto. destruct H1. exploit BELOW; eauto. lia. destruct (zlt h0 h). constructor; auto. auto. @@ -204,19 +204,19 @@ Proof. tauto. assert (ok (Cons l0 h0 s0)) by (constructor; auto). destruct (zle h l0). - rewrite IHok; auto. simpl. intuition. omegaContradiction. - exploit BELOW0; eauto. intros. omegaContradiction. + rewrite IHok; auto. simpl. intuition. extlia. + exploit BELOW0; eauto. intros. extlia. destruct (zle h0 l). - simpl in IHok0; rewrite IHok0. intuition. omegaContradiction. - exploit BELOW; eauto. intros; omegaContradiction. + simpl in IHok0; rewrite IHok0. intuition. extlia. + exploit BELOW; eauto. intros; extlia. destruct (zle l l0). destruct (zle h0 h). simpl. simpl in IHok0; rewrite IHok0. intuition. - simpl. rewrite IHok; auto. simpl. intuition. exploit BELOW0; eauto. intros; omegaContradiction. + simpl. rewrite IHok; auto. simpl. intuition. exploit BELOW0; eauto. intros; extlia. destruct (zle h h0). simpl. rewrite IHok; auto. simpl. intuition. simpl. simpl in IHok0; rewrite IHok0. intuition. - exploit BELOW; eauto. intros; omegaContradiction. + exploit BELOW; eauto. intros; extlia. Qed. Lemma inter_ok: @@ -237,12 +237,12 @@ Proof. constructor; auto. intros. assert (In x (inter (Cons l h s) s0)) by exact H3. rewrite In_inter in H4; auto. apply BELOW0. tauto. - constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. + constructor. lia. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. auto. destruct (zle h h0). - constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. + constructor. lia. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. auto. - constructor. omega. intros. + constructor. lia. intros. assert (In x (inter (Cons l h s) s0)) by exact H3. rewrite In_inter in H4; auto. apply BELOW0. tauto. auto. @@ -281,20 +281,20 @@ Lemma beq_spec: Proof. induction 1; destruct 1; simpl. - tauto. -- split; intros. discriminate. exfalso. apply (H0 l). left; omega. -- split; intros. discriminate. exfalso. apply (H0 l). left; omega. +- split; intros. discriminate. exfalso. apply (H0 l). left; lia. +- split; intros. discriminate. exfalso. apply (H0 l). left; lia. - split; intros. + InvBooleans. subst. rewrite IHok in H3 by auto. rewrite H3. tauto. + destruct (zeq l l0). destruct (zeq h h0). simpl. subst. apply IHok. auto. intros; split; intros. - destruct (proj1 (H1 x)); auto. exfalso. exploit BELOW; eauto. omega. - destruct (proj2 (H1 x)); auto. exfalso. exploit BELOW0; eauto. omega. + destruct (proj1 (H1 x)); auto. exfalso. exploit BELOW; eauto. lia. + destruct (proj2 (H1 x)); auto. exfalso. exploit BELOW0; eauto. lia. exfalso. subst l0. destruct (zlt h h0). - destruct (proj2 (H1 h)). left; omega. omega. exploit BELOW; eauto. omega. - destruct (proj1 (H1 h0)). left; omega. omega. exploit BELOW0; eauto. omega. + destruct (proj2 (H1 h)). left; lia. lia. exploit BELOW; eauto. lia. + destruct (proj1 (H1 h0)). left; lia. lia. exploit BELOW0; eauto. lia. exfalso. destruct (zlt l l0). - destruct (proj1 (H1 l)). left; omega. omega. exploit BELOW0; eauto. omega. - destruct (proj2 (H1 l0)). left; omega. omega. exploit BELOW; eauto. omega. + destruct (proj1 (H1 l)). left; lia. lia. exploit BELOW0; eauto. lia. + destruct (proj2 (H1 l0)). left; lia. lia. exploit BELOW; eauto. lia. Qed. End R. @@ -340,7 +340,7 @@ Proof. unfold add, In; intros. destruct (zlt l h). simpl. apply R.In_add. apply proj2_sig. - intuition. omegaContradiction. + intuition. extlia. Qed. Program Definition remove (l h: Z) (s: t) : t := @@ -392,7 +392,7 @@ Theorem contains_spec: Proof. unfold contains, In; intros. destruct (zlt l h). apply R.contains_In. auto. apply proj2_sig. - split; intros. omegaContradiction. auto. + split; intros. extlia. auto. Qed. Program Definition beq (s1 s2: t) : bool := R.beq s1 s2. diff --git a/lib/Iteration.v b/lib/Iteration.v index 6a9d3253..0cca7fb7 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -237,8 +237,8 @@ Lemma iter_monot: Proof. induction p; intros. simpl. red; intros; red; auto. - destruct q. elimtype False; omega. - simpl. apply F_iter_monot. apply IHp. omega. + destruct q. elimtype False; lia. + simpl. apply F_iter_monot. apply IHp. lia. Qed. Lemma iter_either: diff --git a/lib/Maps.v b/lib/Maps.v index 9e44a7fe..54d92897 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1395,7 +1395,7 @@ Theorem cardinal_remove: Proof. unfold cardinal; intros. exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q). - rewrite P, Q. rewrite ! app_length. simpl. omega. + rewrite P, Q. rewrite ! app_length. simpl. lia. Qed. Theorem cardinal_set: diff --git a/lib/Ordered.v b/lib/Ordered.v index 1adbd330..69dc1c69 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -70,7 +70,7 @@ Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof Z.lt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. -Proof. unfold lt, eq, t; intros. omega. Qed. +Proof. unfold lt, eq, t; intros. lia. Qed. Lemma compare : forall x y : t, Compare lt eq x y. Proof. intros. destruct (Z.compare x y) as [] eqn:E. @@ -99,11 +99,11 @@ Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. - unfold lt; intros. omega. + unfold lt; intros. lia. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. - unfold lt,eq; intros; red; intros. subst. omega. + unfold lt,eq; intros; red; intros. subst. lia. Qed. Lemma compare : forall x y : t, Compare lt eq x y. Proof. @@ -114,7 +114,7 @@ Proof. apply GT. assert (Int.unsigned x <> Int.unsigned y). red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence. - red. omega. + red. lia. Defined. Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec. diff --git a/lib/Parmov.v b/lib/Parmov.v index db27e83f..f602bd60 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -1106,7 +1106,7 @@ Lemma measure_decreasing_1: forall st st', dtransition st st' -> measure st' < measure st. Proof. - induction 1; repeat (simpl; rewrite List.app_length); simpl; omega. + induction 1; repeat (simpl; rewrite List.app_length); simpl; lia. Qed. Lemma measure_decreasing_2: diff --git a/lib/Postorder.v b/lib/Postorder.v index 3181c4cc..eaeaea37 100644 --- a/lib/Postorder.v +++ b/lib/Postorder.v @@ -314,10 +314,10 @@ Proof. destruct (wrk s) as [ | [x succs] l]. discriminate. destruct succs as [ | y succs ]. - inv H. simpl. apply lex_ord_right. omega. + inv H. simpl. apply lex_ord_right. lia. destruct ((gr s)!y) as [succs'|] eqn:?. inv H. simpl. apply lex_ord_left. eapply PTree_Properties.cardinal_remove; eauto. - inv H. simpl. apply lex_ord_right. omega. + inv H. simpl. apply lex_ord_right. lia. Qed. End POSTORDER. diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 20bb91cd..c4a2f5b1 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -552,10 +552,10 @@ Proof. rewrite H; auto. simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true. inversion G. subst x'. rewrite dec_eq_false; auto. - replace (pathlen uf (repr uf a)) with 0. omega. + replace (pathlen uf (repr uf a)) with 0. lia. symmetry. apply pathlen_none. apply repr_res_none. rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G. - destruct (M.elt_eq (repr uf x') (repr uf a)); omega. + destruct (M.elt_eq (repr uf x') (repr uf a)); lia. simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate. rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. symmetry. apply pathlen_zero; auto. apply repr_none; auto. @@ -570,7 +570,7 @@ Proof. intros. repeat rewrite pathlen_merge. destruct (M.elt_eq (repr uf a) (repr uf b)). auto. rewrite H. destruct (M.elt_eq (repr uf y) (repr uf a)). - omega. auto. + lia. auto. Qed. (* Path compression *) diff --git a/lib/Zbits.v b/lib/Zbits.v index 6f3acaab..0539d04b 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -33,7 +33,7 @@ Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y. Lemma eqmod_refl: forall x, eqmod x x. Proof. - intros; red. exists 0. omega. + intros; red. exists 0. lia. Qed. Lemma eqmod_refl2: forall x y, x = y -> eqmod x y. @@ -57,7 +57,7 @@ Lemma eqmod_small_eq: Proof. intros x y [k EQ] I1 I2. generalize (Zdiv_unique _ _ _ _ EQ I2). intro. - rewrite (Z.div_small x modul I1) in H. subst k. omega. + rewrite (Z.div_small x modul I1) in H. subst k. lia. Qed. Lemma eqmod_mod_eq: @@ -136,11 +136,11 @@ Lemma P_mod_two_p_range: forall n p, 0 <= P_mod_two_p p n < two_power_nat n. Proof. induction n; simpl; intros. - - rewrite two_power_nat_O. omega. + - rewrite two_power_nat_O. lia. - rewrite two_power_nat_S. destruct p. - + generalize (IHn p). rewrite Z.succ_double_spec. omega. - + generalize (IHn p). rewrite Z.double_spec. omega. - + generalize (two_power_nat_pos n). omega. + + generalize (IHn p). rewrite Z.succ_double_spec. lia. + + generalize (IHn p). rewrite Z.double_spec. lia. + + generalize (two_power_nat_pos n). lia. Qed. Lemma P_mod_two_p_eq: @@ -157,7 +157,7 @@ Proof. + destruct (IHn p) as [y EQ]. exists y. change (Zpos p~0) with (2 * Zpos p). rewrite EQ. rewrite (Z.double_spec (P_mod_two_p p n)). ring. - + exists 0; omega. + + exists 0; lia. } intros. destruct (H n p) as [y EQ]. @@ -221,8 +221,8 @@ Remark Zshiftin_spec: forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0). Proof. unfold Zshiftin; intros. destruct b. - - rewrite Z.succ_double_spec. omega. - - rewrite Z.double_spec. omega. + - rewrite Z.succ_double_spec. lia. + - rewrite Z.double_spec. lia. Qed. Remark Zshiftin_inj: @@ -231,10 +231,10 @@ Remark Zshiftin_inj: Proof. intros. rewrite !Zshiftin_spec in H. destruct b1; destruct b2. - split; [auto|omega]. - omegaContradiction. - omegaContradiction. - split; [auto|omega]. + split; [auto|lia]. + extlia. + extlia. + split; [auto|lia]. Qed. Remark Zdecomp: @@ -255,9 +255,9 @@ Proof. - subst n. destruct b. + apply Z.testbit_odd_0. + rewrite Z.add_0_r. apply Z.testbit_even_0. - - assert (0 <= Z.pred n) by omega. + - assert (0 <= Z.pred n) by lia. set (n' := Z.pred n) in *. - replace n with (Z.succ n') by (unfold n'; omega). + replace n with (Z.succ n') by (unfold n'; lia). destruct b. + apply Z.testbit_odd_succ; auto. + rewrite Z.add_0_r. apply Z.testbit_even_succ; auto. @@ -273,7 +273,7 @@ Remark Ztestbit_shiftin_succ: forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n. Proof. intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto. - omega. omega. + lia. lia. Qed. Lemma Zshiftin_ind: @@ -287,7 +287,7 @@ Proof. - induction p. + change (P (Zshiftin true (Z.pos p))). auto. + change (P (Zshiftin false (Z.pos p))). auto. - + change (P (Zshiftin true 0)). apply H0. omega. auto. + + change (P (Zshiftin true 0)). apply H0. lia. auto. - compute in H1. intuition congruence. Qed. @@ -323,7 +323,7 @@ Remark Ztestbit_succ: forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n. Proof. intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto. - omega. omega. + lia. lia. Qed. Lemma eqmod_same_bits: @@ -335,13 +335,13 @@ Proof. - change (two_power_nat 0) with 1. exists (x-y); ring. - rewrite two_power_nat_S. assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)). - apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; omega. - omega. omega. + apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; lia. + lia. lia. destruct H0 as [k EQ]. exists k. rewrite (Zdecomp x). rewrite (Zdecomp y). replace (Z.odd y) with (Z.odd x). rewrite EQ. rewrite !Zshiftin_spec. ring. - exploit (H 0). rewrite Nat2Z.inj_succ; omega. + exploit (H 0). rewrite Nat2Z.inj_succ; lia. rewrite !Ztestbit_base. auto. Qed. @@ -351,7 +351,7 @@ Lemma same_bits_eqmod: Z.testbit x i = Z.testbit y i. Proof. induction n; intros. - - simpl in H0. omegaContradiction. + - simpl in H0. extlia. - rewrite Nat2Z.inj_succ in H0. rewrite two_power_nat_S in H. rewrite !(Ztestbit_eq i); intuition. destruct H as [k EQ]. @@ -364,7 +364,7 @@ Proof. exploit Zshiftin_inj; eauto. intros [A B]. destruct (zeq i 0). + auto. - + apply IHn. exists k; auto. omega. + + apply IHn. exists k; auto. lia. Qed. Lemma equal_same_bits: @@ -383,7 +383,7 @@ Proof. replace (- Zshiftin (Z.odd x) y - 1) with (Zshiftin (negb (Z.odd x)) (- y - 1)). rewrite !Ztestbit_shiftin; auto. - destruct (zeq i 0). auto. apply IND. omega. + destruct (zeq i 0). auto. apply IND. lia. rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring. Qed. @@ -395,12 +395,12 @@ Lemma Ztestbit_above: Proof. induction n; intros. - change (two_power_nat 0) with 1 in H. - replace x with 0 by omega. + replace x with 0 by lia. apply Z.testbit_0_l. - rewrite Nat2Z.inj_succ in H0. rewrite Ztestbit_eq. rewrite zeq_false. apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H. - rewrite Zshiftin_spec in H. destruct (Z.odd x); omega. - omega. omega. omega. + rewrite Zshiftin_spec in H. destruct (Z.odd x); lia. + lia. lia. lia. Qed. Lemma Ztestbit_above_neg: @@ -412,10 +412,10 @@ Proof. intros. set (y := -x-1). assert (Z.testbit y i = false). apply Ztestbit_above with n. - unfold y; omega. auto. + unfold y; lia. auto. unfold y in H1. rewrite Z_one_complement in H1. change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto. - omega. + lia. Qed. Lemma Zsign_bit: @@ -425,16 +425,16 @@ Lemma Zsign_bit: Proof. induction n; intros. - change (two_power_nat 1) with 2 in H. - assert (x = 0 \/ x = 1) by omega. + assert (x = 0 \/ x = 1) by lia. destruct H0; subst x; reflexivity. - rewrite Nat2Z.inj_succ. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. rewrite IHn. rewrite two_power_nat_S. destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec. - rewrite zlt_true. auto. destruct (Z.odd x); omega. - rewrite zlt_false. auto. destruct (Z.odd x); omega. + rewrite zlt_true. auto. destruct (Z.odd x); lia. + rewrite zlt_false. auto. destruct (Z.odd x); lia. rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H. - rewrite two_power_nat_S in H. destruct (Z.odd x); omega. - omega. omega. + rewrite two_power_nat_S in H. destruct (Z.odd x); lia. + lia. lia. Qed. Lemma Ztestbit_le: @@ -444,16 +444,16 @@ Lemma Ztestbit_le: x <= y. Proof. intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros. - - replace x with 0. omega. apply equal_same_bits; intros. + - replace x with 0. lia. apply equal_same_bits; intros. rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto. exploit H; eauto. rewrite Ztestbit_0. auto. - assert (Z.div2 x0 <= x). { apply H0. intros. exploit (H1 (Z.succ i)). - omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. + lia. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. } rewrite (Zdecomp x0). rewrite !Zshiftin_spec. - destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega. - exploit (H1 0). omega. rewrite Ztestbit_base; auto. + destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try lia. + exploit (H1 0). lia. rewrite Ztestbit_base; auto. rewrite Ztestbit_shiftin_base. congruence. Qed. @@ -464,16 +464,16 @@ Lemma Ztestbit_mod_two_p: Proof. intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto. - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l. - rewrite zlt_false; auto. omega. + rewrite zlt_false; auto. lia. - intros. rewrite two_p_S; auto. replace (x0 mod (2 * two_p x)) with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)). rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0). - + rewrite zlt_true; auto. omega. + + rewrite zlt_true; auto. lia. + rewrite H0. destruct (zlt (Z.pred i) x). - * rewrite zlt_true; auto. omega. - * rewrite zlt_false; auto. omega. - * omega. + * rewrite zlt_true; auto. lia. + * rewrite zlt_false; auto. lia. + * lia. + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry. apply Zmod_unique with (x1 / two_p x). rewrite !Zshiftin_spec. rewrite Z.add_assoc. f_equal. @@ -481,7 +481,7 @@ Proof. f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto. ring. rewrite Zshiftin_spec. exploit (Z_mod_lt x1 (two_p x)). apply two_p_gt_ZERO; auto. - destruct (Z.odd x0); omega. + destruct (Z.odd x0); lia. Qed. Corollary Ztestbit_two_p_m1: @@ -491,7 +491,7 @@ Proof. intros. replace (two_p n - 1) with ((-1) mod (two_p n)). rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto. apply Zmod_unique with (-1). ring. - exploit (two_p_gt_ZERO n). auto. omega. + exploit (two_p_gt_ZERO n). auto. lia. Qed. Corollary Ztestbit_neg_two_p: @@ -499,7 +499,7 @@ Corollary Ztestbit_neg_two_p: Z.testbit (- (two_p n)) i = if zlt i n then false else true. Proof. intros. - replace (- two_p n) with (- (two_p n - 1) - 1) by omega. + replace (- two_p n) with (- (two_p n - 1) - 1) by lia. rewrite Z_one_complement by auto. rewrite Ztestbit_two_p_m1 by auto. destruct (zlt i n); auto. @@ -516,16 +516,16 @@ Proof. rewrite (Zdecomp x) in *. rewrite (Zdecomp y) in *. transitivity (Z.testbit (Zshiftin (Z.odd x || Z.odd y) (Z.div2 x + Z.div2 y)) i). - f_equal. rewrite !Zshiftin_spec. - exploit (EXCL 0). omega. rewrite !Ztestbit_shiftin_base. intros. + exploit (EXCL 0). lia. rewrite !Ztestbit_shiftin_base. intros. Opaque Z.mul. destruct (Z.odd x); destruct (Z.odd y); simpl in *; discriminate || ring. - rewrite !Ztestbit_shiftin; auto. destruct (zeq i 0). + auto. - + apply IND. omega. intros. - exploit (EXCL (Z.succ j)). omega. + + apply IND. lia. intros. + exploit (EXCL (Z.succ j)). lia. rewrite !Ztestbit_shiftin_succ. auto. - omega. omega. + lia. lia. Qed. (** ** Zero and sign extensions *) @@ -583,8 +583,8 @@ Lemma Znatlike_ind: forall n, P n. Proof. intros. destruct (zle 0 n). - apply natlike_ind; auto. apply H; omega. - apply H. omega. + apply natlike_ind; auto. apply H; lia. + apply H. lia. Qed. Lemma Zzero_ext_spec: @@ -593,16 +593,16 @@ Lemma Zzero_ext_spec: Proof. unfold Zzero_ext. induction n using Znatlike_ind. - intros. rewrite Ziter_base; auto. - rewrite zlt_false. rewrite Ztestbit_0; auto. omega. + rewrite zlt_false. rewrite Ztestbit_0; auto. lia. - intros. rewrite Ziter_succ; auto. rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x); auto. destruct (zeq i 0). - + subst i. rewrite zlt_true; auto. omega. + + subst i. rewrite zlt_true; auto. lia. + rewrite IHn. destruct (zlt (Z.pred i) n). - rewrite zlt_true; auto. omega. - rewrite zlt_false; auto. omega. - omega. + rewrite zlt_true; auto. lia. + rewrite zlt_false; auto. lia. + lia. Qed. Lemma Zsign_ext_spec: @@ -611,29 +611,29 @@ Lemma Zsign_ext_spec: Proof. intros n0 x i I0. unfold Zsign_ext. unfold proj_sumbool; destruct (zlt 0 n0) as [N0|N0]; simpl. -- revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1); [ | omega ]. +- revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1); [ | lia ]. unfold Zsign_ext. intros. destruct (zeq x 1). + subst x; simpl. replace (if zlt i 1 then i else 0) with 0. rewrite Ztestbit_base. destruct (Z.odd x0); [ apply Ztestbit_m1; auto | apply Ztestbit_0 ]. - destruct (zlt i 1); omega. - + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)) by omega. - rewrite Ziter_succ by (unfold x1; omega). rewrite Ztestbit_shiftin by auto. + destruct (zlt i 1); lia. + + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)) by lia. + rewrite Ziter_succ by (unfold x1; lia). rewrite Ztestbit_shiftin by auto. destruct (zeq i 0). - * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega. - * rewrite H by (unfold x1; omega). + * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. lia. + * rewrite H by (unfold x1; lia). unfold x1; destruct (zlt (Z.pred i) (Z.pred x)). - ** rewrite zlt_true by omega. - rewrite (Ztestbit_eq i x0) by omega. - rewrite zeq_false by omega. auto. - ** rewrite zlt_false by omega. - rewrite (Ztestbit_eq (x - 1) x0) by omega. - rewrite zeq_false by omega. auto. -- rewrite Ziter_base by omega. rewrite andb_false_r. + ** rewrite zlt_true by lia. + rewrite (Ztestbit_eq i x0) by lia. + rewrite zeq_false by lia. auto. + ** rewrite zlt_false by lia. + rewrite (Ztestbit_eq (x - 1) x0) by lia. + rewrite zeq_false by lia. auto. +- rewrite Ziter_base by lia. rewrite andb_false_r. rewrite Z.testbit_0_l, Z.testbit_neg_r. auto. - destruct (zlt i n0); omega. + destruct (zlt i n0); lia. Qed. (** [Zzero_ext n x] is [x modulo 2^n] *) @@ -650,14 +650,14 @@ Qed. Lemma Zzero_ext_range: forall n x, 0 <= n -> 0 <= Zzero_ext n x < two_p n. Proof. - intros. rewrite Zzero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. omega. + intros. rewrite Zzero_ext_mod; auto. apply Z_mod_lt. apply two_p_gt_ZERO. lia. Qed. Lemma eqmod_Zzero_ext: forall n x, 0 <= n -> eqmod (two_p n) (Zzero_ext n x) x. Proof. intros. rewrite Zzero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod. - apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. Qed. (** Relation between [Zsign_ext n x] and (Zzero_ext n x] *) @@ -670,13 +670,13 @@ Proof. rewrite Zsign_ext_spec by auto. destruct (Z.testbit x (n - 1)) eqn:SIGNBIT. - set (n' := - two_p n). - replace (Zzero_ext n x - two_p n) with (Zzero_ext n x + n') by (unfold n'; omega). + replace (Zzero_ext n x - two_p n) with (Zzero_ext n x + n') by (unfold n'; lia). rewrite Z_add_is_or; auto. - rewrite Zzero_ext_spec by auto. unfold n'; rewrite Ztestbit_neg_two_p by omega. + rewrite Zzero_ext_spec by auto. unfold n'; rewrite Ztestbit_neg_two_p by lia. destruct (zlt i n). rewrite orb_false_r; auto. auto. - intros. rewrite Zzero_ext_spec by omega. unfold n'; rewrite Ztestbit_neg_two_p by omega. + intros. rewrite Zzero_ext_spec by lia. unfold n'; rewrite Ztestbit_neg_two_p by lia. destruct (zlt j n); auto using andb_false_r. -- replace (Zzero_ext n x - 0) with (Zzero_ext n x) by omega. +- replace (Zzero_ext n x - 0) with (Zzero_ext n x) by lia. rewrite Zzero_ext_spec by auto. destruct (zlt i n); auto. Qed. @@ -688,20 +688,20 @@ Lemma Zsign_ext_range: forall n x, 0 < n -> -two_p (n-1) <= Zsign_ext n x < two_p (n-1). Proof. intros. - assert (A: 0 <= Zzero_ext n x < two_p n) by (apply Zzero_ext_range; omega). + assert (A: 0 <= Zzero_ext n x < two_p n) by (apply Zzero_ext_range; lia). assert (B: Z.testbit (Zzero_ext n x) (n - 1) = if zlt (Zzero_ext n x) (two_p (n - 1)) then false else true). { set (N := Z.to_nat (n - 1)). generalize (Zsign_bit N (Zzero_ext n x)). rewrite ! two_power_nat_two_p. - rewrite inj_S. unfold N; rewrite Z2Nat.id by omega. - intros X; apply X. replace (Z.succ (n - 1)) with n by omega. exact A. + rewrite inj_S. unfold N; rewrite Z2Nat.id by lia. + intros X; apply X. replace (Z.succ (n - 1)) with n by lia. exact A. } assert (C: two_p n = 2 * two_p (n - 1)). - { rewrite <- two_p_S by omega. f_equal; omega. } - rewrite Zzero_ext_spec, zlt_true in B by omega. - rewrite Zsign_ext_zero_ext by omega. rewrite B. - destruct (zlt (Zzero_ext n x) (two_p (n - 1))); omega. + { rewrite <- two_p_S by lia. f_equal; lia. } + rewrite Zzero_ext_spec, zlt_true in B by lia. + rewrite Zsign_ext_zero_ext by lia. rewrite B. + destruct (zlt (Zzero_ext n x) (two_p (n - 1))); lia. Qed. Lemma eqmod_Zsign_ext: @@ -711,9 +711,9 @@ Proof. intros. rewrite Zsign_ext_zero_ext by auto. apply eqmod_trans with (x - 0). apply eqmod_sub. - apply eqmod_Zzero_ext; omega. + apply eqmod_Zzero_ext; lia. exists (if Z.testbit x (n - 1) then 1 else 0). destruct (Z.testbit x (n - 1)); ring. - apply eqmod_refl2; omega. + apply eqmod_refl2; lia. Qed. (** ** Decomposition of a number as a sum of powers of two. *) @@ -743,19 +743,19 @@ Proof. { induction n; intros. simpl. rewrite two_power_nat_O in H0. - assert (x = 0) by omega. subst x. omega. + assert (x = 0) by lia. subst x. lia. rewrite two_power_nat_S in H0. simpl Z_one_bits. rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0. assert (EQ: Z.div2 x * two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))). - apply IHn. omega. - destruct (Z.odd x); omega. + apply IHn. lia. + destruct (Z.odd x); lia. rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ. rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec. destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring. - omega. omega. + lia. lia. } - intros. rewrite <- H. change (two_p 0) with 1. omega. - omega. exact H0. + intros. rewrite <- H. change (two_p 0) with 1. lia. + lia. exact H0. Qed. Lemma Z_one_bits_range: @@ -768,12 +768,12 @@ Proof. tauto. intros x i j. rewrite Nat2Z.inj_succ. assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)). - intros. exploit IHn; eauto. omega. + intros. exploit IHn; eauto. lia. destruct (Z.odd x); simpl. - intros [A|B]. subst j. omega. auto. + intros [A|B]. subst j. lia. auto. auto. } - intros. generalize (H n x 0 i H0). omega. + intros. generalize (H n x 0 i H0). lia. Qed. Remark Z_one_bits_zero: @@ -787,15 +787,15 @@ Remark Z_one_bits_two_p: 0 <= x < Z.of_nat n -> Z_one_bits n (two_p x) i = (i + x) :: nil. Proof. - induction n; intros; simpl. simpl in H. omegaContradiction. + induction n; intros; simpl. simpl in H. extlia. rewrite Nat2Z.inj_succ in H. - assert (x = 0 \/ 0 < x) by omega. destruct H0. - subst x; simpl. decEq. omega. apply Z_one_bits_zero. + assert (x = 0 \/ 0 < x) by lia. destruct H0. + subst x; simpl. decEq. lia. apply Z_one_bits_zero. assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)). apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec. - rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; omega. omega. + rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; lia. lia. destruct H1 as [A B]; rewrite A; rewrite B. - rewrite IHn. f_equal; omega. omega. + rewrite IHn. f_equal; lia. lia. Qed. (** ** Recognition of powers of two *) @@ -820,7 +820,7 @@ Proof. induction p; simpl P_is_power2; intros. - discriminate. - change (Z.pos p~0) with (2 * Z.pos p). apply IHp in H. - rewrite Z.log2_double by xomega. rewrite two_p_S. congruence. + rewrite Z.log2_double by extlia. rewrite two_p_S. congruence. apply Z.log2_nonneg. - reflexivity. Qed. @@ -848,7 +848,7 @@ Proof. intros. assert (x <> 0) by (red; intros; subst x; discriminate). apply Z_is_power2_sound in H1. destruct H1 as [P Q]. subst i. - split. apply Z.log2_nonneg. apply Z.log2_lt_pow2. omega. rewrite <- two_p_equiv; tauto. + split. apply Z.log2_nonneg. apply Z.log2_lt_pow2. lia. rewrite <- two_p_equiv; tauto. Qed. Lemma Z_is_power2_complete: @@ -858,11 +858,11 @@ Opaque Z.log2. assert (A: forall x i, Z_is_power2 x = Some i -> Z_is_power2 (2 * x) = Some (Z.succ i)). { destruct x; simpl; intros; try discriminate. change (2 * Z.pos p) with (Z.pos (xO p)); simpl. - destruct (P_is_power2 p); inv H. rewrite <- Z.log2_double by xomega. auto. + destruct (P_is_power2 p); inv H. rewrite <- Z.log2_double by extlia. auto. } induction i using Znatlike_ind; intros. -- replace i with 0 by omega. reflexivity. -- rewrite two_p_S by omega. apply A. apply IHi; omega. +- replace i with 0 by lia. reflexivity. +- rewrite two_p_S by lia. apply A. apply IHi; lia. Qed. Definition Z_is_power2m1 (x: Z) : option Z := Z_is_power2 (Z.succ x). @@ -876,13 +876,13 @@ Qed. Lemma Z_is_power2m1_sound: forall x i, Z_is_power2m1 x = Some i -> x = two_p i - 1. Proof. - unfold Z_is_power2m1; intros. apply Z_is_power2_sound in H. omega. + unfold Z_is_power2m1; intros. apply Z_is_power2_sound in H. lia. Qed. Lemma Z_is_power2m1_complete: forall i, 0 <= i -> Z_is_power2m1 (two_p i - 1) = Some i. Proof. - intros. unfold Z_is_power2m1. replace (Z.succ (two_p i - 1)) with (two_p i) by omega. + intros. unfold Z_is_power2m1. replace (Z.succ (two_p i - 1)) with (two_p i) by lia. apply Z_is_power2_complete; auto. Qed. @@ -891,8 +891,8 @@ Lemma Z_is_power2m1_range: 0 <= n -> 0 <= x < two_p n -> Z_is_power2m1 x = Some i -> 0 <= i <= n. Proof. intros. destruct (zeq x (two_p n - 1)). -- subst x. rewrite Z_is_power2m1_complete in H1 by auto. inv H1; omega. -- unfold Z_is_power2m1 in H1. apply (Z_is_power2_range n (Z.succ x) i) in H1; omega. +- subst x. rewrite Z_is_power2m1_complete in H1 by auto. inv H1; lia. +- unfold Z_is_power2m1 in H1. apply (Z_is_power2_range n (Z.succ x) i) in H1; lia. Qed. (** ** Relation between bitwise operations and multiplications / divisions by powers of 2 *) @@ -903,7 +903,7 @@ Lemma Zshiftl_mul_two_p: forall x n, 0 <= n -> Z.shiftl x n = x * two_p n. Proof. intros. destruct n; simpl. - - omega. + - lia. - pattern p. apply Pos.peano_ind. + change (two_power_pos 1) with 2. simpl. ring. + intros. rewrite Pos.iter_succ. rewrite H0. @@ -925,7 +925,7 @@ Proof. rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp. change (two_power_pos 1) with 2. rewrite Zdiv2_div. rewrite Z.mul_comm. apply Zdiv_Zdiv. - rewrite two_power_pos_nat. apply two_power_nat_pos. omega. + rewrite two_power_pos_nat. apply two_power_nat_pos. lia. - compute in H. congruence. Qed. @@ -938,12 +938,12 @@ Lemma Zquot_Zdiv: Proof. intros. destruct (zlt x 0). - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)). - + red. right; split. omega. + + red. right; split. lia. exploit (Z_mod_lt (x + y - 1) y); auto. - rewrite Z.abs_eq. omega. omega. + rewrite Z.abs_eq. lia. lia. + transitivity ((y * ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)). rewrite <- Z_div_mod_eq. ring. auto. ring. - - apply Zquot_Zdiv_pos; omega. + - apply Zquot_Zdiv_pos; lia. Qed. Lemma Zdiv_shift: @@ -953,8 +953,8 @@ Proof. intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H). set (q := x / y). set (r := x mod y). intros. destruct (zeq r 0). - apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. omega. - apply Zdiv_unique with (r - 1). rewrite H1. ring. omega. + apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. lia. + apply Zdiv_unique with (r - 1). rewrite H1. ring. lia. Qed. (** ** Size of integers, in bits. *) @@ -967,7 +967,7 @@ Definition Zsize (x: Z) : Z := Remark Zsize_pos: forall x, 0 <= Zsize x. Proof. - destruct x; simpl. omega. compute; intuition congruence. omega. + destruct x; simpl. lia. compute; intuition congruence. lia. Qed. Remark Zsize_pos': forall x, 0 < x -> 0 < Zsize x. @@ -991,8 +991,8 @@ Lemma Ztestbit_size_1: Proof. intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto. intros. rewrite Zsize_shiftin; auto. - replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by omega. - rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); omega. + replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by lia. + rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); lia. Qed. Lemma Ztestbit_size_2: @@ -1002,12 +1002,12 @@ Proof. - subst x0; intros. apply Ztestbit_0. - pattern x0; apply Zshiftin_pos_ind. + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin. - rewrite zeq_false. apply Ztestbit_0. omega. omega. + rewrite zeq_false. apply Ztestbit_0. lia. lia. + intros. rewrite Zsize_shiftin in H1; auto. generalize (Zsize_pos' _ H); intros. - rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega. - omega. omega. - + omega. + rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. lia. + lia. lia. + + lia. Qed. Lemma Zsize_interval_1: @@ -1029,18 +1029,18 @@ Proof. assert (Z.of_nat N = n) by (apply Z2Nat.id; auto). rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0. destruct (zeq x 0). - subst x; simpl; omega. + subst x; simpl; lia. destruct (zlt n (Zsize x)); auto. - exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. omega. - rewrite Ztestbit_size_1. congruence. omega. + exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. lia. + rewrite Ztestbit_size_1. congruence. lia. Qed. Lemma Zsize_monotone: forall x y, 0 <= x <= y -> Zsize x <= Zsize y. Proof. intros. apply Z.ge_le. apply Zsize_interval_2. apply Zsize_pos. - exploit (Zsize_interval_1 y). omega. - omega. + exploit (Zsize_interval_1 y). lia. + lia. Qed. (** ** Bit insertion, bit extraction *) @@ -1070,7 +1070,7 @@ Lemma Zextract_s_spec: Proof. unfold Zextract_s; intros. rewrite Zsign_ext_spec by auto. rewrite Z.shiftr_spec. rewrite Z.add_comm. auto. - destruct (zlt i len); omega. + destruct (zlt i len); lia. Qed. (** Insert bits [0...len-1] of [y] into bits [to...to+len-1] of [x] *) @@ -1092,10 +1092,10 @@ Proof. { intros; apply Ztestbit_two_p_m1; auto. } rewrite Z.lor_spec, Z.land_spec, Z.ldiff_spec by auto. destruct (zle to i). -- rewrite ! Z.shiftl_spec by auto. rewrite ! M by omega. +- rewrite ! Z.shiftl_spec by auto. rewrite ! M by lia. unfold proj_sumbool; destruct (zlt (i - to) len); simpl; rewrite andb_true_r, andb_false_r. -+ rewrite zlt_true by omega. apply orb_false_r. -+ rewrite zlt_false by omega; auto. -- rewrite ! Z.shiftl_spec_low by omega. simpl. apply andb_true_r. ++ rewrite zlt_true by lia. apply orb_false_r. ++ rewrite zlt_false by lia; auto. +- rewrite ! Z.shiftl_spec_low by lia. simpl. apply andb_true_r. Qed. -- cgit From dd191041123aa9ef77bd794502d097fffcbcf06b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Dec 2020 11:10:41 +0100 Subject: Add lemma list_norepet_rev --- lib/Coqlib.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 948f128e..ae9dceec 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1011,6 +1011,14 @@ Proof. generalize list_norepet_app; firstorder. Qed. +Lemma list_norepet_rev: + forall (A: Type) (l: list A), list_norepet l -> list_norepet (List.rev l). +Proof. + induction 1; simpl. +- constructor. +- apply list_norepet_append_commut. simpl. constructor; auto. rewrite <- List.in_rev; auto. +Qed. + (** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *) Inductive is_tail (A: Type): list A -> list A -> Prop := -- cgit From bbf3b4140f4263cdcb7dcb9c9a32c8c7651818d8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Dec 2020 11:11:15 +0100 Subject: Add new fold_ind induction principle for folds fold_inv is in Type, hence can prove goals such as `{ x | P x }`. Also, no extensionality property is needed. fold_rec is now derived from fold_inv. --- lib/Maps.v | 145 ++++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 82 insertions(+), 63 deletions(-) (limited to 'lib') diff --git a/lib/Maps.v b/lib/Maps.v index 54d92897..092ab6ea 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1285,103 +1285,122 @@ Module ZTree := ITree(ZIndexed). Module Tree_Properties(T: TREE). -(** An induction principle over [fold]. *) +(** Two induction principles over [fold]. *) Section TREE_FOLD_IND. Variables V A: Type. Variable f: A -> T.elt -> V -> A. -Variable P: T.t V -> A -> Prop. +Variable P: T.t V -> A -> Type. Variable init: A. Variable m_final: T.t V. -Hypothesis P_compat: - forall m m' a, - (forall x, T.get x m = T.get x m') -> - P m a -> P m' a. - Hypothesis H_base: - P (T.empty _) init. + forall m, + (forall k, T.get k m = None) -> + P m init. Hypothesis H_rec: forall m a k v, - T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v). + T.get k m = Some v -> T.get k m_final = Some v -> + P (T.remove k m) a -> P m (f a k v). -Let f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). +Let f' (p : T.elt * V) (a: A) := f a (fst p) (snd p). -Let P' (l: list (T.elt * V)) (a: A) : Prop := - forall m, list_equiv l (T.elements m) -> P m a. +Let P' (l: list (T.elt * V)) (a: A) : Type := + forall m, (forall k v, In (k, v) l <-> T.get k m = Some v) -> P m a. -Remark H_base': +Let H_base': P' nil init. Proof. - red; intros. apply P_compat with (T.empty _); auto. - intros. rewrite T.gempty. symmetry. case_eq (T.get x m); intros; auto. - assert (In (x, v) nil). rewrite (H (x, v)). apply T.elements_correct. auto. - contradiction. + intros m EQV. apply H_base. + intros. destruct (T.get k m) as [v|] eqn:G; auto. + apply EQV in G. contradiction. Qed. -Remark H_rec': +Let H_rec': forall k v l a, - ~In k (List.map (@fst T.elt V) l) -> - In (k, v) (T.elements m_final) -> + ~In k (List.map fst l) -> + T.get k m_final = Some v -> P' l a -> - P' (l ++ (k, v) :: nil) (f a k v). + P' ((k, v) :: l) (f a k v). Proof. - unfold P'; intros. + unfold P'; intros k v l a NOTIN FINAL HR m EQV. set (m0 := T.remove k m). - apply P_compat with (T.set k v m0). - intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k). - symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)). - apply in_or_app. simpl. intuition congruence. - apply T.gro. auto. - apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. - apply H1. red. intros [k' v']. - split; intros. - apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. - rewrite <- (H2 (k', v')). apply in_or_app. auto. - red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto. - assert (T.get k' m0 = Some v'). apply T.elements_complete. auto. - unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence. - assert (In (k', v') (T.elements m)). apply T.elements_correct; auto. - rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. - simpl in H6. intuition congruence. + apply H_rec. +- apply EQV. simpl; auto. +- auto. +- apply HR. intros k' v'. rewrite T.grspec. split; intros; destruct (T.elt_eq k' k). + + subst k'. elim NOTIN. change k with (fst (k, v')). apply List.in_map; auto. + + apply EQV. simpl; auto. + + congruence. + + apply EQV in H. simpl in H. intuition congruence. Qed. -Lemma fold_rec_aux: - forall l1 l2 a, - list_equiv (l2 ++ l1) (T.elements m_final) -> - list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) -> - list_norepet (List.map (@fst T.elt V) l1) -> - P' l2 a -> P' (l2 ++ l1) (List.fold_left f' l1 a). +Lemma fold_ind_aux: + forall l, + (forall k v, In (k, v) l -> T.get k m_final = Some v) -> + list_norepet (List.map fst l) -> + P' l (List.fold_right f' init l). Proof. - induction l1; intros; simpl. - rewrite <- List.app_nil_end. auto. - destruct a as [k v]; simpl in *. inv H1. - change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1. - rewrite app_ass. auto. - red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. - simpl in H4. intuition congruence. - auto. - unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib. - rewrite <- (H (k, v)). apply in_or_app. simpl. auto. + induction l as [ | [k v] l ]; simpl; intros FINAL NOREPET. +- apply H_base'. +- apply H_rec'. + + inv NOREPET. auto. + + apply FINAL. auto. + + apply IHl. auto. inv NOREPET; auto. Qed. -Theorem fold_rec: +Theorem fold_ind: P m_final (T.fold f m_final init). Proof. - intros. rewrite T.fold_spec. fold f'. - assert (P' (nil ++ T.elements m_final) (List.fold_left f' (T.elements m_final) init)). - apply fold_rec_aux. - simpl. red; intros; tauto. - simpl. red; intros. elim H0. - apply T.elements_keys_norepet. - apply H_base'. - simpl in H. red in H. apply H. red; intros. tauto. + intros. + set (l' := List.rev (T.elements m_final)). + assert (P' l' (List.fold_right f' init l')). + { apply fold_ind_aux. + intros. apply T.elements_complete. apply List.in_rev. auto. + unfold l'; rewrite List.map_rev. apply list_norepet_rev. apply T.elements_keys_norepet. } + unfold l', f' in X; rewrite fold_left_rev_right in X. + rewrite T.fold_spec. apply X. + intros; simpl. rewrite <- List.in_rev. + split. apply T.elements_complete. apply T.elements_correct. Qed. End TREE_FOLD_IND. +Section TREE_FOLD_REC. + +Variables V A: Type. +Variable f: A -> T.elt -> V -> A. +Variable P: T.t V -> A -> Prop. +Variable init: A. +Variable m_final: T.t V. + +Hypothesis P_compat: + forall m m' a, + (forall x, T.get x m = T.get x m') -> + P m a -> P m' a. + +Hypothesis H_base: + P (T.empty _) init. + +Hypothesis H_rec: + forall m a k v, + T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v). + +Theorem fold_rec: + P m_final (T.fold f m_final init). +Proof. + apply fold_ind. +- intros. apply P_compat with (T.empty V); auto. + + intros. rewrite T.gempty. auto. +- intros. apply P_compat with (T.set k v (T.remove k m)). + + intros. rewrite T.gsspec, T.grspec. destruct (T.elt_eq x k); auto. congruence. + + apply H_rec; auto. apply T.grs. +Qed. + +End TREE_FOLD_REC. + (** A nonnegative measure over trees *) Section MEASURE. -- cgit From eca149363d20d94198a4b1e1ae4f9f964e468098 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 16:07:24 +0100 Subject: Define `fold_ind_aux` and `fold_ind` transparently The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time. --- lib/Maps.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/Maps.v b/lib/Maps.v index 092ab6ea..c617d488 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1349,7 +1349,7 @@ Proof. + inv NOREPET. auto. + apply FINAL. auto. + apply IHl. auto. inv NOREPET; auto. -Qed. +Defined. Theorem fold_ind: P m_final (T.fold f m_final init). @@ -1364,7 +1364,7 @@ Proof. rewrite T.fold_spec. apply X. intros; simpl. rewrite <- List.in_rev. split. apply T.elements_complete. apply T.elements_correct. -Qed. +Defined. End TREE_FOLD_IND. -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- lib/Coqlib.v | 20 ++++++++++---------- lib/Integers.v | 47 +++++++++++++++++++++++++---------------------- lib/Intv.v | 2 +- 3 files changed, 36 insertions(+), 33 deletions(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index ae9dceec..bd52d20a 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -116,7 +116,7 @@ Lemma Plt_ne: Proof. unfold Plt; intros. red; intro. subst y. eelim Pos.lt_irrefl; eauto. Qed. -Hint Resolve Plt_ne: coqlib. +Global Hint Resolve Plt_ne: coqlib. Lemma Plt_trans: forall (x y z: positive), Plt x y -> Plt y z -> Plt x z. @@ -127,14 +127,14 @@ Lemma Plt_succ: Proof. unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl. Qed. -Hint Resolve Plt_succ: coqlib. +Global Hint Resolve Plt_succ: coqlib. Lemma Plt_trans_succ: forall (x y: positive), Plt x y -> Plt x (Pos.succ y). Proof. intros. apply Plt_trans with y. assumption. apply Plt_succ. Qed. -Hint Resolve Plt_succ: coqlib. +Global Hint Resolve Plt_succ: coqlib. Lemma Plt_succ_inv: forall (x y: positive), Plt x (Pos.succ y) -> Plt x y \/ x = y. @@ -175,7 +175,7 @@ Proof (Pos.lt_le_trans). Lemma Plt_strict: forall p, ~ Plt p p. Proof (Pos.lt_irrefl). -Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. +Global Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. Ltac extlia := unfold Plt, Ple in *; lia. @@ -559,7 +559,7 @@ Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C := (** Properties of [List.nth] (n-th element of a list). *) -Hint Resolve in_eq in_cons: coqlib. +Global Hint Resolve in_eq in_cons: coqlib. Lemma nth_error_in: forall (A: Type) (n: nat) (l: list A) (x: A), @@ -573,14 +573,14 @@ Proof. discriminate. apply in_cons. auto. Qed. -Hint Resolve nth_error_in: coqlib. +Global Hint Resolve nth_error_in: coqlib. Lemma nth_error_nil: forall (A: Type) (idx: nat), nth_error (@nil A) idx = None. Proof. induction idx; simpl; intros; reflexivity. Qed. -Hint Resolve nth_error_nil: coqlib. +Global Hint Resolve nth_error_nil: coqlib. (** Compute the length of a list, with result in [Z]. *) @@ -671,7 +671,7 @@ Lemma incl_cons_inv: Proof. unfold incl; intros. apply H. apply in_cons. auto. Qed. -Hint Resolve incl_cons_inv: coqlib. +Global Hint Resolve incl_cons_inv: coqlib. Lemma incl_app_inv_l: forall (A: Type) (l1 l2 m: list A), @@ -687,7 +687,7 @@ Proof. unfold incl; intros. apply H. apply in_or_app. right; assumption. Qed. -Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. +Global Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. Lemma incl_same_head: forall (A: Type) (x: A) (l1 l2: list A), @@ -1042,7 +1042,7 @@ Proof. constructor. constructor. constructor. auto. Qed. -Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. +Global Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. Lemma is_tail_incl: forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2. diff --git a/lib/Integers.v b/lib/Integers.v index 03f19c98..9368b531 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -91,7 +91,7 @@ Proof. generalize modulus_gt_one; lia. Qed. -Hint Resolve modulus_pos: ints. +Global Hint Resolve modulus_pos: ints. (** * Representation of machine integers *) @@ -400,45 +400,45 @@ Definition eqm := eqmod modulus. Lemma eqm_refl: forall x, eqm x x. Proof (eqmod_refl modulus). -Hint Resolve eqm_refl: ints. +Global Hint Resolve eqm_refl: ints. Lemma eqm_refl2: forall x y, x = y -> eqm x y. Proof (eqmod_refl2 modulus). -Hint Resolve eqm_refl2: ints. +Global Hint Resolve eqm_refl2: ints. Lemma eqm_sym: forall x y, eqm x y -> eqm y x. Proof (eqmod_sym modulus). -Hint Resolve eqm_sym: ints. +Global Hint Resolve eqm_sym: ints. Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z. Proof (eqmod_trans modulus). -Hint Resolve eqm_trans: ints. +Global Hint Resolve eqm_trans: ints. Lemma eqm_small_eq: forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y. Proof (eqmod_small_eq modulus). -Hint Resolve eqm_small_eq: ints. +Global Hint Resolve eqm_small_eq: ints. Lemma eqm_add: forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d). Proof (eqmod_add modulus). -Hint Resolve eqm_add: ints. +Global Hint Resolve eqm_add: ints. Lemma eqm_neg: forall x y, eqm x y -> eqm (-x) (-y). Proof (eqmod_neg modulus). -Hint Resolve eqm_neg: ints. +Global Hint Resolve eqm_neg: ints. Lemma eqm_sub: forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d). Proof (eqmod_sub modulus). -Hint Resolve eqm_sub: ints. +Global Hint Resolve eqm_sub: ints. Lemma eqm_mult: forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d). Proof (eqmod_mult modulus). -Hint Resolve eqm_mult: ints. +Global Hint Resolve eqm_mult: ints. Lemma eqm_same_bits: forall x y, @@ -466,7 +466,7 @@ Lemma eqm_unsigned_repr: Proof. unfold eqm; intros. rewrite unsigned_repr_eq. apply eqmod_mod. auto with ints. Qed. -Hint Resolve eqm_unsigned_repr: ints. +Global Hint Resolve eqm_unsigned_repr: ints. Lemma eqm_unsigned_repr_l: forall a b, eqm a b -> eqm (unsigned (repr a)) b. @@ -474,7 +474,7 @@ Proof. intros. apply eqm_trans with a. apply eqm_sym. apply eqm_unsigned_repr. auto. Qed. -Hint Resolve eqm_unsigned_repr_l: ints. +Global Hint Resolve eqm_unsigned_repr_l: ints. Lemma eqm_unsigned_repr_r: forall a b, eqm a b -> eqm a (unsigned (repr b)). @@ -482,7 +482,7 @@ Proof. intros. apply eqm_trans with b. auto. apply eqm_unsigned_repr. Qed. -Hint Resolve eqm_unsigned_repr_r: ints. +Global Hint Resolve eqm_unsigned_repr_r: ints. Lemma eqm_signed_unsigned: forall x, eqm (signed x) (unsigned x). @@ -497,7 +497,7 @@ Theorem unsigned_range: Proof. destruct i. simpl. lia. Qed. -Hint Resolve unsigned_range: ints. +Global Hint Resolve unsigned_range: ints. Theorem unsigned_range_2: forall i, 0 <= unsigned i <= max_unsigned. @@ -505,7 +505,7 @@ Proof. intro; unfold max_unsigned. generalize (unsigned_range i). lia. Qed. -Hint Resolve unsigned_range_2: ints. +Global Hint Resolve unsigned_range_2: ints. Theorem signed_range: forall i, min_signed <= signed i <= max_signed. @@ -524,7 +524,7 @@ Proof. destruct i; simpl. unfold repr. apply mkint_eq. rewrite Z_mod_modulus_eq. apply Z.mod_small; lia. Qed. -Hint Resolve repr_unsigned: ints. +Global Hint Resolve repr_unsigned: ints. Lemma repr_signed: forall i, repr (signed i) = i. @@ -532,7 +532,7 @@ Proof. intros. transitivity (repr (unsigned i)). apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints. Qed. -Hint Resolve repr_signed: ints. +Global Hint Resolve repr_signed: ints. Opaque repr. @@ -547,7 +547,7 @@ Proof. intros. rewrite unsigned_repr_eq. apply Z.mod_small. unfold max_unsigned in H. lia. Qed. -Hint Resolve unsigned_repr: ints. +Global Hint Resolve unsigned_repr: ints. Theorem signed_repr: forall z, min_signed <= z <= max_signed -> signed (repr z) = z. @@ -4802,7 +4802,7 @@ Qed. End AGREE64. -Hint Resolve +Global Hint Resolve agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs agree64_repr agree64_of_int agree64_of_int_eq @@ -4816,19 +4816,22 @@ Notation ptrofs := Ptrofs.int. Global Opaque Ptrofs.repr. -Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans +Global Hint Resolve + Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r Int.unsigned_range Int.unsigned_range_2 Int.repr_unsigned Int.repr_signed Int.unsigned_repr : ints. -Hint Resolve Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans +Global Hint Resolve + Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r Int64.unsigned_range Int64.unsigned_range_2 Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr : ints. -Hint Resolve Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans +Global Hint Resolve + Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r Ptrofs.unsigned_range Ptrofs.unsigned_range_2 diff --git a/lib/Intv.v b/lib/Intv.v index 19943942..82d3c751 100644 --- a/lib/Intv.v +++ b/lib/Intv.v @@ -303,7 +303,7 @@ Qed. (** Hints *) -Hint Resolve +Global Hint Resolve notin_range range_notin is_notempty empty_notin in_notempty disjoint_sym empty_disjoint_r empty_disjoint_l -- cgit