diff options
Diffstat (limited to 'lib/Integers.v')
-rw-r--r-- | lib/Integers.v | 1236 |
1 files changed, 618 insertions, 618 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index a3ff5209..a0140e57 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -133,16 +133,16 @@ Proof. induction n; simpl; intros. - rewrite two_power_nat_O. exists (Zpos p). ring. - rewrite two_power_nat_S. destruct p. - + destruct (IHn p) as [y EQ]. exists y. - change (Zpos p~1) with (2 * Zpos p + 1). rewrite EQ. - rewrite Z.succ_double_spec. ring. - + destruct (IHn p) as [y EQ]. exists y. - change (Zpos p~0) with (2 * Zpos p). rewrite EQ. + + destruct (IHn p) as [y EQ]. exists y. + change (Zpos p~1) with (2 * Zpos p + 1). rewrite EQ. + rewrite Z.succ_double_spec. ring. + + destruct (IHn p) as [y EQ]. exists y. + change (Zpos p~0) with (2 * Zpos p). rewrite EQ. rewrite (Z.double_spec (P_mod_two_p p n)). ring. + exists 0; omega. } - intros. - destruct (H n p) as [y EQ]. + intros. + destruct (H n p) as [y EQ]. symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range. Qed. @@ -150,12 +150,12 @@ Lemma Z_mod_modulus_range: forall x, 0 <= Z_mod_modulus x < modulus. Proof. intros; unfold Z_mod_modulus. - destruct x. + destruct x. - generalize modulus_pos; omega. - apply P_mod_two_p_range. - set (r := P_mod_two_p p wordsize). assert (0 <= r < modulus) by apply P_mod_two_p_range. - destruct (zeq r 0). + destruct (zeq r 0). + generalize modulus_pos; omega. + omega. Qed. @@ -171,22 +171,22 @@ Lemma Z_mod_modulus_eq: Proof. intros. unfold Z_mod_modulus. destruct x. - rewrite Zmod_0_l. auto. - - apply P_mod_two_p_eq. + - apply P_mod_two_p_eq. - generalize (P_mod_two_p_range wordsize p) (P_mod_two_p_eq wordsize p). fold modulus. intros A B. exploit (Z_div_mod_eq (Zpos p) modulus). apply modulus_pos. intros C. set (q := Zpos p / modulus) in *. - set (r := P_mod_two_p p wordsize) in *. - rewrite <- B in C. + set (r := P_mod_two_p p wordsize) in *. + rewrite <- B in C. change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0). - + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring. + + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring. generalize modulus_pos; omega. + symmetry. apply Zmod_unique with (-q - 1). rewrite C. ring. omega. Qed. (** The [unsigned] and [signed] functions return the Coq integer corresponding - to the given machine integer, interpreted as unsigned or signed + to the given machine integer, interpreted as unsigned or signed respectively. *) Definition unsigned (n: int) : Z := intval n. @@ -198,7 +198,7 @@ Definition signed (n: int) : Z := (** Conversely, [repr] takes a Coq integer and returns the corresponding machine integer. The argument is treated modulo [modulus]. *) -Definition repr (x: Z) : int := +Definition repr (x: Z) : int := mkint (Z_mod_modulus x) (Z_mod_modulus_range' x). Definition zero := repr 0. @@ -212,12 +212,12 @@ Proof. intros. subst y. assert (forall (n m: Z) (P1 P2: n < m), P1 = P2). { - unfold Zlt; intros. - apply eq_proofs_unicity. + unfold Zlt; intros. + apply eq_proofs_unicity. intros c1 c2. destruct c1; destruct c2; (left; reflexivity) || (right; congruence). } destruct Px as [Px1 Px2]. destruct Py as [Py1 Py2]. - rewrite (H _ _ Px1 Py1). + rewrite (H _ _ Px1 Py1). rewrite (H _ _ Px2 Py2). reflexivity. Qed. @@ -231,7 +231,7 @@ Defined. (** * Arithmetic and logical operations over machine integers *) -Definition eq (x y: int) : bool := +Definition eq (x y: int) : bool := if zeq (unsigned x) (unsigned y) then true else false. Definition lt (x y: int) : bool := if zlt (signed x) (signed y) then true else false. @@ -340,7 +340,7 @@ Definition Zshiftin (b: bool) (x: Z) : Z := *) Definition Zzero_ext (n: Z) (x: Z) : Z := - Z.iter n + Z.iter n (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x))) (fun x => 0) x. @@ -410,8 +410,8 @@ Definition notbool (x: int) : int := if eq x zero then one else zero. Remark half_modulus_power: half_modulus = two_p (zwordsize - 1). Proof. - unfold half_modulus. rewrite modulus_power. - set (ws1 := zwordsize - 1). + unfold half_modulus. rewrite modulus_power. + set (ws1 := zwordsize - 1). replace (zwordsize) with (Zsucc ws1). rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega. unfold ws1. generalize wordsize_pos; omega. @@ -420,8 +420,8 @@ 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. + rewrite half_modulus_power. rewrite modulus_power. + rewrite <- two_p_S. apply f_equal. omega. generalize wordsize_pos; omega. Qed. @@ -454,8 +454,8 @@ Qed. Remark wordsize_max_unsigned: zwordsize <= max_unsigned. Proof. assert (zwordsize < modulus). - rewrite modulus_power. apply two_p_strict. - generalize wordsize_pos. omega. + rewrite modulus_power. apply two_p_strict. + generalize wordsize_pos. omega. unfold max_unsigned. omega. Qed. @@ -468,14 +468,14 @@ Qed. Remark max_signed_unsigned: max_signed < max_unsigned. Proof. - unfold max_signed, max_unsigned. rewrite half_modulus_modulus. + unfold max_signed, max_unsigned. rewrite half_modulus_modulus. generalize half_modulus_pos. omega. Qed. Lemma unsigned_repr_eq: forall x, unsigned (repr x) = Zmod x modulus. Proof. - intros. simpl. apply Z_mod_modulus_eq. + intros. simpl. apply Z_mod_modulus_eq. Qed. Lemma signed_repr_eq: @@ -528,14 +528,14 @@ Qed. Lemma eqmod_mod_eq: forall x y, eqmod x y -> x mod modul = y mod modul. Proof. - intros x y [k EQ]. subst x. + intros x y [k EQ]. subst x. rewrite Zplus_comm. apply Z_mod_plus. auto. Qed. Lemma eqmod_mod: forall x, eqmod x (x mod modul). Proof. - intros; red. exists (x / modul). + intros; red. exists (x / modul). rewrite Zmult_comm. apply Z_div_mod_eq. auto. Qed. @@ -549,7 +549,7 @@ Qed. Lemma eqmod_neg: forall x y, eqmod x y -> eqmod (-x) (-y). Proof. - intros x y [k EQ]; red. exists (-k). rewrite EQ. ring. + intros x y [k EQ]; red. exists (-k). rewrite EQ. ring. Qed. Lemma eqmod_sub: @@ -573,11 +573,11 @@ End EQ_MODULO. Lemma eqmod_divides: forall n m x y, eqmod n x y -> Zdivide m n -> eqmod m x y. Proof. - intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2]. + intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2]. exists (k1*k2). rewrite <- Zmult_assoc. rewrite <- EQ2. auto. -Qed. +Qed. -(** We then specialize these definitions to equality modulo +(** We then specialize these definitions to equality modulo $2^{wordsize}$ #2<sup>wordsize</sup>#. *) Hint Resolve modulus_pos: ints. @@ -630,7 +630,7 @@ Hint Resolve eqm_mult: ints. Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y. Proof. - intros. unfold repr. apply mkint_eq. + intros. unfold repr. apply mkint_eq. rewrite !Z_mod_modulus_eq. apply eqmod_mod_eq. auto with ints. exact H. Qed. @@ -644,7 +644,7 @@ Hint Resolve eqm_unsigned_repr: ints. Lemma eqm_unsigned_repr_l: forall a b, eqm a b -> eqm (unsigned (repr a)) b. Proof. - intros. apply eqm_trans with a. + intros. apply eqm_trans with a. apply eqm_sym. apply eqm_unsigned_repr. auto. Qed. Hint Resolve eqm_unsigned_repr_l: ints. @@ -653,7 +653,7 @@ Lemma eqm_unsigned_repr_r: forall a b, eqm a b -> eqm a (unsigned (repr b)). Proof. intros. apply eqm_trans with b. auto. - apply eqm_unsigned_repr. + apply eqm_unsigned_repr. Qed. Hint Resolve eqm_unsigned_repr_r: ints. @@ -662,7 +662,7 @@ Lemma eqm_signed_unsigned: Proof. intros; red. unfold signed. set (y := unsigned x). case (zlt y half_modulus); intro. - apply eqmod_refl. red; exists (-1); ring. + apply eqmod_refl. red; exists (-1); ring. Qed. Theorem unsigned_range: @@ -675,7 +675,7 @@ Hint Resolve unsigned_range: ints. Theorem unsigned_range_2: forall i, 0 <= unsigned i <= max_unsigned. Proof. - intro; unfold max_unsigned. + intro; unfold max_unsigned. generalize (unsigned_range i). omega. Qed. Hint Resolve unsigned_range_2: ints. @@ -683,13 +683,13 @@ Hint Resolve unsigned_range_2: ints. Theorem signed_range: forall i, min_signed <= signed i <= max_signed. Proof. - intros. unfold signed. + 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 min_signed, max_signed. - rewrite half_modulus_modulus in *. omega. -Qed. + rewrite half_modulus_modulus in *. omega. +Qed. Theorem repr_unsigned: forall i, repr (unsigned i) = i. @@ -702,7 +702,7 @@ Hint Resolve repr_unsigned: ints. Lemma repr_signed: forall i, repr (signed i) = i. Proof. - intros. transitivity (repr (unsigned i)). + intros. transitivity (repr (unsigned i)). apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints. Qed. Hint Resolve repr_signed: ints. @@ -717,7 +717,7 @@ Qed. Theorem unsigned_repr: forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z. Proof. - intros. rewrite unsigned_repr_eq. + intros. rewrite unsigned_repr_eq. apply Zmod_small. unfold max_unsigned in H. omega. Qed. Hint Resolve unsigned_repr: ints. @@ -728,16 +728,16 @@ 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. + symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega. pose (z' := z + modulus). replace (repr z) with (repr z'). replace (unsigned (repr z')) with z'. rewrite zlt_false. unfold z'. omega. unfold z'. unfold min_signed in H. - rewrite half_modulus_modulus. omega. + rewrite half_modulus_modulus. omega. symmetry. apply unsigned_repr. unfold z', max_unsigned. unfold min_signed, max_signed in H. - rewrite half_modulus_modulus. omega. + rewrite half_modulus_modulus. omega. apply eqm_samerepr. unfold z'; red. exists 1. omega. Qed. @@ -765,16 +765,16 @@ Qed. Theorem unsigned_one: unsigned one = 1. Proof. - unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega. - unfold modulus. replace wordsize with (S(pred wordsize)). - rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)). + unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega. + unfold modulus. replace wordsize with (S(pred wordsize)). + rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)). omega. - generalize wordsize_pos. unfold zwordsize. omega. + generalize wordsize_pos. unfold zwordsize. omega. Qed. Theorem unsigned_mone: unsigned mone = modulus - 1. Proof. - unfold mone; rewrite unsigned_repr_eq. + unfold mone; rewrite unsigned_repr_eq. replace (-1) with ((modulus - 1) + (-1) * modulus). rewrite Z_mod_plus_full. apply Zmod_small. generalize modulus_pos. omega. omega. @@ -789,12 +789,12 @@ 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 half_modulus_modulus. generalize half_modulus_pos. omega. Qed. Theorem one_not_zero: one <> zero. Proof. - assert (unsigned one <> unsigned zero). + assert (unsigned one <> unsigned zero). rewrite unsigned_one; rewrite unsigned_zero; congruence. congruence. Qed. @@ -802,7 +802,7 @@ Qed. Theorem unsigned_repr_wordsize: unsigned iwordsize = zwordsize. Proof. - unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small. + unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small. generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. Qed. @@ -820,7 +820,7 @@ Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y. Proof. intros; unfold eq. case (eq_dec x y); intro. subst y. rewrite zeq_true. auto. - rewrite zeq_false. auto. + rewrite zeq_false. auto. destruct x; destruct y. simpl. red; intro. elim n. apply mkint_eq. auto. Qed. @@ -838,11 +838,11 @@ Qed. Theorem eq_signed: forall x y, eq x y = if zeq (signed x) (signed y) then true else false. Proof. - intros. predSpec eq eq_spec x y. - subst x. rewrite zeq_true; auto. + intros. predSpec eq eq_spec x y. + subst x. rewrite zeq_true; auto. destruct (zeq (signed x) (signed y)); auto. elim H. rewrite <- (repr_signed x). rewrite <- (repr_signed y). congruence. -Qed. +Qed. (** ** Properties of addition *) @@ -851,7 +851,7 @@ Proof. intros; reflexivity. Qed. Theorem add_signed: forall x y, add x y = repr (signed x + signed y). -Proof. +Proof. intros. rewrite add_unsigned. apply eqm_samerepr. apply eqm_add; apply eqm_sym; apply eqm_signed_unsigned. Qed. @@ -876,7 +876,7 @@ Proof. set (x' := unsigned x). set (y' := unsigned y). set (z' := unsigned z). - apply eqm_samerepr. + apply eqm_samerepr. apply eqm_trans with ((x' + y') + z'). auto with ints. rewrite <- Zplus_assoc. auto with ints. @@ -884,7 +884,7 @@ Qed. Theorem add_permut: forall x y z, add x (add y z) = add y (add x z). Proof. - intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. + intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. Qed. Theorem add_neg_zero: forall x, add x (neg x) = zero. @@ -901,19 +901,19 @@ Proof. intros. unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r. rewrite unsigned_repr_eq. - generalize (unsigned_range x) (unsigned_range y). intros. + 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. -Qed. + rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. + rewrite unsigned_one. apply Zmod_unique with 1. omega. omega. +Qed. Corollary unsigned_add_either: forall x y, unsigned (add x y) = unsigned x + unsigned y \/ unsigned (add x y) = unsigned x + unsigned y - modulus. Proof. - intros. rewrite unsigned_add_carry. unfold add_carry. - rewrite unsigned_zero. rewrite Zplus_0_r. + intros. rewrite unsigned_add_carry. unfold add_carry. + rewrite unsigned_zero. rewrite Zplus_0_r. destruct (zlt (unsigned x + unsigned y) modulus). rewrite unsigned_zero. left; omega. rewrite unsigned_one. right; omega. @@ -928,7 +928,7 @@ Qed. Theorem neg_zero: neg zero = zero. Proof. - unfold neg. rewrite unsigned_zero. auto. + unfold neg. rewrite unsigned_zero. auto. Qed. Theorem neg_involutive: forall x, neg (neg x) = x. @@ -936,7 +936,7 @@ 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. -Qed. +Qed. Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y). Proof. @@ -952,7 +952,7 @@ Qed. Theorem sub_zero_l: forall x, sub x zero = x. Proof. - intros; unfold sub. rewrite unsigned_zero. + intros; unfold sub. rewrite unsigned_zero. replace (unsigned x - 0) with (unsigned x) by omega. apply repr_unsigned. Qed. @@ -974,7 +974,7 @@ Qed. Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y. Proof. - intros. repeat rewrite sub_add_opp. + intros. repeat rewrite sub_add_opp. repeat rewrite add_assoc. decEq. apply add_commut. Qed. @@ -989,7 +989,7 @@ Theorem sub_shifted: sub (add x z) (add y z) = sub x y. Proof. intros. rewrite sub_add_opp. rewrite neg_add_distr. - rewrite add_assoc. + rewrite add_assoc. rewrite (add_commut (neg y) (neg z)). rewrite <- (add_assoc z). rewrite add_neg_zero. rewrite (add_commut zero). rewrite add_zero. @@ -1010,22 +1010,22 @@ Proof. intros. unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r. rewrite unsigned_repr_eq. - generalize (unsigned_range x) (unsigned_range y). intros. + 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. -Qed. + rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega. + rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. +Qed. (** ** Properties of multiplication *) Theorem mul_commut: forall x y, mul x y = mul y x. Proof. - intros; unfold mul. decEq. ring. + intros; unfold mul. decEq. ring. Qed. Theorem mul_zero: forall x, mul x zero = zero. Proof. - intros; unfold mul. rewrite unsigned_zero. + intros; unfold mul. rewrite unsigned_zero. unfold zero. decEq. ring. Qed. @@ -1038,7 +1038,7 @@ Qed. Theorem mul_mone: forall x, mul x mone = neg x. Proof. - intros; unfold mul, neg. rewrite unsigned_mone. + intros; unfold mul, neg. rewrite unsigned_mone. apply eqm_samerepr. replace (-unsigned x) with (0 - unsigned x) by omega. replace (unsigned x * (modulus - 1)) with (unsigned x * modulus - unsigned x) by ring. @@ -1074,11 +1074,11 @@ Qed. Theorem mul_add_distr_r: forall x y z, mul x (add y z) = add (mul x y) (mul x z). Proof. - intros. rewrite mul_commut. rewrite mul_add_distr_l. + intros. rewrite mul_commut. rewrite mul_add_distr_l. decEq; apply mul_commut. -Qed. +Qed. -Theorem neg_mul_distr_l: +Theorem neg_mul_distr_l: forall x y, neg(mul x y) = mul (neg x) y. Proof. intros. unfold mul, neg. @@ -1093,7 +1093,7 @@ Theorem neg_mul_distr_r: forall x y, neg(mul x y) = mul x (neg y). Proof. intros. rewrite (mul_commut x y). rewrite (mul_commut x (neg y)). - apply neg_mul_distr_l. + apply neg_mul_distr_l. Qed. Theorem mul_signed: @@ -1109,13 +1109,13 @@ Lemma modu_divu_Euclid: forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y). Proof. intros. unfold add, mul, divu, modu. - transitivity (repr (unsigned x)). auto with ints. - apply eqm_samerepr. + transitivity (repr (unsigned x)). auto with ints. + apply eqm_samerepr. set (x' := unsigned x). set (y' := unsigned y). apply eqm_trans with ((x' / y') * y' + x' mod y'). apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq. generalize (unsigned_range y); intro. - assert (unsigned y <> 0). red; intro. + assert (unsigned y <> 0). red; intro. elim H. rewrite <- (repr_unsigned y). unfold zero. congruence. unfold y'. omega. auto with ints. @@ -1124,7 +1124,7 @@ Qed. Theorem modu_divu: forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y). Proof. - intros. + intros. assert (forall a b c, a = add b c -> c = sub a b). intros. subst a. rewrite sub_add_l. rewrite sub_idem. rewrite add_commut. rewrite add_zero. auto. @@ -1135,20 +1135,20 @@ Lemma mods_divs_Euclid: forall x y, x = add (mul (divs x y) y) (mods x y). Proof. intros. unfold add, mul, divs, mods. - transitivity (repr (signed x)). auto with ints. - apply eqm_samerepr. + transitivity (repr (signed x)). auto with ints. + apply eqm_samerepr. set (x' := signed x). set (y' := signed y). apply eqm_trans with ((Z.quot x' y') * y' + Z.rem x' y'). apply eqm_refl2. rewrite Zmult_comm. apply Z.quot_rem'. apply eqm_add; auto with ints. - apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints. - unfold y'. apply eqm_signed_unsigned. + apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints. + unfold y'. apply eqm_signed_unsigned. Qed. Theorem mods_divs: forall x y, mods x y = sub x (mul (divs x y) y). Proof. - intros. + intros. assert (forall a b c, a = add b c -> c = sub a b). intros. subst a. rewrite sub_add_l. rewrite sub_idem. rewrite add_commut. rewrite add_zero. auto. @@ -1171,26 +1171,26 @@ Qed. Theorem divs_mone: forall x, divs x mone = neg x. Proof. - unfold divs, neg; intros. - rewrite signed_mone. + unfold divs, neg; intros. + rewrite signed_mone. replace (Z.quot (signed x) (-1)) with (- (signed x)). - apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned. + apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned. set (x' := signed x). set (one := 1). change (-1) with (- one). rewrite Zquot_opp_r. - assert (Z.quot x' one = x'). + 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. - unfold one; ring. + change (Z.abs one) with 1. + destruct (zle 0 x'). left. omega. right. omega. + unfold one; ring. congruence. Qed. Theorem mods_mone: forall x, mods x mone = zero. Proof. - intros. rewrite mods_divs. rewrite divs_mone. - rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. + intros. rewrite mods_divs. rewrite divs_mone. + rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. Qed. (** ** Bit-level properties *) @@ -1207,14 +1207,14 @@ Qed. Remark Ztestbit_m1: forall n, 0 <= n -> Z.testbit (-1) n = true. Proof. - intros. destruct n; simpl; auto. + intros. destruct n; simpl; auto. Qed. Remark Zshiftin_spec: forall b x, Zshiftin b x = 2 * x + (if b then 1 else 0). Proof. unfold Zshiftin; intros. destruct b. - - rewrite Z.succ_double_spec. omega. + - rewrite Z.succ_double_spec. omega. - rewrite Z.double_spec. omega. Qed. @@ -1222,7 +1222,7 @@ Remark Zshiftin_inj: forall b1 x1 b2 x2, Zshiftin b1 x1 = Zshiftin b2 x2 -> b1 = b2 /\ x1 = x2. Proof. - intros. rewrite !Zshiftin_spec in H. + intros. rewrite !Zshiftin_spec in H. destruct b1; destruct b2. split; [auto|omega]. omegaContradiction. @@ -1235,7 +1235,7 @@ Remark Zdecomp: Proof. intros. destruct x; simpl. - auto. - - destruct p; auto. + - destruct p; auto. - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto. Qed. @@ -1265,7 +1265,7 @@ Qed. Remark Ztestbit_shiftin_succ: forall b x n, 0 <= n -> Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n. Proof. - intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto. + intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto. omega. omega. Qed. @@ -1273,19 +1273,19 @@ Remark Ztestbit_eq: forall n x, 0 <= n -> Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n). Proof. - intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto. + intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto. Qed. Remark Ztestbit_base: forall x, Z.testbit x 0 = Z.odd x. Proof. - intros. rewrite Ztestbit_eq. apply zeq_true. omega. + intros. rewrite Ztestbit_eq. apply zeq_true. omega. Qed. Remark Ztestbit_succ: forall n x, 0 <= n -> Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n. Proof. - intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto. + intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto. omega. omega. Qed. @@ -1296,14 +1296,14 @@ Lemma eqmod_same_bits: Proof. induction n; intros. - change (two_power_nat 0) with 1. exists (x-y); ring. - - rewrite two_power_nat_S. + - rewrite two_power_nat_S. assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)). - apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega. - omega. omega. + apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega. + omega. omega. destruct H0 as [k EQ]. - exists k. rewrite (Zdecomp x). rewrite (Zdecomp y). + exists k. rewrite (Zdecomp x). rewrite (Zdecomp y). replace (Z.odd y) with (Z.odd x). - rewrite EQ. rewrite !Zshiftin_spec. ring. + rewrite EQ. rewrite !Zshiftin_spec. ring. exploit (H 0). rewrite inj_S; omega. rewrite !Ztestbit_base. auto. Qed. @@ -1321,14 +1321,14 @@ Lemma same_bits_eqmod: Proof. induction n; intros. - simpl in H0. omegaContradiction. - - rewrite inj_S in H0. rewrite two_power_nat_S in H. - rewrite !(Ztestbit_eq i); intuition. + - rewrite inj_S in H0. rewrite two_power_nat_S in H. + rewrite !(Ztestbit_eq i); intuition. destruct H as [k EQ]. assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) = Zshiftin (Z.odd y) (k * two_power_nat n + Z.div2 y)). { rewrite (Zdecomp x) in EQ. rewrite (Zdecomp y) in EQ. - rewrite EQ. rewrite !Zshiftin_spec. ring. + rewrite EQ. rewrite !Zshiftin_spec. ring. } exploit Zshiftin_inj; eauto. intros [A B]. destruct (zeq i 0). @@ -1348,8 +1348,8 @@ Remark two_power_nat_infinity: Proof. intros x0 POS0; pattern x0; apply natlike_ind; auto. exists O. compute; auto. - intros. destruct H0 as [n LT]. exists (S n). rewrite two_power_nat_S. - generalize (two_power_nat_pos n). omega. + intros. destruct H0 as [n LT]. exists (S n). rewrite two_power_nat_S. + generalize (two_power_nat_pos n). omega. Qed. Lemma equal_same_bits: @@ -1357,15 +1357,15 @@ Lemma equal_same_bits: (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) -> x = y. Proof. - intros. + intros. set (z := if zlt x y then y - x else x - y). assert (0 <= z). unfold z; destruct (zlt x y); omega. - exploit (two_power_nat_infinity z); auto. intros [n LT]. + exploit (two_power_nat_infinity z); auto. intros [n LT]. assert (eqmod (two_power_nat n) x y). - apply eqmod_same_bits. intros. apply H. tauto. + apply eqmod_same_bits. intros. apply H. tauto. assert (eqmod (two_power_nat n) z 0). - unfold z. destruct (zlt x y). + unfold z. destruct (zlt x y). replace 0 with (y - y) by omega. apply eqmod_sub. apply eqmod_refl. auto. replace 0 with (x - x) by omega. apply eqmod_sub. apply eqmod_refl. apply eqmod_sym; auto. assert (z = 0). @@ -1377,13 +1377,13 @@ Lemma Z_one_complement: forall i, 0 <= i -> forall x, Z.testbit (-x-1) i = negb (Z.testbit x i). Proof. - intros i0 POS0. pattern i0. apply Zlt_0_ind; auto. - intros i IND POS x. + intros i0 POS0. pattern i0. apply Zlt_0_ind; auto. + intros i IND POS x. rewrite (Zdecomp x). set (y := Z.div2 x). replace (- Zshiftin (Z.odd x) y - 1) with (Zshiftin (negb (Z.odd x)) (- y - 1)). - rewrite !Ztestbit_shiftin; auto. - destruct (zeq i 0). auto. apply IND. omega. + rewrite !Ztestbit_shiftin; auto. + destruct (zeq i 0). auto. apply IND. omega. rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring. Qed. @@ -1393,14 +1393,14 @@ Lemma Ztestbit_above: i >= Z.of_nat n -> Z.testbit x i = false. Proof. - induction n; intros. - - change (two_power_nat 0) with 1 in H. - replace x with 0 by omega. + induction n; intros. + - change (two_power_nat 0) with 1 in H. + replace x with 0 by omega. apply Z.testbit_0_l. - rewrite inj_S in H0. rewrite Ztestbit_eq. rewrite zeq_false. - apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H. - rewrite Zshiftin_spec in H. destruct (Z.odd x); omega. - omega. omega. omega. + apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H. + rewrite Zshiftin_spec in H. destruct (Z.odd x); omega. + omega. omega. omega. Qed. Lemma Ztestbit_above_neg: @@ -1410,11 +1410,11 @@ Lemma Ztestbit_above_neg: Z.testbit x i = true. Proof. intros. set (y := -x-1). - assert (Z.testbit y i = false). - apply Ztestbit_above with n. + assert (Z.testbit y i = false). + apply Ztestbit_above with n. unfold y; omega. auto. unfold y in H1. rewrite Z_one_complement in H1. - change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto. + change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto. omega. Qed. @@ -1423,17 +1423,17 @@ Lemma Zsign_bit: 0 <= x < two_power_nat (S n) -> Z.testbit x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true. Proof. - induction n; intros. - - change (two_power_nat 1) with 2 in H. - assert (x = 0 \/ x = 1) by omega. + induction n; intros. + - change (two_power_nat 1) with 2 in H. + assert (x = 0 \/ x = 1) by omega. destruct H0; subst x; reflexivity. - - rewrite inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. - rewrite IHn. rewrite two_power_nat_S. + - rewrite inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. + rewrite IHn. rewrite two_power_nat_S. destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec. - rewrite zlt_true. auto. destruct (Z.odd x); omega. - rewrite zlt_false. auto. destruct (Z.odd x); omega. - rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H. - rewrite two_power_nat_S in H. destruct (Z.odd x); omega. + rewrite zlt_true. auto. destruct (Z.odd x); omega. + rewrite zlt_false. auto. destruct (Z.odd x); omega. + rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H. + rewrite two_power_nat_S in H. destruct (Z.odd x); omega. omega. omega. Qed. @@ -1443,7 +1443,7 @@ Lemma Zshiftin_ind: (forall b x, 0 <= x -> P x -> P (Zshiftin b x)) -> forall x, 0 <= x -> P x. Proof. - intros. destruct x. + intros. destruct x. - auto. - induction p. + change (P (Zshiftin true (Z.pos p))). auto. @@ -1472,16 +1472,16 @@ Lemma Ztestbit_le: x <= y. Proof. intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros. - - replace x with 0. omega. apply equal_same_bits; intros. - rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto. + - replace x with 0. omega. apply equal_same_bits; intros. + rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto. exploit H; eauto. rewrite Ztestbit_0. auto. - assert (Z.div2 x0 <= x). { apply H0. intros. exploit (H1 (Zsucc i)). - omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. + omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto. } - rewrite (Zdecomp x0). rewrite !Zshiftin_spec. + rewrite (Zdecomp x0). rewrite !Zshiftin_spec. destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega. - exploit (H1 0). omega. rewrite Ztestbit_base; auto. + exploit (H1 0). omega. rewrite Ztestbit_base; auto. rewrite Ztestbit_shiftin_base. congruence. Qed. @@ -1502,25 +1502,25 @@ Lemma same_bits_eq: (forall i, 0 <= i < zwordsize -> testbit x i = testbit y i) -> x = y. Proof. - intros. rewrite <- (repr_unsigned x). rewrite <- (repr_unsigned y). + intros. rewrite <- (repr_unsigned x). rewrite <- (repr_unsigned y). apply eqm_samerepr. apply eqm_same_bits. auto. Qed. Lemma bits_above: forall x i, i >= zwordsize -> testbit x i = false. Proof. - intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range. -Qed. + intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range. +Qed. Lemma bits_zero: forall i, testbit zero i = false. Proof. - intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0. + intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0. Qed. Remark bits_one: forall n, testbit one n = zeq n 0. Proof. - unfold testbit; intros. rewrite unsigned_one. apply Ztestbit_1. + unfold testbit; intros. rewrite unsigned_one. apply Ztestbit_1. Qed. Lemma bits_mone: @@ -1539,25 +1539,25 @@ Lemma sign_bit_of_unsigned: Proof. intros. unfold testbit. set (ws1 := pred wordsize). - assert (zwordsize - 1 = Z_of_nat ws1). - unfold zwordsize, ws1, wordsize. + assert (zwordsize - 1 = Z_of_nat ws1). + unfold zwordsize, ws1, wordsize. destruct WS.wordsize as [] eqn:E. elim WS.wordsize_not_zero; auto. - rewrite inj_S. simpl. omega. + rewrite inj_S. simpl. omega. assert (half_modulus = two_power_nat ws1). rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power. rewrite H; rewrite H0. - apply Zsign_bit. rewrite two_power_nat_S. rewrite <- H0. + apply Zsign_bit. rewrite two_power_nat_S. rewrite <- H0. rewrite <- half_modulus_modulus. apply unsigned_range. Qed. - + Lemma bits_signed: forall x i, 0 <= i -> Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1). Proof. intros. destruct (zlt i zwordsize). - - apply same_bits_eqm. apply eqm_signed_unsigned. omega. + - apply same_bits_eqm. apply eqm_signed_unsigned. omega. - 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. @@ -1569,11 +1569,11 @@ 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. fold (testbit y i). destruct (zlt i zwordsize). - apply H. omega. auto. + intros. apply Ztestbit_le. generalize (unsigned_range y); omega. + intros. fold (testbit y i). destruct (zlt i zwordsize). + apply H. omega. auto. fold (testbit x i) in H1. rewrite bits_above in H1; auto. congruence. -Qed. +Qed. (** ** Properties of bitwise and, or, xor *) @@ -1654,7 +1654,7 @@ Qed. Theorem or_zero: forall x, or x zero = x. Proof. - bit_solve. + bit_solve. Qed. Corollary or_zero_l: forall x, or zero x = x. @@ -1664,7 +1664,7 @@ Qed. Theorem or_mone: forall x, or x mone = mone. Proof. - bit_solve. + bit_solve. Qed. Theorem or_idem: forall x, or x x = x. @@ -1677,7 +1677,7 @@ Theorem and_or_distrib: and x (or y z) = or (and x y) (and x z). Proof. bit_solve. apply demorgan1. -Qed. +Qed. Corollary and_or_distrib_l: forall x y z, @@ -1690,8 +1690,8 @@ Theorem or_and_distrib: forall x y z, or x (and y z) = and (or x y) (or x z). Proof. - bit_solve. apply orb_andb_distrib_r. -Qed. + bit_solve. apply orb_andb_distrib_r. +Qed. Corollary or_and_distrib_l: forall x y z, @@ -1702,7 +1702,7 @@ Qed. Theorem and_or_absorb: forall x y, and x (or x y) = x. Proof. - bit_solve. + bit_solve. assert (forall a b, a && (a || b) = a) by destr_bool. auto. Qed. @@ -1716,7 +1716,7 @@ Qed. Theorem xor_commut: forall x y, xor x y = xor y x. Proof. - bit_solve. apply xorb_comm. + bit_solve. apply xorb_comm. Qed. Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z). @@ -1726,7 +1726,7 @@ Qed. Theorem xor_zero: forall x, xor x zero = x. Proof. - bit_solve. apply xorb_false. + bit_solve. apply xorb_false. Qed. Corollary xor_zero_l: forall x, xor zero x = x. @@ -1736,7 +1736,7 @@ Qed. Theorem xor_idem: forall x, xor x x = zero. Proof. - bit_solve. apply xorb_nilpotent. + bit_solve. apply xorb_nilpotent. Qed. Theorem xor_zero_one: xor zero one = one. @@ -1747,7 +1747,7 @@ Proof. apply xor_idem. Qed. Theorem xor_zero_equal: forall x y, xor x y = zero -> x = y. Proof. - intros. apply same_bits_eq; intros. + intros. apply same_bits_eq; intros. assert (xorb (testbit x i) (testbit y i) = false). rewrite <- bits_xor; auto. rewrite H. apply bits_zero. destruct (testbit x i); destruct (testbit y i); reflexivity || discriminate. @@ -1757,23 +1757,23 @@ Theorem and_xor_distrib: forall x y z, and x (xor y z) = xor (and x y) (and x z). Proof. - bit_solve. + bit_solve. assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)) by destr_bool. auto. -Qed. +Qed. Theorem and_le: forall x y, unsigned (and x y) <= unsigned x. Proof. - intros. apply bits_le; intros. + intros. apply bits_le; intros. rewrite bits_and in H0; auto. rewrite andb_true_iff in H0. tauto. Qed. Theorem or_le: forall x y, unsigned x <= unsigned (or x y). Proof. - intros. apply bits_le; intros. - rewrite bits_or; auto. rewrite H0; auto. + intros. apply bits_le; intros. + rewrite bits_or; auto. rewrite H0; auto. Qed. (** Properties of bitwise complement.*) @@ -1781,7 +1781,7 @@ Qed. Theorem not_involutive: forall (x: int), not (not x) = x. Proof. - intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero. + intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero. Qed. Theorem not_zero: @@ -1799,31 +1799,31 @@ Qed. Theorem not_or_and_not: forall x y, not (or x y) = and (not x) (not y). Proof. - bit_solve. apply negb_orb. + bit_solve. apply negb_orb. Qed. Theorem not_and_or_not: forall x y, not (and x y) = or (not x) (not y). Proof. - bit_solve. apply negb_andb. + bit_solve. apply negb_andb. Qed. Theorem and_not_self: forall x, and x (not x) = zero. Proof. - bit_solve. + bit_solve. Qed. Theorem or_not_self: forall x, or x (not x) = mone. Proof. - bit_solve. + bit_solve. Qed. Theorem xor_not_self: forall x, xor x (not x) = mone. Proof. - bit_solve. destruct (testbit x i); auto. + bit_solve. destruct (testbit x i); auto. Qed. Lemma unsigned_not: @@ -1832,7 +1832,7 @@ Proof. intros. transitivity (unsigned (repr(-unsigned x - 1))). f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega. rewrite unsigned_repr_eq. apply Zmod_unique with (-1). - unfold max_unsigned. omega. + unfold max_unsigned. omega. generalize (unsigned_range x). unfold max_unsigned. omega. Qed. @@ -1840,30 +1840,30 @@ Theorem not_neg: forall x, not x = add (neg x) mone. Proof. bit_solve. - rewrite <- (repr_unsigned x) at 1. unfold add. + 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. apply same_bits_eqm; auto. replace (-unsigned x - 1) with (-unsigned x + (-1)) by omega. - apply eqm_add. - unfold neg. apply eqm_unsigned_repr. - rewrite unsigned_mone. exists (-1). ring. + apply eqm_add. + unfold neg. apply eqm_unsigned_repr. + rewrite unsigned_mone. exists (-1). ring. Qed. Theorem neg_not: forall x, neg x = add (not x) one. Proof. - intros. rewrite not_neg. rewrite add_assoc. - replace (add mone one) with zero. rewrite add_zero. auto. - apply eqm_samerepr. rewrite unsigned_mone. rewrite unsigned_one. - exists (-1). ring. + intros. rewrite not_neg. rewrite add_assoc. + replace (add mone one) with zero. rewrite add_zero. auto. + apply eqm_samerepr. rewrite unsigned_mone. rewrite unsigned_one. + exists (-1). ring. Qed. Theorem sub_add_not: forall x y, sub x y = add (add x (not y)) one. Proof. - intros. rewrite sub_add_opp. rewrite neg_not. + intros. rewrite sub_add_opp. rewrite neg_not. rewrite ! add_assoc. auto. Qed. @@ -1883,13 +1883,13 @@ Theorem sub_borrow_add_carry: b = zero \/ b = one -> sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one. Proof. - intros. unfold sub_borrow, add_carry. rewrite unsigned_not. + intros. unfold sub_borrow, add_carry. rewrite unsigned_not. 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. rewrite zlt_false. rewrite xor_idem; auto. - unfold max_unsigned; omega. + unfold max_unsigned; omega. destruct H; subst b. rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto. rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto. @@ -1908,14 +1908,14 @@ 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). omega. 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. omega. intros. + exploit (EXCL (Z.succ j)). omega. rewrite !Ztestbit_shiftin_succ. auto. omega. omega. Qed. @@ -1926,8 +1926,8 @@ 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. - intros. + apply Z_add_is_or. omega. + intros. assert (testbit (and x y) j = testbit zero j) by congruence. autorewrite with ints in H2. assumption. omega. Qed. @@ -1935,9 +1935,9 @@ Qed. Theorem xor_is_or: forall x y, and x y = zero -> xor x y = or x y. Proof. - bit_solve. + bit_solve. assert (testbit (and x y) i = testbit zero i) by congruence. - autorewrite with ints in H1; auto. + autorewrite with ints in H1; auto. destruct (testbit x i); destruct (testbit y i); simpl in *; congruence. Qed. @@ -1957,8 +1957,8 @@ Proof. intros. rewrite add_is_or. rewrite and_or_distrib; auto. rewrite (and_commut x y). - rewrite and_assoc. - repeat rewrite <- (and_assoc x). + rewrite and_assoc. + repeat rewrite <- (and_assoc x). rewrite (and_commut (and x x)). rewrite <- and_assoc. rewrite H. rewrite and_commut. apply and_zero. @@ -1972,8 +1972,8 @@ Lemma bits_shl: testbit (shl x y) i = if zlt i (unsigned y) then false else testbit x (i - unsigned y). Proof. - intros. unfold shl. rewrite testbit_repr; auto. - destruct (zlt i (unsigned y)). + 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. Qed. @@ -1984,11 +1984,11 @@ Lemma bits_shru: testbit (shru x y) i = if zlt (i + unsigned y) zwordsize then testbit x (i + unsigned y) else false. Proof. - intros. unfold shru. rewrite testbit_repr; auto. + intros. unfold shru. rewrite testbit_repr; auto. rewrite Z.shiftr_spec. fold (testbit x (i + unsigned y)). destruct (zlt (i + unsigned y) zwordsize). auto. - apply bits_above; auto. + apply bits_above; auto. omega. Qed. @@ -1998,8 +1998,8 @@ Lemma bits_shr: testbit (shr x y) i = testbit x (if zlt (i + unsigned y) zwordsize then i + unsigned y else zwordsize - 1). Proof. - intros. unfold shr. rewrite testbit_repr; auto. - rewrite Z.shiftr_spec. apply bits_signed. + intros. unfold shr. rewrite testbit_repr; auto. + rewrite Z.shiftr_spec. apply bits_signed. generalize (unsigned_range y); omega. omega. Qed. @@ -2017,10 +2017,10 @@ Lemma bitwise_binop_shl: f' false false = false -> f (shl x n) (shl y n) = shl (f x y) n. Proof. - intros. apply same_bits_eq; intros. + 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); omega. Qed. Theorem and_shl: @@ -2060,22 +2060,22 @@ Qed. Theorem shl_shl: forall x y z, - ltu y iwordsize = true -> + ltu y iwordsize = true -> ltu z iwordsize = true -> ltu (add y z) iwordsize = true -> shl (shl x y) z = shl x (add y z). Proof. - intros. + intros. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. assert (unsigned (add y z) = unsigned y + unsigned z). - unfold add. apply unsigned_repr. + unfold add. apply unsigned_repr. generalize two_wordsize_max_unsigned; omega. - apply same_bits_eq; intros. + 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. destruct (zlt (i - unsigned z) (unsigned y)). - + rewrite bits_shl; auto. rewrite zlt_true. auto. omega. + + rewrite bits_shl; auto. rewrite zlt_true. auto. omega. + rewrite bits_shl; auto. rewrite zlt_false. f_equal. omega. omega. + omega. Qed. @@ -2091,10 +2091,10 @@ Lemma bitwise_binop_shru: f' false false = false -> f (shru x n) (shru y n) = shru (f x y) n. Proof. - intros. apply same_bits_eq; intros. + 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); omega. Qed. Theorem and_shru: @@ -2120,7 +2120,7 @@ Qed. Theorem shru_shru: forall x y z, - ltu y iwordsize = true -> + ltu y iwordsize = true -> ltu z iwordsize = true -> ltu (add y z) iwordsize = true -> shru (shru x y) z = shru x (add y z). @@ -2128,14 +2128,14 @@ Proof. intros. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. assert (unsigned (add y z) = unsigned y + unsigned z). - unfold add. apply unsigned_repr. + unfold add. apply unsigned_repr. generalize two_wordsize_max_unsigned; omega. - apply same_bits_eq; intros. + 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. + + 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. Qed. @@ -2150,10 +2150,10 @@ Lemma bitwise_binop_shr: (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) -> f (shr x n) (shr y n) = shr (f x y) n. Proof. - intros. apply same_bits_eq; intros. + intros. apply same_bits_eq; intros. rewrite H; auto. rewrite !bits_shr; auto. - rewrite H; auto. - destruct (zlt (i + unsigned n) zwordsize). + rewrite H; auto. + destruct (zlt (i + unsigned n) zwordsize). generalize (unsigned_range n); omega. omega. Qed. @@ -2181,7 +2181,7 @@ Qed. Theorem shr_shr: forall x y z, - ltu y iwordsize = true -> + ltu y iwordsize = true -> ltu z iwordsize = true -> ltu (add y z) iwordsize = true -> shr (shr x y) z = shr x (add y z). @@ -2189,14 +2189,14 @@ Proof. intros. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. assert (unsigned (add y z) = unsigned y + unsigned z). - unfold add. apply unsigned_repr. + unfold add. apply unsigned_repr. generalize two_wordsize_max_unsigned; omega. - apply same_bits_eq; intros. + 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 omega. auto. rewrite (zlt_false _ (i + unsigned (add y z))). - destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega. + destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega. omega. destruct (zlt (i + unsigned z) zwordsize); omega. Qed. @@ -2217,8 +2217,8 @@ Theorem shr_and_shru_and: shru (shl z y) y = z -> and (shr x y) z = and (shru x y) z. Proof. - intros. - rewrite <- H. + intros. + rewrite <- H. rewrite and_shru. rewrite and_shr_shru. auto. Qed. @@ -2228,19 +2228,19 @@ Theorem shru_lt_zero: Proof. intros. apply same_bits_eq; intros. rewrite bits_shru; auto. - rewrite unsigned_repr. + rewrite unsigned_repr. destruct (zeq i 0). subst i. rewrite Zplus_0_l. rewrite zlt_true. rewrite sign_bit_of_unsigned. - unfold lt. rewrite signed_zero. unfold signed. + unfold lt. rewrite signed_zero. unfold signed. destruct (zlt (unsigned x) half_modulus). - rewrite zlt_false. auto. generalize (unsigned_range x); omega. - rewrite zlt_true. unfold one; rewrite testbit_repr; auto. - generalize (unsigned_range x); omega. + rewrite zlt_false. auto. generalize (unsigned_range x); omega. + rewrite zlt_true. unfold one; rewrite testbit_repr; auto. + generalize (unsigned_range x); omega. omega. rewrite zlt_false. - unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false. - destruct (lt x zero). + 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. @@ -2256,10 +2256,10 @@ Proof. rewrite unsigned_repr. transitivity (testbit x (zwordsize - 1)). f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega. - rewrite sign_bit_of_unsigned. - unfold lt. rewrite signed_zero. unfold signed. + 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_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. Qed. @@ -2267,18 +2267,18 @@ Qed. (** ** Properties of rotations *) Lemma bits_rol: - forall x y i, + forall x y i, 0 <= i < zwordsize -> testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize). Proof. intros. unfold rol. - exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. - set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). + exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. + set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). intros EQ. - exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. + 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: omega. destruct (zlt i j). - rewrite Z.shiftl_spec_low; auto. simpl. unfold testbit. f_equal. @@ -2289,9 +2289,9 @@ Proof. 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). + f_equal. symmetry. apply Zmod_unique with (-k). rewrite EQ. ring. - omega. omega. omega. omega. + omega. omega. omega. omega. Qed. Lemma bits_ror: @@ -2300,26 +2300,26 @@ Lemma bits_ror: testbit (ror x y) i = testbit x ((i + unsigned y) mod zwordsize). Proof. intros. unfold ror. - exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. - set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). + exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos. + set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize). intros EQ. - exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos. + 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: omega. destruct (zlt (i + j) zwordsize). - - rewrite Z.shiftl_spec_low; auto. rewrite orb_false_r. + - 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. - 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). + 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. + omega. omega. omega. omega. Qed. Hint Rewrite bits_rol bits_ror: ints. @@ -2330,13 +2330,13 @@ Theorem shl_rolm: shl x n = rolm x n (shl mone n). Proof. intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros. - unfold rolm. apply same_bits_eq; intros. - rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto. + unfold rolm. apply same_bits_eq; intros. + rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto. destruct (zlt i (unsigned n)). - rewrite andb_false_r; auto. - - generalize (unsigned_range n); intros. - rewrite bits_mone. rewrite andb_true_r. f_equal. - symmetry. apply Zmod_small. omega. + - generalize (unsigned_range n); intros. + rewrite bits_mone. rewrite andb_true_r. f_equal. + symmetry. apply Zmod_small. omega. omega. Qed. @@ -2346,15 +2346,15 @@ Theorem shru_rolm: shru x n = rolm x (sub iwordsize n) (shru mone n). Proof. intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros. - unfold rolm. apply same_bits_eq; intros. - rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto. + unfold rolm. apply same_bits_eq; intros. + rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto. destruct (zlt (i + unsigned n) zwordsize). - - generalize (unsigned_range n); intros. + - 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. + symmetry. apply Zmod_unique with (-1). ring. omega. rewrite unsigned_repr_wordsize. generalize wordsize_max_unsigned. omega. - omega. + omega. - rewrite andb_false_r; auto. Qed. @@ -2362,8 +2362,8 @@ Theorem rol_zero: forall x, rol x zero = x. Proof. - bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r. - apply Zmod_small; auto. + bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r. + apply Zmod_small; auto. Qed. Lemma bitwise_binop_rol: @@ -2371,8 +2371,8 @@ Lemma bitwise_binop_rol: (forall x y i, 0 <= i < zwordsize -> testbit (f x y) i = f' (testbit x i) (testbit y i)) -> rol (f x y) n = f (rol x n) (rol y n). Proof. - intros. apply same_bits_eq; intros. - rewrite H; auto. rewrite !bits_rol; auto. rewrite H; auto. + intros. apply same_bits_eq; intros. + rewrite H; auto. rewrite !bits_rol; auto. rewrite H; auto. apply Z_mod_lt. apply wordsize_pos. Qed. @@ -2402,11 +2402,11 @@ Theorem rol_rol: Zdivide zwordsize modulus -> rol (rol x n) m = rol x (modu (add n m) iwordsize). Proof. - bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos. + bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos. set (M := unsigned m); set (N := unsigned n). apply eqmod_trans with (i - M - N). apply eqmod_sub. - apply eqmod_sym. apply eqmod_mod. apply wordsize_pos. + apply eqmod_sym. apply eqmod_mod. apply wordsize_pos. apply eqmod_refl. replace (i - M - N) with (i - (M + N)) by omega. apply eqmod_sub. @@ -2416,8 +2416,8 @@ Proof. 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. - eapply eqmod_trans. 2: apply H1. - apply eqmod_refl2. apply eqmod_mod_eq. apply wordsize_pos. auto. + eapply eqmod_trans. 2: apply H1. + apply eqmod_refl2. apply eqmod_mod_eq. apply wordsize_pos. auto. apply Z_mod_lt. apply wordsize_pos. Qed. @@ -2436,7 +2436,7 @@ Theorem rolm_rolm: (and (rol m1 n2) m2). Proof. intros. - unfold rolm. rewrite rol_and. rewrite and_assoc. + unfold rolm. rewrite rol_and. rewrite and_assoc. rewrite rol_rol. reflexivity. auto. Qed. @@ -2444,7 +2444,7 @@ Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2). Proof. - intros; unfold rolm. symmetry. apply and_or_distrib. + intros; unfold rolm. symmetry. apply and_or_distrib. Qed. Theorem ror_rol: @@ -2455,23 +2455,23 @@ Proof. intros. generalize (ltu_iwordsize_inv _ H); intros. apply same_bits_eq; intros. - rewrite bits_ror; auto. rewrite bits_rol; auto. f_equal. + rewrite bits_ror; auto. rewrite bits_rol; auto. f_equal. 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. + apply eqmod_mod_eq. apply wordsize_pos. exists 1. ring. + rewrite unsigned_repr_wordsize. + generalize wordsize_pos; generalize wordsize_max_unsigned; omega. Qed. Theorem ror_rol_neg: forall x y, (zwordsize | modulus) -> ror x y = rol x (neg y). Proof. intros. apply same_bits_eq; intros. - rewrite bits_ror by auto. rewrite bits_rol by auto. - f_equal. apply eqmod_mod_eq. omega. - apply eqmod_trans with (i - (- unsigned y)). - apply eqmod_refl2; omega. + rewrite bits_ror by auto. rewrite bits_rol by auto. + f_equal. apply eqmod_mod_eq. omega. + apply eqmod_trans with (i - (- unsigned y)). + apply eqmod_refl2; omega. apply eqmod_sub. apply eqmod_refl. - apply eqmod_divides with modulus. + apply eqmod_divides with modulus. apply eqm_unsigned_repr. auto. Qed. @@ -2484,17 +2484,17 @@ Theorem or_ror: Proof. intros. generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros. - unfold ror, or, shl, shru. apply same_bits_eq; intros. - rewrite !testbit_repr; auto. + unfold ror, or, shl, shru. apply same_bits_eq; intros. + rewrite !testbit_repr; auto. rewrite !Z.lor_spec. rewrite orb_comm. f_equal; apply same_bits_eqm; auto. - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. - rewrite Zmod_small; auto. - 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. - - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. + rewrite Zmod_small; auto. + 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. + - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal. apply Zmod_small; auto. Qed. @@ -2509,23 +2509,23 @@ Fixpoint powerserie (l: list Z): Z := Lemma Z_one_bits_powerserie: forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0). Proof. - assert (forall n x i, + assert (forall n x i, 0 <= i -> 0 <= x < two_power_nat n -> x * two_p i = powerserie (Z_one_bits n x i)). { induction n; intros. - simpl. rewrite two_power_nat_O in H0. + simpl. rewrite two_power_nat_O in H0. assert (x = 0) by omega. subst x. omega. rewrite two_power_nat_S in H0. simpl Z_one_bits. rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0. assert (EQ: Z.div2 x * two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))). apply IHn. omega. - destruct (Z.odd x); omega. + destruct (Z.odd x); omega. rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ. - rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec. + rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec. destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring. - omega. omega. + omega. omega. } intros. rewrite <- H. change (two_p 0) with 1. omega. omega. exact H0. @@ -2543,7 +2543,7 @@ Proof. assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)). intros. exploit IHn; eauto. omega. destruct (Z.odd x); simpl. - intros [A|B]. subst j. omega. auto. + intros [A|B]. subst j. omega. auto. auto. } intros. generalize (H wordsize x 0 i H0). fold zwordsize; omega. @@ -2572,7 +2572,7 @@ Theorem is_power2_range: Proof. intros. unfold ltu. rewrite unsigned_repr_wordsize. apply zlt_true. generalize (is_power2_rng _ _ H). tauto. -Qed. +Qed. Lemma is_power2_correct: forall n logn, @@ -2589,7 +2589,7 @@ Proof. rewrite unsigned_repr. replace (two_p z) with (two_p z + 0). auto. omega. elim (H z); intros. generalize wordsize_max_unsigned; omega. - auto with coqlib. + auto with coqlib. intros; discriminate. Qed. @@ -2600,9 +2600,9 @@ Remark two_p_range: Proof. intros. split. assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega. - generalize (two_p_monotone_strict _ _ H). - unfold zwordsize; rewrite <- two_power_nat_two_p. - unfold max_unsigned, modulus. omega. + generalize (two_p_monotone_strict _ _ H). + unfold zwordsize; rewrite <- two_power_nat_two_p. + unfold max_unsigned, modulus. omega. Qed. Remark Z_one_bits_zero: @@ -2617,7 +2617,7 @@ Remark Z_one_bits_two_p: Z_one_bits n (two_p x) i = (i + x) :: nil. Proof. induction n; intros; simpl. simpl in H. omegaContradiction. - rewrite inj_S in H. + rewrite inj_S in H. assert (x = 0 \/ 0 < x) by omega. destruct H0. subst x; simpl. decEq. omega. apply Z_one_bits_zero. assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)). @@ -2631,7 +2631,7 @@ Lemma is_power2_two_p: forall n, 0 <= n < zwordsize -> is_power2 (repr (two_p n)) = Some (repr n). Proof. - intros. unfold is_power2. rewrite unsigned_repr. + intros. unfold is_power2. rewrite unsigned_repr. rewrite Z_one_bits_two_p. auto. auto. apply two_p_range. auto. Qed. @@ -2645,7 +2645,7 @@ Lemma Zshiftl_mul_two_p: Proof. intros. destruct n; simpl. - omega. - - pattern p. apply Pos.peano_ind. + - pattern p. apply Pos.peano_ind. + change (two_power_pos 1) with 2. simpl. ring. + intros. rewrite Pos.iter_succ. rewrite H0. rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp. @@ -2658,7 +2658,7 @@ Lemma shl_mul_two_p: shl x y = mul x (repr (two_p (unsigned y))). Proof. intros. unfold shl, mul. apply eqm_samerepr. - rewrite Zshiftl_mul_two_p. auto with ints. + rewrite Zshiftl_mul_two_p. auto with ints. generalize (unsigned_range y); omega. Qed. @@ -2666,7 +2666,7 @@ Theorem shl_mul: forall x y, shl x y = mul x (shl one y). Proof. - intros. + intros. assert (shl one y = repr (two_p (unsigned y))). { rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto. @@ -2690,21 +2690,21 @@ Theorem shifted_or_is_add: unsigned y < two_p n -> or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y). Proof. - intros. rewrite <- add_is_or. - - unfold add. apply eqm_samerepr. apply eqm_add; auto with ints. + intros. rewrite <- add_is_or. + - unfold add. apply eqm_samerepr. apply eqm_add; auto with ints. 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. + apply eqm_mult; auto with ints. apply eqm_unsigned_repr_l. + apply eqm_refl2. rewrite unsigned_repr. auto. generalize wordsize_max_unsigned; omega. - bit_solve. - rewrite unsigned_repr. + rewrite unsigned_repr. destruct (zlt i n). + auto. - + replace (testbit y i) with false. apply andb_false_r. + + 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). apply Ztestbit_above with (Z.to_nat n). - rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0. + rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0. generalize (unsigned_range y); omega. rewrite EQ; auto. + generalize wordsize_max_unsigned; omega. @@ -2717,8 +2717,8 @@ Lemma Zshiftr_div_two_p: Proof. intros. destruct n; unfold Z.shiftr; simpl. - rewrite Zdiv_1_r. auto. - - pattern p. apply Pos.peano_ind. - + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div. + - pattern p. apply Pos.peano_ind. + + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div. + intros. rewrite Pos.iter_succ. rewrite H0. rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp. change (two_power_pos 1) with 2. @@ -2731,7 +2731,7 @@ Lemma shru_div_two_p: forall x y, shru x y = repr (unsigned x / two_p (unsigned y)). Proof. - intros. unfold shru. + intros. unfold shru. rewrite Zshiftr_div_two_p. auto. generalize (unsigned_range y); omega. Qed. @@ -2775,12 +2775,12 @@ Lemma Ztestbit_mod_two_p: Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false. Proof. intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto. - - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l. + - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l. rewrite zlt_false; auto. omega. - - intros. rewrite two_p_S; auto. - replace (x0 mod (2 * two_p x)) + - intros. rewrite two_p_S; auto. + replace (x0 mod (2 * two_p x)) with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)). - rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0). + rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0). + rewrite zlt_true; auto. omega. + rewrite H0. destruct (zlt (Z.pred i) x). * rewrite zlt_true; auto. omega. @@ -2800,10 +2800,10 @@ Corollary Ztestbit_two_p_m1: forall n i, 0 <= n -> 0 <= i -> Z.testbit (two_p n - 1) i = if zlt i n then true else false. Proof. - intros. replace (two_p n - 1) with ((-1) mod (two_p n)). + intros. replace (two_p n - 1) with ((-1) mod (two_p n)). rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto. - apply Zmod_unique with (-1). ring. - exploit (two_p_gt_ZERO n). auto. omega. + apply Zmod_unique with (-1). ring. + exploit (two_p_gt_ZERO n). auto. omega. Qed. Theorem modu_and: @@ -2814,12 +2814,12 @@ Proof. intros. generalize (is_power2_correct _ _ H); intro. generalize (is_power2_rng _ _ H); intro. apply same_bits_eq; intros. - rewrite bits_and; auto. + rewrite bits_and; auto. unfold sub. rewrite testbit_repr; auto. - rewrite H0. rewrite unsigned_one. + rewrite H0. rewrite unsigned_one. unfold modu. rewrite testbit_repr; auto. rewrite H0. - rewrite Ztestbit_mod_two_p. rewrite Ztestbit_two_p_m1. - destruct (zlt i (unsigned logn)). + rewrite Ztestbit_mod_two_p. rewrite Ztestbit_two_p_m1. + destruct (zlt i (unsigned logn)). rewrite andb_true_r; auto. rewrite andb_false_r; auto. tauto. tauto. tauto. tauto. @@ -2834,11 +2834,11 @@ Lemma Zquot_Zdiv: Proof. intros. destruct (zlt x 0). - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)). - + red. right; split. omega. - exploit (Z_mod_lt (x + y - 1) y); auto. + + red. right; split. omega. + exploit (Z_mod_lt (x + y - 1) y); auto. rewrite Z.abs_eq. omega. omega. + transitivity ((y * ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)). - rewrite <- Z_div_mod_eq. ring. auto. ring. + rewrite <- Z_div_mod_eq. ring. auto. ring. - apply Zquot_Zdiv_pos; omega. Qed. @@ -2850,20 +2850,20 @@ Proof. intros. set (uy := unsigned y). assert (0 <= uy < zwordsize - 1). - generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. + generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. generalize wordsize_pos wordsize_max_unsigned; omega. - rewrite shr_div_two_p. unfold shrx. unfold divs. + 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). + symmetry. apply mul_pow2. replace y with (repr uy). apply is_power2_two_p. omega. apply repr_unsigned. rewrite mul_commut. apply mul_one. assert (two_p uy > 0). apply two_p_gt_ZERO. omega. - assert (two_p uy < half_modulus). - rewrite half_modulus_power. + 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. omega. assert (unsigned (shl one y) = two_p uy). rewrite H1. apply unsigned_repr. unfold max_unsigned. omega. assert (signed (shl one y) = two_p uy). @@ -2871,15 +2871,15 @@ Proof. unfold max_signed. generalize min_signed_neg. omega. rewrite H6. rewrite Zquot_Zdiv; auto. - unfold lt. rewrite signed_zero. + unfold lt. rewrite signed_zero. destruct (zlt (signed x) 0); auto. rewrite add_signed. assert (signed (sub (shl one y) one) = two_p uy - 1). - unfold sub. rewrite H5. rewrite unsigned_one. + unfold sub. rewrite H5. rewrite unsigned_one. apply signed_repr. - generalize min_signed_neg. unfold max_signed. omega. + generalize min_signed_neg. unfold max_signed. omega. rewrite H7. rewrite signed_repr. f_equal. f_equal. omega. - generalize (signed_range x). intros. + generalize (signed_range x). intros. assert (two_p uy - 1 <= max_signed). unfold max_signed. omega. omega. Qed. @@ -2888,27 +2888,27 @@ Theorem shrx_shr_2: ltu y (repr (zwordsize - 1)) = true -> shrx x y = shr (add x (shru (shr x (repr (zwordsize - 1))) (sub iwordsize y))) y. Proof. - intros. + intros. rewrite shrx_shr by auto. f_equal. rewrite shr_lt_zero. destruct (lt x zero). - set (uy := unsigned y). generalize (unsigned_range y); fold uy; intros. assert (0 <= uy < zwordsize - 1). - generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. + generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto. generalize wordsize_pos wordsize_max_unsigned; omega. assert (two_p uy < modulus). - rewrite modulus_power. apply two_p_monotone_strict. omega. + rewrite modulus_power. apply two_p_monotone_strict. omega. 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. + 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). - destruct (zlt i uy). + 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. -- replace (shru zero (sub iwordsize y)) with zero. +- replace (shru zero (sub iwordsize y)) with zero. rewrite add_zero; auto. bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto. Qed. @@ -2917,9 +2917,9 @@ Lemma Zdiv_shift: forall x y, y > 0 -> (x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1. Proof. - intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H). + intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H). set (q := x / y). set (r := x mod y). intros. - destruct (zeq r 0). + destruct (zeq r 0). apply Zdiv_unique with (y - 1). rewrite H1. rewrite e. ring. omega. apply Zdiv_unique with (r - 1). rewrite H1. ring. omega. Qed. @@ -2930,8 +2930,8 @@ Theorem shrx_carry: shrx x y = add (shr x y) (shr_carry x y). Proof. intros. rewrite shrx_shr; auto. unfold shr_carry. - unfold lt. set (sx := signed x). rewrite signed_zero. - destruct (zlt sx 0); simpl. + unfold lt. set (sx := signed x). rewrite signed_zero. + destruct (zlt sx 0); simpl. 2: rewrite add_zero; auto. set (uy := unsigned y). assert (0 <= uy < zwordsize - 1). @@ -2943,46 +2943,46 @@ Proof. symmetry. rewrite H1. apply modu_and with (logn := y). rewrite is_power2_two_p. unfold uy. rewrite repr_unsigned. auto. omega. - rewrite H2. rewrite H1. + 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 < modulus). rewrite modulus_power. apply two_p_monotone_strict. omega. - assert (two_p uy < half_modulus). - rewrite half_modulus_power. + 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. 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. + unfold sub. apply eqm_samerepr. apply eqm_sub. apply eqm_sym; apply eqm_unsigned_repr. rewrite unsigned_one. apply eqm_refl. rewrite H7. rewrite add_signed. fold sx. - rewrite (signed_repr (two_p uy - 1)). rewrite signed_repr. - unfold modu. rewrite unsigned_repr. - unfold eq. rewrite unsigned_zero. rewrite unsigned_repr. + rewrite (signed_repr (two_p uy - 1)). rewrite signed_repr. + unfold modu. rewrite unsigned_repr. + unfold eq. rewrite unsigned_zero. rewrite unsigned_repr. assert (unsigned x mod two_p uy = sx mod two_p uy). - apply eqmod_mod_eq; auto. apply eqmod_divides with modulus. + apply eqmod_mod_eq; auto. apply eqmod_divides with modulus. fold eqm. unfold sx. apply eqm_sym. apply eqm_signed_unsigned. - unfold modulus. rewrite two_power_nat_two_p. + 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. rewrite H8. rewrite Zdiv_shift; auto. - unfold add. apply eqm_samerepr. apply eqm_add. - apply eqm_unsigned_repr. + 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 (signed_range x). fold sx. intros. split. omega. unfold max_signed. omega. + generalize min_signed_neg. unfold max_signed. omega. Qed. (** Connections between [shr] and [shru]. *) Lemma shr_shru_positive: forall x y, - signed x >= 0 -> + signed x >= 0 -> shr x y = shru x y. Proof. intros. @@ -2996,7 +2996,7 @@ Proof. intros. assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega. 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. + 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. @@ -3008,7 +3008,7 @@ Theorem shr_and_is_shru_and: forall x y z, lt y zero = false -> shr (and x y) z = shru (and x y) z. Proof. - intros. apply shr_shru_positive. apply and_positive. + intros. apply shr_shru_positive. apply and_positive. unfold lt in H. rewrite signed_zero in H. destruct (zlt (signed y) 0). congruence. auto. Qed. @@ -3017,14 +3017,14 @@ Qed. Lemma Ziter_base: forall (A: Type) n (f: A -> A) x, n <= 0 -> Z.iter n f x = x. Proof. - intros. unfold Z.iter. destruct n; auto. compute in H. elim H; auto. + intros. unfold Z.iter. destruct n; auto. compute in H. elim H; auto. Qed. Lemma Ziter_succ: forall (A: Type) n (f: A -> A) x, 0 <= n -> Z.iter (Z.succ n) f x = f (Z.iter n f x). Proof. - intros. destruct n; simpl. + intros. destruct n; simpl. - auto. - rewrite Pos.add_1_r. apply Pos.iter_succ. - compute in H. elim H; auto. @@ -3037,7 +3037,7 @@ Lemma Znatlike_ind: forall n, P n. Proof. intros. destruct (zle 0 n). - apply natlike_ind; auto. apply H; omega. + apply natlike_ind; auto. apply H; omega. apply H. omega. Qed. @@ -3045,12 +3045,12 @@ Lemma Zzero_ext_spec: forall n x i, 0 <= i -> Z.testbit (Zzero_ext n x) i = if zlt i n then Z.testbit x i else false. Proof. - unfold Zzero_ext. induction n using Znatlike_ind. + unfold Zzero_ext. induction n using Znatlike_ind. - intros. rewrite Ziter_base; auto. rewrite zlt_false. rewrite Ztestbit_0; auto. omega. - - intros. rewrite Ziter_succ; auto. - rewrite Ztestbit_shiftin; auto. - rewrite (Ztestbit_eq i x); auto. + - intros. rewrite Ziter_succ; auto. + rewrite Ztestbit_shiftin; auto. + rewrite (Ztestbit_eq i x); auto. destruct (zeq i 0). + subst i. rewrite zlt_true; auto. omega. + rewrite IHn. destruct (zlt (Z.pred i) n). @@ -3059,12 +3059,12 @@ Proof. omega. Qed. -Lemma bits_zero_ext: +Lemma bits_zero_ext: forall n x i, 0 <= i -> testbit (zero_ext n x) i = if zlt i n then testbit x i else false. Proof. intros. unfold zero_ext. destruct (zlt i zwordsize). - rewrite testbit_repr; auto. rewrite Zzero_ext_spec. auto. auto. + rewrite testbit_repr; auto. rewrite Zzero_ext_spec. auto. auto. rewrite !bits_above; auto. destruct (zlt i n); auto. Qed. @@ -3072,20 +3072,20 @@ Lemma Zsign_ext_spec: forall n x i, 0 <= i -> 0 < n -> Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1). Proof. - intros n0 x i I0 N0. + intros n0 x i I0 N0. revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1). - unfold Zsign_ext. intros. destruct (zeq x 1). - + subst x; simpl. + + subst x; simpl. replace (if zlt i 1 then i else 0) with 0. rewrite Ztestbit_base. - destruct (Z.odd x0). - apply Ztestbit_m1; auto. + destruct (Z.odd x0). + apply Ztestbit_m1; auto. apply Ztestbit_0. destruct (zlt i 1); omega. + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)). - rewrite Ziter_succ. rewrite Ztestbit_shiftin. - destruct (zeq i 0). + rewrite Ziter_succ. rewrite Ztestbit_shiftin. + destruct (zeq i 0). * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega. * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)). rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega. @@ -3097,13 +3097,13 @@ Proof. - omega. Qed. -Lemma bits_sign_ext: +Lemma bits_sign_ext: forall n x i, 0 <= i < zwordsize -> 0 < n -> 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. rewrite Zsign_ext_spec. destruct (zlt i n); auto. - omega. auto. + omega. auto. Qed. Hint Rewrite bits_zero_ext bits_sign_ext: ints. @@ -3119,7 +3119,7 @@ Theorem sign_ext_above: forall n x, n >= zwordsize -> sign_ext n x = x. Proof. intros. apply same_bits_eq; intros. - unfold sign_ext; rewrite testbit_repr; auto. + unfold sign_ext; rewrite testbit_repr; auto. rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. omega. Qed. @@ -3127,22 +3127,22 @@ Theorem zero_ext_and: forall n x, 0 <= n -> zero_ext n x = and x (repr (two_p n - 1)). Proof. bit_solve. rewrite testbit_repr; auto. rewrite Ztestbit_two_p_m1; intuition. - destruct (zlt i n). - rewrite andb_true_r; auto. + destruct (zlt i n). + rewrite andb_true_r; auto. rewrite andb_false_r; auto. tauto. Qed. Theorem zero_ext_mod: - forall n x, 0 <= n < zwordsize -> + forall n x, 0 <= n < zwordsize -> unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n). Proof. intros. apply equal_same_bits. intros. rewrite Ztestbit_mod_two_p; auto. - fold (testbit (zero_ext n x) i). + 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. + rewrite bits_above. rewrite zlt_false; auto. omega. omega. omega. Qed. @@ -3150,8 +3150,8 @@ Theorem zero_ext_widen: forall x n n', 0 <= n <= n' -> zero_ext n' (zero_ext n x) = zero_ext n x. Proof. - bit_solve. destruct (zlt i n). - apply zlt_true. omega. + bit_solve. destruct (zlt i n). + apply zlt_true. omega. destruct (zlt i n'); auto. tauto. tauto. Qed. @@ -3163,11 +3163,11 @@ Proof. intros. destruct (zlt n' zwordsize). bit_solve. destruct (zlt i n'). auto. - rewrite (zlt_false _ i n). + rewrite (zlt_false _ i n). destruct (zlt (n' - 1) n); f_equal; omega. omega. omega. destruct (zlt i n'); omega. - omega. omega. + omega. omega. apply sign_ext_above; auto. Qed. @@ -3176,10 +3176,10 @@ Theorem sign_zero_ext_widen: sign_ext n' (zero_ext n x) = zero_ext n x. Proof. intros. destruct (zlt n' zwordsize). - bit_solve. + bit_solve. destruct (zlt i n'). auto. - rewrite !zlt_false. auto. omega. omega. omega. + rewrite !zlt_false. auto. omega. omega. omega. destruct (zlt i n'); omega. omega. apply sign_ext_above; auto. @@ -3189,8 +3189,8 @@ Theorem zero_ext_narrow: forall x n n', 0 <= n <= n' -> zero_ext n (zero_ext n' x) = zero_ext n x. Proof. - bit_solve. destruct (zlt i n). - apply zlt_true. omega. + bit_solve. destruct (zlt i n). + apply zlt_true. omega. auto. omega. omega. omega. Qed. @@ -3201,10 +3201,10 @@ Theorem sign_ext_narrow: Proof. intros. destruct (zlt n zwordsize). bit_solve. destruct (zlt i n); f_equal; apply zlt_true; omega. - omega. + omega. destruct (zlt i n); omega. omega. omega. - rewrite (sign_ext_above n'). auto. omega. + rewrite (sign_ext_above n'). auto. omega. Qed. Theorem zero_sign_ext_narrow: @@ -3212,7 +3212,7 @@ Theorem zero_sign_ext_narrow: zero_ext n (sign_ext n' x) = zero_ext n x. Proof. intros. destruct (zlt n' zwordsize). - bit_solve. + bit_solve. destruct (zlt i n); auto. rewrite zlt_true; auto. omega. omega. omega. omega. @@ -3235,10 +3235,10 @@ Theorem sign_ext_zero_ext: forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x. Proof. intros. destruct (zlt n zwordsize). - bit_solve. - destruct (zlt i n). + bit_solve. + destruct (zlt i n). rewrite zlt_true; auto. - rewrite zlt_true; auto. omega. + rewrite zlt_true; auto. omega. destruct (zlt i n); omega. rewrite zero_ext_above; auto. Qed. @@ -3268,12 +3268,12 @@ Proof. assert (unsigned y = zwordsize - n). unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega. apply same_bits_eq; intros. - rewrite bits_zero_ext. + rewrite bits_zero_ext. rewrite bits_shru; auto. destruct (zlt i n). - rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. - omega. omega. omega. - rewrite zlt_false. auto. omega. + rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. + omega. omega. omega. + rewrite zlt_false. auto. omega. omega. Qed. @@ -3287,13 +3287,13 @@ Proof. assert (unsigned y = zwordsize - n). unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega. apply same_bits_eq; intros. - rewrite bits_sign_ext. + rewrite bits_sign_ext. rewrite bits_shr; auto. destruct (zlt i n). - rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. - omega. omega. omega. - rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega. - omega. omega. omega. omega. omega. + rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega. + omega. omega. omega. + rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega. + omega. omega. omega. omega. omega. Qed. (** [zero_ext n x] is the unique integer congruent to [x] modulo [2^n] @@ -3302,13 +3302,13 @@ 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. omega. 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. + intros. rewrite zero_ext_mod; auto. apply eqmod_sym. apply eqmod_mod. apply two_p_gt_ZERO. omega. Qed. @@ -3318,25 +3318,25 @@ 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; auto. set (X := shl x (repr (zwordsize - n))). assert (two_p (n - 1) > 0) by (apply two_p_gt_ZERO; omega). assert (unsigned (repr (zwordsize - n)) = zwordsize - n). - apply unsigned_repr. + apply unsigned_repr. split. omega. generalize wordsize_max_unsigned; omega. rewrite shr_div_two_p. rewrite signed_repr. rewrite H1. - apply Zdiv_interval_1. + apply Zdiv_interval_1. omega. omega. apply two_p_gt_ZERO; omega. 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. rewrite <- half_modulus_power. - generalize (signed_range X). unfold min_signed, max_signed. omega. + generalize (signed_range X). unfold min_signed, max_signed. omega. omega. omega. - apply Zdiv_interval_2. apply signed_range. + 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. @@ -3346,13 +3346,13 @@ Lemma eqmod_sign_ext': forall n x, 0 < n < zwordsize -> eqmod (two_p n) (unsigned (sign_ext n x)) (unsigned x). Proof. - intros. + intros. set (N := Z.to_nat n). assert (Z.of_nat N = n) by (apply Z2Nat.id; omega). - 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 <- 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. omega. Qed. @@ -3360,11 +3360,11 @@ Lemma eqmod_sign_ext: forall n x, 0 < n < zwordsize -> eqmod (two_p n) (signed (sign_ext n x)) (unsigned x). Proof. - intros. apply eqmod_trans with (unsigned (sign_ext n x)). - apply eqmod_divides with modulus. apply eqm_signed_unsigned. - exists (two_p (zwordsize - n)). + intros. apply eqmod_trans with (unsigned (sign_ext n x)). + 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. omega. omega. omega. apply eqmod_sign_ext'; auto. Qed. @@ -3374,8 +3374,8 @@ Theorem one_bits_range: forall x i, In i (one_bits x) -> ltu i iwordsize = true. 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. + intros. unfold ltu, iwordsize. apply zlt_true. + repeat rewrite unsigned_repr. tauto. generalize wordsize_max_unsigned; omega. generalize wordsize_max_unsigned; omega. intros. unfold one_bits in H. @@ -3392,21 +3392,21 @@ Fixpoint int_of_one_bits (l: list int) : int := Theorem one_bits_decomp: forall x, x = int_of_one_bits (one_bits x). Proof. - intros. + intros. transitivity (repr (powerserie (Z_one_bits wordsize (unsigned x) 0))). transitivity (repr (unsigned x)). auto with ints. decEq. apply Z_one_bits_powerserie. auto with ints. - unfold one_bits. + unfold one_bits. generalize (Z_one_bits_range (unsigned x)). generalize (Z_one_bits wordsize (unsigned x) 0). induction l. intros; reflexivity. intros; simpl. rewrite <- IHl. unfold add. apply eqm_samerepr. - apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut. - rewrite mul_one. apply eqm_unsigned_repr_r. + apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut. + rewrite mul_one. apply eqm_unsigned_repr_r. rewrite unsigned_repr. auto with ints. - generalize (H a (in_eq _ _)). generalize wordsize_max_unsigned. omega. + generalize (H a (in_eq _ _)). generalize wordsize_max_unsigned. omega. auto with ints. intros; apply H; auto with coqlib. Qed. @@ -3443,7 +3443,7 @@ Lemma translate_eq: Proof. intros. unfold eq. case (zeq (unsigned x) (unsigned y)); intro. unfold add. rewrite e. apply zeq_true. - apply zeq_false. unfold add. red; intro. apply n. + apply zeq_false. unfold add. red; intro. apply n. apply eqm_small_eq; auto with ints. replace (unsigned x) with ((unsigned x + unsigned d) - unsigned d). replace (unsigned y) with ((unsigned y + unsigned d) - unsigned d). @@ -3473,7 +3473,7 @@ Theorem translate_cmpu: Proof. intros. unfold cmpu. rewrite translate_eq. repeat rewrite translate_ltu; auto. -Qed. +Qed. Lemma translate_lt: forall x y d, @@ -3495,13 +3495,13 @@ Theorem translate_cmp: Proof. intros. unfold cmp. rewrite translate_eq. repeat rewrite translate_lt; auto. -Qed. +Qed. Theorem notbool_isfalse_istrue: forall x, is_false x -> is_true (notbool x). Proof. - unfold is_false, is_true, notbool; intros; subst x. - rewrite eq_true. apply one_not_zero. + unfold is_false, is_true, notbool; intros; subst x. + rewrite eq_true. apply one_not_zero. Qed. Theorem notbool_istrue_isfalse: @@ -3527,7 +3527,7 @@ Theorem lt_sub_overflow: forall x y, xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero. Proof. - intros. unfold negative, sub_overflow, lt. rewrite sub_signed. + intros. unfold negative, sub_overflow, lt. rewrite sub_signed. rewrite signed_zero. rewrite Zminus_0_r. generalize (signed_range x) (signed_range y). set (X := signed x); set (Y := signed y). intros RX RY. @@ -3540,19 +3540,19 @@ Proof. + 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_false by omega. replace (signed (repr (X - Y))) with (X - Y - modulus). - rewrite zlt_true by omega. apply xor_idem. - rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y). - rewrite zlt_false; auto. + rewrite zlt_true by omega. 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. destruct (zlt (X - Y) (-half_modulus)). - + unfold proj_sumbool; rewrite zle_false by omega. + + unfold proj_sumbool; rewrite zle_false by omega. replace (signed (repr (X - Y))) with (X - Y + modulus). rewrite zlt_false by omega. apply xor_zero. - rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus). + 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. @@ -3573,8 +3573,8 @@ Lemma no_overlap_sound: unsigned (add base ofs1) + sz1 <= unsigned (add base ofs2) \/ unsigned (add base ofs2) + sz2 <= unsigned (add base ofs1). Proof. - intros. - destruct (andb_prop _ _ H1). clear H1. + intros. + destruct (andb_prop _ _ H1). clear H1. destruct (andb_prop _ _ H2). clear H2. exploit proj_sumbool_true. eexact H1. intro A; clear H1. exploit proj_sumbool_true. eexact H4. intro B; clear H4. @@ -3610,18 +3610,18 @@ Lemma Zsize_shiftin: forall b x, 0 < x -> Zsize (Zshiftin b x) = Zsucc (Zsize x). Proof. intros. destruct x; compute in H; try discriminate. - destruct b. + destruct b. change (Zshiftin true (Zpos p)) with (Zpos (p~1)). - simpl. f_equal. rewrite Pos.add_1_r; auto. + simpl. f_equal. rewrite Pos.add_1_r; auto. change (Zshiftin false (Zpos p)) with (Zpos (p~0)). - simpl. f_equal. rewrite Pos.add_1_r; auto. + simpl. f_equal. rewrite Pos.add_1_r; auto. Qed. Lemma Ztestbit_size_1: forall x, 0 < x -> Z.testbit x (Zpred (Zsize x)) = true. Proof. intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto. - intros. rewrite Zsize_shiftin; auto. + intros. rewrite Zsize_shiftin; auto. replace (Z.pred (Z.succ (Zsize x))) with (Z.succ (Z.pred (Zsize x))) by omega. rewrite Ztestbit_shiftin_succ. auto. generalize (Zsize_pos' x H); omega. Qed. @@ -3629,14 +3629,14 @@ Qed. Lemma Ztestbit_size_2: forall x, 0 <= x -> forall i, i >= Zsize x -> Z.testbit x i = false. Proof. - intros x0 POS0. destruct (zeq x0 0). - - subst x0; intros. apply Ztestbit_0. + intros x0 POS0. destruct (zeq x0 0). + - subst x0; intros. apply Ztestbit_0. - pattern x0; apply Zshiftin_pos_ind. - + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin. + + simpl. intros. change 1 with (Zshiftin true 0). rewrite Ztestbit_shiftin. rewrite zeq_false. apply Ztestbit_0. omega. omega. + intros. rewrite Zsize_shiftin in H1; auto. generalize (Zsize_pos' _ H); intros. - rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega. + rewrite Ztestbit_shiftin. rewrite zeq_false. apply H0. omega. omega. omega. + omega. Qed. @@ -3644,25 +3644,25 @@ Qed. Lemma Zsize_interval_1: forall x, 0 <= x -> 0 <= x < two_p (Zsize x). Proof. - intros. + intros. assert (x = x mod (two_p (Zsize x))). apply equal_same_bits; intros. - rewrite Ztestbit_mod_two_p; auto. - destruct (zlt i (Zsize x)). auto. apply Ztestbit_size_2; auto. - apply Zsize_pos; auto. - rewrite H0 at 1. rewrite H0 at 3. apply Z_mod_lt. apply two_p_gt_ZERO. apply Zsize_pos; auto. + rewrite Ztestbit_mod_two_p; auto. + destruct (zlt i (Zsize x)). auto. apply Ztestbit_size_2; auto. + apply Zsize_pos; auto. + rewrite H0 at 1. rewrite H0 at 3. apply Z_mod_lt. apply two_p_gt_ZERO. apply Zsize_pos; auto. Qed. Lemma Zsize_interval_2: forall x n, 0 <= n -> 0 <= x < two_p n -> n >= Zsize x. Proof. - intros. set (N := Z.to_nat n). + intros. set (N := Z.to_nat n). assert (Z.of_nat N = n) by (apply Z2Nat.id; auto). - rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0. - destruct (zeq x 0). - subst x; simpl; omega. + rewrite <- H1 in H0. rewrite <- two_power_nat_two_p in H0. + destruct (zeq x 0). + subst x; simpl; omega. destruct (zlt n (Zsize x)); auto. - exploit (Ztestbit_above N x (Zpred (Zsize x))). auto. omega. + exploit (Ztestbit_above N x (Zpred (Zsize x))). auto. omega. rewrite Ztestbit_size_1. congruence. omega. Qed. @@ -3670,15 +3670,15 @@ Lemma Zsize_monotone: forall x y, 0 <= x <= y -> Zsize x <= Zsize y. Proof. intros. apply Zge_le. apply Zsize_interval_2. apply Zsize_pos. - exploit (Zsize_interval_1 y). omega. - omega. + exploit (Zsize_interval_1 y). omega. + omega. Qed. Theorem size_zero: size zero = 0. Proof. unfold size; rewrite unsigned_zero; auto. Qed. - + Theorem bits_size_1: forall x, x = zero \/ testbit x (Zpred (size x)) = true. Proof. @@ -3690,8 +3690,8 @@ 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); omega. + fold (size x); omega. Qed. Theorem size_range: @@ -3700,9 +3700,9 @@ Proof. intros; split. apply Zsize_pos. destruct (bits_size_1 x). subst x; unfold size; rewrite unsigned_zero; simpl. generalize wordsize_pos; omega. - destruct (zle (size x) zwordsize); auto. + destruct (zle (size x) zwordsize); auto. rewrite bits_above in H. congruence. omega. -Qed. +Qed. Theorem bits_size_3: forall x n, @@ -3710,10 +3710,10 @@ Theorem bits_size_3: (forall i, n <= i < zwordsize -> testbit x i = false) -> size x <= n. Proof. - intros. destruct (zle (size x) n). auto. - destruct (bits_size_1 x). + intros. destruct (zle (size x) n). auto. + destruct (bits_size_1 x). subst x. unfold size; rewrite unsigned_zero; assumption. - rewrite (H0 (Z.pred (size x))) in H1. congruence. + rewrite (H0 (Z.pred (size x))) in H1. congruence. generalize (size_range x); omega. Qed. @@ -3728,7 +3728,7 @@ Proof. assert (size x <= n). apply bits_size_3; auto. destruct (zlt (size x) n). - rewrite bits_size_2 in H0. congruence. omega. + rewrite bits_size_2 in H0. congruence. omega. omega. Qed. @@ -3747,24 +3747,24 @@ Qed. Theorem size_and: forall a b, size (and a b) <= Z.min (size a) (size b). Proof. - intros. + 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; omega. apply bits_size_3. auto. intros. - rewrite bits_and. zify. subst z z0. destruct H1. - rewrite (bits_size_2 a). auto. omega. - rewrite (bits_size_2 b). apply andb_false_r. omega. + rewrite bits_and. zify. subst z z0. destruct H1. + rewrite (bits_size_2 a). auto. omega. + rewrite (bits_size_2 b). apply andb_false_r. omega. omega. Qed. Corollary and_interval: forall a b, 0 <= unsigned (and a b) < two_p (Z.min (size a) (size b)). Proof. - intros. - generalize (size_interval_1 (and a b)); intros. + 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 size_and. + apply two_p_monotone. split. generalize (size_range (and a b)); omega. + apply size_and. omega. Qed. @@ -3776,42 +3776,42 @@ Proof. subst a. rewrite size_zero. rewrite or_zero_l. zify; omega. destruct (bits_size_1 b). subst b. rewrite size_zero. rewrite or_zero. zify; omega. - 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. - apply bits_size_4. tauto. rewrite bits_or. rewrite H1. apply orb_true_l. + 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. + 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. omega. omega. + intros. rewrite bits_or. rewrite !bits_size_2. auto. omega. omega. omega. Qed. Corollary or_interval: forall a b, 0 <= unsigned (or a b) < two_p (Z.max (size a) (size b)). Proof. - intros. rewrite <- size_or. apply size_interval_1. + intros. rewrite <- size_or. apply size_interval_1. Qed. Theorem size_xor: forall a b, size (xor a b) <= Z.max (size a) (size b). Proof. - intros. + 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; omega. apply bits_size_3. auto. intros. - rewrite bits_xor. rewrite !bits_size_2. auto. + rewrite bits_xor. rewrite !bits_size_2. auto. + zify; omega. zify; omega. - zify; omega. - omega. + omega. Qed. Corollary xor_interval: forall a b, 0 <= unsigned (xor a b) < two_p (Z.max (size a) (size b)). Proof. - intros. - generalize (size_interval_1 (xor a b)); intros. + 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)); omega. apply size_xor. omega. Qed. @@ -3837,7 +3837,7 @@ Notation int := Int.int. Remark int_wordsize_divides_modulus: Zdivide (Z_of_nat Int.wordsize) Int.modulus. Proof. - exists (two_p (32-5)); reflexivity. + exists (two_p (32-5)); reflexivity. Qed. Module Wordsize_8. @@ -3883,8 +3883,8 @@ Lemma bits_shl': testbit (shl' x y) i = if zlt i (Int.unsigned y) then false else testbit x (i - Int.unsigned y). Proof. - intros. unfold shl'. rewrite testbit_repr; auto. - destruct (zlt i (Int.unsigned y)). + 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. Qed. @@ -3895,11 +3895,11 @@ Lemma bits_shru': testbit (shru' x y) i = if zlt (i + Int.unsigned y) zwordsize then testbit x (i + Int.unsigned y) else false. Proof. - intros. unfold shru'. rewrite testbit_repr; auto. + intros. unfold shru'. rewrite testbit_repr; auto. rewrite Z.shiftr_spec. fold (testbit x (i + Int.unsigned y)). destruct (zlt (i + Int.unsigned y) zwordsize). auto. - apply bits_above; auto. + apply bits_above; auto. omega. Qed. @@ -3909,8 +3909,8 @@ Lemma bits_shr': testbit (shr' x y) i = testbit x (if zlt (i + Int.unsigned y) zwordsize then i + Int.unsigned y else zwordsize - 1). Proof. - intros. unfold shr'. rewrite testbit_repr; auto. - rewrite Z.shiftr_spec. apply bits_signed. + intros. unfold shr'. rewrite testbit_repr; auto. + rewrite Z.shiftr_spec. apply bits_signed. generalize (Int.unsigned_range y); omega. omega. Qed. @@ -3927,7 +3927,7 @@ Definition ofwords (hi lo: Int.int) : int := Lemma bits_loword: forall n i, 0 <= i < Int.zwordsize -> Int.testbit (loword n) i = testbit n i. Proof. - intros. unfold loword. rewrite Int.testbit_repr; auto. + intros. unfold loword. rewrite Int.testbit_repr; auto. Qed. Lemma bits_hiword: @@ -3937,7 +3937,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. omega. omega. Qed. Lemma bits_ofwords: @@ -3945,53 +3945,53 @@ Lemma bits_ofwords: testbit (ofwords hi lo) i = if zlt i Int.zwordsize then Int.testbit lo i else Int.testbit hi (i - Int.zwordsize). Proof. - intros. unfold ofwords. rewrite bits_or; auto. rewrite bits_shl; auto. - change (unsigned (repr Int.zwordsize)) with Int.zwordsize. + intros. unfold ofwords. rewrite bits_or; auto. rewrite bits_shl; auto. + change (unsigned (repr Int.zwordsize)) with Int.zwordsize. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. destruct (zlt i Int.zwordsize). - rewrite testbit_repr; auto. + rewrite testbit_repr; auto. rewrite !testbit_repr; auto. - fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto. + fold (Int.testbit lo i). rewrite Int.bits_above. apply orb_false_r. auto. omega. 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. + 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. Qed. Lemma hi_ofwords: forall hi lo, hiword (ofwords hi lo) = hi. Proof. - intros. apply Int.same_bits_eq; intros. + intros. apply Int.same_bits_eq; intros. rewrite bits_hiword; auto. rewrite bits_ofwords. - rewrite zlt_false. f_equal. omega. omega. + rewrite zlt_false. f_equal. omega. omega. assert (zwordsize = 2 * Int.zwordsize) by reflexivity. omega. Qed. Lemma ofwords_recompose: forall n, ofwords (hiword n) (loword n) = n. 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. + 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. Qed. Lemma ofwords_add: forall lo hi, ofwords hi lo = repr (Int.unsigned hi * two_p 32 + Int.unsigned lo). Proof. - intros. unfold ofwords. rewrite shifted_or_is_add. - apply eqm_samerepr. apply eqm_add. apply eqm_mult. + intros. unfold ofwords. rewrite shifted_or_is_add. + apply eqm_samerepr. apply eqm_add. apply eqm_mult. apply eqm_sym; apply eqm_unsigned_repr. - apply eqm_refl. + apply eqm_refl. apply eqm_sym; apply eqm_unsigned_repr. change Int.zwordsize with 32; change zwordsize with 64; omega. - rewrite unsigned_repr. generalize (Int.unsigned_range lo). intros [A B]. exact B. + 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. Qed. @@ -4000,7 +4000,7 @@ Lemma ofwords_add': forall lo hi, unsigned (ofwords hi lo) = Int.unsigned hi * two_p 32 + Int.unsigned lo. Proof. intros. rewrite ofwords_add. apply unsigned_repr. - generalize (Int.unsigned_range hi) (Int.unsigned_range lo). + generalize (Int.unsigned_range hi) (Int.unsigned_range lo). change (two_p 32) with Int.modulus. change Int.modulus with 4294967296. change max_unsigned with 18446744073709551615. @@ -4011,7 +4011,7 @@ Remark eqm_mul_2p32: forall x y, Int.eqm x y -> eqm (x * two_p 32) (y * two_p 32). Proof. intros. destruct H as [k EQ]. exists k. rewrite EQ. - change Int.modulus with (two_p 32). + change Int.modulus with (two_p 32). change modulus with (two_p 32 * two_p 32). ring. Qed. @@ -4023,7 +4023,7 @@ Proof. replace (repr (Int.unsigned hi * two_p 32 + Int.unsigned lo)) with (repr (Int.signed hi * two_p 32 + Int.unsigned lo)). apply signed_repr. - generalize (Int.signed_range hi) (Int.unsigned_range lo). + generalize (Int.signed_range hi) (Int.unsigned_range lo). change (two_p 32) with Int.modulus. change min_signed with (Int.min_signed * Int.modulus). change max_signed with (Int.max_signed * Int.modulus + Int.modulus - 1). @@ -4074,7 +4074,7 @@ Lemma decompose_not: forall xh xl, not (ofwords xh xl) = ofwords (Int.not xh) (Int.not xl). Proof. - intros. unfold not, Int.not. rewrite <- decompose_xor. f_equal. + intros. unfold not, Int.not. rewrite <- decompose_xor. f_equal. apply (Int64.eq_spec mone (ofwords Int.mone Int.mone)). Qed. @@ -4087,21 +4087,21 @@ Lemma decompose_shl_1: Proof. intros. assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). - { unfold Int.sub. rewrite Int.unsigned_repr. auto. + { unfold Int.sub. rewrite Int.unsigned_repr. auto. rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } 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.unsigned y)). auto. + destruct (zlt i Int.zwordsize). rewrite Int.bits_shl by omega. + 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 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. 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_l. f_equal. omega. + rewrite zlt_false by omega. rewrite zlt_false by omega. rewrite orb_false_r. f_equal. omega. Qed. @@ -4114,16 +4114,16 @@ Proof. intros. 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. + { unfold Int.sub. rewrite Int.unsigned_repr. auto. rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } 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. + rewrite Int.bits_shl by omega. 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 omega. auto. + rewrite zlt_false by omega. + rewrite bits_ofwords by omega. rewrite zlt_true by omega. f_equal. omega. Qed. Lemma decompose_shru_1: @@ -4135,25 +4135,25 @@ Lemma decompose_shru_1: Proof. intros. assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). - { unfold Int.sub. rewrite Int.unsigned_repr. auto. + { unfold Int.sub. rewrite Int.unsigned_repr. auto. rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } 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 zlt_true by omega. rewrite bits_ofwords by omega. - rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. + rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. rewrite Int.bits_shru by omega. rewrite H0. destruct (zlt (i + Int.unsigned y) (Int.zwordsize)). rewrite zlt_true by omega. rewrite orb_false_r. auto. - rewrite zlt_false by omega. + rewrite zlt_false by omega. rewrite orb_false_l. f_equal. omega. - rewrite Int.bits_shru by omega. + rewrite Int.bits_shru by omega. 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 bits_ofwords by omega. + rewrite zlt_true by omega. rewrite zlt_false by omega. f_equal. omega. rewrite zlt_false by omega. auto. Qed. @@ -4166,15 +4166,15 @@ Proof. intros. 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. + { unfold Int.sub. rewrite Int.unsigned_repr. auto. rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } 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. 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_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. Qed. @@ -4188,26 +4188,26 @@ Lemma decompose_shr_1: Proof. intros. assert (Int.unsigned (Int.sub Int.iwordsize y) = Int.zwordsize - Int.unsigned y). - { unfold Int.sub. rewrite Int.unsigned_repr. auto. + { unfold Int.sub. rewrite Int.unsigned_repr. auto. rewrite Int.unsigned_repr_wordsize. generalize Int.wordsize_max_unsigned; omega. } 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 zlt_true by omega. rewrite bits_ofwords by omega. - rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. + rewrite Int.bits_or by omega. rewrite Int.bits_shl by omega. rewrite Int.bits_shru by omega. rewrite H0. destruct (zlt (i + Int.unsigned y) (Int.zwordsize)). rewrite zlt_true by omega. rewrite orb_false_r. auto. - rewrite zlt_false by omega. + rewrite zlt_false by omega. rewrite orb_false_l. f_equal. omega. - rewrite Int.bits_shr by omega. + rewrite Int.bits_shr by omega. 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 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. Qed. @@ -4221,24 +4221,24 @@ Proof. intros. 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. + { unfold Int.sub. rewrite Int.unsigned_repr. auto. rewrite Int.unsigned_repr_wordsize. generalize (Int.unsigned_range_2 y). omega. } 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. 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_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 Int.bits_shr by omega. 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. + 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. + symmetry. rewrite zlt_false by omega. f_equal. destruct (zlt (i - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. Qed. @@ -4249,8 +4249,8 @@ Lemma decompose_add: (Int.add xl yl). Proof. intros. symmetry. rewrite ofwords_add. rewrite add_unsigned. - apply eqm_samerepr. - rewrite ! ofwords_add'. rewrite (Int.unsigned_add_carry xl yl). + apply eqm_samerepr. + rewrite ! ofwords_add'. rewrite (Int.unsigned_add_carry xl yl). set (cc := Int.add_carry xl yl Int.zero). set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh); set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh). @@ -4264,8 +4264,8 @@ Proof. apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32. replace (Xh + Yh) with ((Xh + Yh + Int.unsigned cc) - Int.unsigned cc) by ring. apply Int.eqm_sub. 2: apply Int.eqm_refl. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. Qed. Lemma decompose_sub: @@ -4275,8 +4275,8 @@ Lemma decompose_sub: (Int.sub xl yl). Proof. intros. symmetry. rewrite ofwords_add. - apply eqm_samerepr. - rewrite ! ofwords_add'. rewrite (Int.unsigned_sub_borrow xl yl). + apply eqm_samerepr. + rewrite ! ofwords_add'. rewrite (Int.unsigned_sub_borrow xl yl). set (bb := Int.sub_borrow xl yl Int.zero). set (Xl := Int.unsigned xl); set (Xh := Int.unsigned xh); set (Yl := Int.unsigned yl); set (Yh := Int.unsigned yh). @@ -4290,8 +4290,8 @@ Proof. apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32. replace (Xh - Yh) with ((Xh - Yh - Int.unsigned bb) + Int.unsigned bb) by ring. apply Int.eqm_add. 2: apply Int.eqm_refl. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. 2: apply Int.eqm_refl. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. Qed. Lemma decompose_sub': @@ -4300,9 +4300,9 @@ Lemma decompose_sub': ofwords (Int.add (Int.add xh (Int.not yh)) (Int.add_carry xl (Int.not yl) Int.one)) (Int.sub xl yl). Proof. - intros. rewrite decompose_sub. f_equal. + intros. rewrite decompose_sub. f_equal. rewrite Int.sub_borrow_add_carry by auto. - rewrite Int.sub_add_not_3. rewrite Int.xor_assoc. rewrite Int.xor_idem. + rewrite Int.sub_add_not_3. rewrite Int.xor_assoc. rewrite Int.xor_idem. rewrite Int.xor_zero. auto. rewrite Int.xor_zero_l. unfold Int.add_carry. destruct (zlt (Int.unsigned xl + Int.unsigned (Int.not yl) + Int.unsigned Int.one) Int.modulus); @@ -4314,12 +4314,12 @@ Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y). Lemma mul'_mulhu: forall x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y). Proof. - intros. - rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul. + intros. + rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul. set (p := Int.unsigned x * Int.unsigned y). - set (ph := p / Int.modulus). set (pl := p mod Int.modulus). + set (ph := p / Int.modulus). set (pl := p mod Int.modulus). transitivity (repr (ph * Int.modulus + pl)). -- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. +- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. - apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints. rewrite Int.unsigned_repr_eq. apply eqm_refl. Qed. @@ -4330,7 +4330,7 @@ Lemma decompose_mul: ofwords (Int.add (Int.add (hiword (mul' xl yl)) (Int.mul xl yh)) (Int.mul xh yl)) (loword (mul' xl yl)). Proof. - intros. + intros. set (pl := loword (mul' xl yl)); set (ph := hiword (mul' xl yl)). assert (EQ0: unsigned (mul' xl yl) = Int.unsigned ph * two_p 32 + Int.unsigned pl). { rewrite <- (ofwords_recompose (mul' xl yl)). apply ofwords_add'. } @@ -4339,7 +4339,7 @@ Proof. set (YL := Int.unsigned yl); set (YH := Int.unsigned yh). set (PH := Int.unsigned ph) in *. set (PL := Int.unsigned pl) in *. transitivity (repr (((PH + XL * YH) + XH * YL) * two_p 32 + PL)). - apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. + apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. apply eqm_mul_2p32. rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. rewrite Int.add_unsigned. apply Int.eqm_unsigned_repr_l. apply Int.eqm_add. @@ -4349,14 +4349,14 @@ Proof. transitivity (repr (unsigned (mul' xl yl) + (XL * YH + XH * YL) * two_p 32)). rewrite EQ0. f_equal. ring. transitivity (repr ((XL * YL + (XL * YH + XH * YL) * two_p 32))). - apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. + apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. unfold mul'. apply eqm_unsigned_repr_l. apply eqm_refl. transitivity (repr (0 + (XL * YL + (XL * YH + XH * YL) * two_p 32))). - rewrite Zplus_0_l; auto. + rewrite Zplus_0_l; auto. transitivity (repr (XH * YH * (two_p 32 * two_p 32) + (XL * YL + (XL * YH + XH * YL) * two_p 32))). - apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. - change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring. - f_equal. ring. + apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl. + change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring. + f_equal. ring. Qed. Lemma decompose_mul_2: @@ -4365,7 +4365,7 @@ Lemma decompose_mul_2: ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl)) (Int.mul xl yl). Proof. - intros. rewrite decompose_mul. rewrite mul'_mulhu. + intros. rewrite decompose_mul. rewrite mul'_mulhu. rewrite hi_ofwords, lo_ofwords. auto. Qed. @@ -4375,11 +4375,11 @@ Lemma decompose_ltu: 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)). + rewrite e. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). apply zlt_true; omega. apply zlt_false; omega. - change (two_p 32) with Int.modulus. - generalize (Int.unsigned_range xl) (Int.unsigned_range yl). + 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. @@ -4392,9 +4392,9 @@ Lemma decompose_leu: if Int.eq xh yh then negb (Int.ltu yl xl) else Int.ltu xh yh. Proof. intros. rewrite decompose_ltu. rewrite Int.eq_sym. - unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). + unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). auto. - unfold Int.ltu. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). + unfold Int.ltu. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). rewrite zlt_false by omega; auto. rewrite zlt_true by omega; auto. Qed. @@ -4403,13 +4403,13 @@ Lemma decompose_lt: forall xh xl yh yl, lt (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.lt xh yh. Proof. - intros. unfold lt. rewrite ! ofwords_add''. rewrite Int.eq_signed. + 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)). + rewrite e. unfold Int.ltu. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). apply zlt_true; omega. apply zlt_false; omega. - change (two_p 32) with Int.modulus. - generalize (Int.unsigned_range xl) (Int.unsigned_range yl). + 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. @@ -4422,9 +4422,9 @@ Lemma decompose_le: if Int.eq xh yh then negb (Int.ltu yl xl) else Int.lt xh yh. Proof. intros. rewrite decompose_lt. rewrite Int.eq_sym. - rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)). + rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)). auto. - unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). + unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). rewrite zlt_false by omega; auto. rewrite zlt_true by omega; auto. Qed. |