diff options
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 1212 |
1 files changed, 664 insertions, 548 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 8990c78d..68bff3a0 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -72,7 +73,7 @@ Definition min_signed : Z := - half_modulus. Remark wordsize_pos: zwordsize > 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,15 +84,15 @@ 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. +Global Hint Resolve modulus_pos: ints. (** * Representation of machine integers *) @@ -321,16 +322,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 +347,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: @@ -400,45 +401,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 +467,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 +475,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 +483,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). @@ -495,17 +496,17 @@ 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. +Global Hint Resolve unsigned_range: ints. 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. +Global Hint Resolve unsigned_range_2: ints. Theorem signed_range: forall i, min_signed <= signed i <= max_signed. @@ -513,18 +514,18 @@ 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. +Global Hint Resolve repr_unsigned: ints. Lemma repr_signed: forall i, repr (signed i) = i. @@ -532,7 +533,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. @@ -545,34 +546,34 @@ 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. +Global Hint Resolve unsigned_repr: ints. Theorem signed_repr: forall z, min_signed <= z <= max_signed -> signed (repr z) = z. 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 +581,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 +593,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 +605,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 +637,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 +696,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 +730,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 +742,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 +754,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 +774,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 +784,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 +792,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 +808,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 +851,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 +879,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 +956,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 +1026,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 +1054,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 +1068,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 +1097,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 +1165,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 +1182,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 +1196,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 +1208,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 +1478,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 +1491,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 +1535,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 +1556,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 +1574,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 +1623,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 +1637,7 @@ Proof. destruct (zlt (i + unsigned y) zwordsize). auto. apply bits_above; auto. - omega. + lia. Qed. Lemma bits_shr: @@ -1647,15 +1648,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 +1668,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 +1696,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 +1717,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 +1735,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 +1752,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 +1787,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 +1812,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 +1848,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 +1866,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 +1892,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 +1913,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 +1936,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 +1964,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 +1994,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 +2010,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 +2066,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 +2117,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 +2125,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 +2150,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 +2167,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 +2204,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 +2215,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 +2229,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 +2265,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 +2288,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 +2308,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 +2361,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 +2387,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 +2405,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 +2435,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 +2464,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 +2493,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 +2527,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 +2536,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 +2550,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 +2578,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 +2587,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 +2600,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 +2614,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 +2624,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 +2634,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 +2646,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 +2670,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 +2701,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 +2726,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,41 +2742,41 @@ 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: forall n x, - 0 < n < zwordsize -> + 0 < n <= zwordsize -> let y := repr (zwordsize - n) in sign_ext n x = shr (shl x y) y. 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 +2785,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] @@ -2800,28 +2801,28 @@ Qed. Lemma sign_ext_range: forall n x, 0 < n < zwordsize -> -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1). Proof. - intros. rewrite sign_ext_shr_shl; auto. + intros. rewrite sign_ext_shr_shl by lia. 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 +2831,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 +2847,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 +2858,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 +2871,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 +2885,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 +2897,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 +2911,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 +2925,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 +2940,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 +2956,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 +2971,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 +2985,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 +3016,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 +3060,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 +3071,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 +3093,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 +3130,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 +3144,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 +3187,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 +3204,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 +3239,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 +3256,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 +3271,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 +3286,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 +3300,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 +3321,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 +3336,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 +3346,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 +3370,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 +3384,121 @@ 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. + +(** ** Accessing bit fields *) + +Definition unsigned_bitfield_extract (pos width: Z) (n: int) : int := + zero_ext width (shru n (repr pos)). + +Definition signed_bitfield_extract (pos width: Z) (n: int) : int := + sign_ext width (shru n (repr pos)). + +Definition bitfield_insert (pos width: Z) (n p: int) : int := + let mask := shl (repr (two_p width - 1)) (repr pos) in + or (shl (zero_ext width p) (repr pos)) + (and n (not mask)). + +Lemma bits_unsigned_bitfield_extract: + forall pos width n i, + 0 <= pos -> 0 < width -> pos + width <= zwordsize -> + 0 <= i < zwordsize -> + testbit (unsigned_bitfield_extract pos width n) i = + if zlt i width then testbit n (i + pos) else false. +Proof. + intros. unfold unsigned_bitfield_extract. rewrite bits_zero_ext by lia. + destruct (zlt i width); auto. + rewrite bits_shru by auto. rewrite unsigned_repr, zlt_true. auto. + lia. + generalize wordsize_max_unsigned; lia. +Qed. + +Lemma bits_signed_bitfield_extract: + forall pos width n i, + 0 <= pos -> 0 < width -> pos + width <= zwordsize -> + 0 <= i < zwordsize -> + testbit (signed_bitfield_extract pos width n) i = + testbit n (if zlt i width then i + pos else width - 1 + pos). +Proof. + intros. unfold signed_bitfield_extract. rewrite bits_sign_ext by lia. + rewrite bits_shru, unsigned_repr, zlt_true. + destruct (zlt i width); auto. + destruct (zlt i width); lia. + generalize wordsize_max_unsigned; lia. + destruct (zlt i width); lia. +Qed. + +Lemma bits_bitfield_insert: + forall pos width n p i, + 0 <= pos -> 0 < width -> pos + width <= zwordsize -> + 0 <= i < zwordsize -> + testbit (bitfield_insert pos width n p) i = + if zle pos i && zlt i (pos + width) then testbit p (i - pos) else testbit n i. +Proof. + intros. unfold bitfield_insert. + assert (P: unsigned (repr pos) = pos). + { apply unsigned_repr. generalize wordsize_max_unsigned; lia. } + rewrite bits_or, bits_and, bits_not, ! bits_shl, ! P by auto. + destruct (zlt i pos). +- unfold proj_sumbool; rewrite zle_false by lia. cbn. apply andb_true_r. +- unfold proj_sumbool; rewrite zle_true by lia; cbn. + rewrite bits_zero_ext, testbit_repr, Ztestbit_two_p_m1 by lia. + destruct (zlt (i - pos) width); cbn. ++ rewrite zlt_true by lia. rewrite andb_false_r, orb_false_r. auto. ++ rewrite zlt_false by lia. apply andb_true_r. +Qed. + +Lemma unsigned_bitfield_extract_by_shifts: + forall pos width n, + 0 <= pos -> 0 < width -> pos + width <= zwordsize -> + unsigned_bitfield_extract pos width n = + shru (shl n (repr (zwordsize - pos - width))) (repr (zwordsize - width)). +Proof. + intros. apply same_bits_eq; intros. + rewrite bits_unsigned_bitfield_extract by lia. + rewrite bits_shru by auto. + rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia). + destruct (zlt i width). +- rewrite bits_shl by lia. + rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia). + rewrite zlt_true by lia. rewrite zlt_false by lia. f_equal; lia. +- rewrite zlt_false by lia. auto. +Qed. + +Lemma signed_bitfield_extract_by_shifts: + forall pos width n, + 0 <= pos -> 0 < width -> pos + width <= zwordsize -> + signed_bitfield_extract pos width n = + shr (shl n (repr (zwordsize - pos - width))) (repr (zwordsize - width)). +Proof. + intros. apply same_bits_eq; intros. + rewrite bits_signed_bitfield_extract by lia. + rewrite bits_shr by auto. + rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia). + rewrite bits_shl. + rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia). + symmetry. rewrite zlt_false. f_equal. + destruct (zlt i width); [rewrite zlt_true | rewrite zlt_false]; lia. + destruct zlt; lia. + destruct zlt; lia. +Qed. + +Lemma bitfield_insert_alternative: + forall pos width n p, + 0 <= width -> + bitfield_insert pos width n p = + let mask := shl (repr (two_p width - 1)) (repr pos) in + or (and (shl p (repr pos)) mask) + (and n (not mask)). +Proof. + intros. unfold bitfield_insert. + set (m1 := repr (two_p width - 1)). + set (m2 := shl m1 (repr pos)). + f_equal. + rewrite zero_ext_and by lia. fold m1. unfold m2. rewrite <- and_shl. auto. Qed. End Make. @@ -3465,7 +3578,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 +3592,7 @@ Proof. destruct (zlt (i + Int.unsigned y) zwordsize). auto. apply bits_above; auto. - omega. + lia. Qed. Lemma bits_shr': @@ -3490,8 +3603,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 +3613,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 +3664,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 +3685,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 +3719,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 +3737,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 +3753,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 +3774,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 +3795,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 +3820,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 +3847,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 +3874,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 +3887,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 +3900,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 +3911,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 +3926,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 +3940,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 +3955,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 +3971,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 +3986,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 +4010,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 +4030,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 +4049,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 +4068,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 +4116,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 +4131,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 +4147,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 +4156,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 +4169,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 +4183,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 +4207,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 +4222,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 +4267,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 +4294,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 +4315,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 +4346,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 +4368,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 +4401,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 +4555,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 +4574,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 +4585,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 +4604,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 +4620,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 +4640,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 +4800,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,12 +4910,12 @@ 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. -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 +4929,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 |