diff options
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index c48af2fc..6143ab55 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -18,6 +18,7 @@ Require Import Eqdep_dec Zquot Zwf. Require Import Coqlib Zbits Axioms. Require Archi. +Require Import Lia. (** * Comparisons *) @@ -1205,20 +1206,20 @@ Proof. simpl. pose proof half_modulus_pos as HMOD. destruct (zlt 0 half_modulus) as [HMOD' | HMOD']. - 2: omega. + 2: lia. clear HMOD'. destruct (zlt (intval x) half_modulus) as [ LOW | HIGH]. { destruct x as [ix RANGE]. simpl in *. - destruct (zlt ix 0). omega. + destruct (zlt ix 0). lia. reflexivity. } destruct (zlt _ _) as [LOW' | HIGH']; trivial. destruct x as [ix RANGE]. simpl in *. rewrite half_modulus_modulus in *. - omega. + lia. Qed. Local Opaque repr. @@ -2482,20 +2483,20 @@ Proof. clear H. rewrite two_power_nat_two_p. split. - omega. + lia. set (w := (Z.of_nat wordsize)) in *. assert ((two_p 2) <= (two_p w)) as MONO. { apply two_p_monotone. - omega. + lia. } change (two_p 2) with 4 in MONO. - omega. + lia. } generalize wordsize_max_unsigned. fold zwordsize. generalize wordsize_pos. - omega. + lia. } rewrite unsigned_repr by assumption. simpl. @@ -3677,27 +3678,27 @@ Lemma shr'63: Proof. intro. unfold shr', mone, zero. - rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega). + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). apply same_bits_eq. intros i BIT. rewrite testbit_repr by assumption. - rewrite Z.shiftr_spec by omega. - rewrite bits_signed by omega. + rewrite Z.shiftr_spec by lia. + rewrite bits_signed by lia. simpl. change zwordsize with 64 in *. destruct (zlt _ _) as [LT | GE]. { - replace i with 0 in * by omega. + replace i with 0 in * by lia. change (0 + 63) with (zwordsize - 1). rewrite sign_bit_of_signed. destruct (lt x _). - all: rewrite testbit_repr by (change zwordsize with 64 in *; omega). + all: rewrite testbit_repr by (change zwordsize with 64 in *; lia). all: simpl; reflexivity. } change (64 - 1) with (zwordsize - 1). rewrite sign_bit_of_signed. destruct (lt x _). - all: rewrite testbit_repr by (change zwordsize with 64 in *; omega). + all: rewrite testbit_repr by (change zwordsize with 64 in *; lia). { symmetry. apply Ztestbit_m1. tauto. @@ -3711,11 +3712,11 @@ Lemma shru'63: Proof. intro. unfold shru'. - rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega). + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). apply same_bits_eq. intros i BIT. rewrite testbit_repr by assumption. - rewrite Z.shiftr_spec by omega. + rewrite Z.shiftr_spec by lia. unfold lt. rewrite signed_zero. unfold one, zero. @@ -3728,15 +3729,15 @@ Proof. rewrite sign_bit_of_signed. unfold lt. rewrite signed_zero. - destruct (zlt _ _); try omega. + destruct (zlt _ _); try lia. reflexivity. } change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i+63)). - rewrite bits_above by (change zwordsize with 64; omega). + rewrite bits_above by (change zwordsize with 64; lia). rewrite Ztestbit_1. destruct (zeq i 0); trivial. subst i. - omega. + lia. } destruct (zeq i 0) as [IZERO | INONZERO]. { subst i. @@ -3745,14 +3746,14 @@ Proof. unfold lt. rewrite signed_zero. rewrite bits_zero. - destruct (zlt _ _); try omega. + destruct (zlt _ _); try lia. reflexivity. } change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)). rewrite bits_zero. apply bits_above. change zwordsize with 64. - omega. + lia. Qed. Theorem shrx'1_shr': |