From 43974a1651612a8dcfde280652346ee54abffd0a Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 21 Dec 2012 15:22:18 +0000 Subject: Integers: specialized function to compute x mod 2^N; used in "repr" to avoid the cost of a general Zmod. Memdata: updated accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2077 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Integers.v | 291 +++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 177 insertions(+), 114 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index 6630de3..7d5f016 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -90,6 +90,104 @@ Qed. Record int: Type := mkint { intval: Z; intrange: 0 <= intval < modulus }. +(** Binary decomposition of integers (type [Z]) *) + +Definition Z_bin_decomp (x: Z) : bool * Z := + match x with + | Z0 => (false, 0) + | Zpos p => + match p with + | xI q => (true, Zpos q) + | xO q => (false, Zpos q) + | xH => (true, 0) + end + | Zneg p => + match p with + | xI q => (true, Zneg q - 1) + | xO q => (false, Zneg q) + | xH => (true, -1) + end + end. + +Definition Z_bin_comp (b: bool) (x: Z) : Z := + if b then Zdouble_plus_one x else Zdouble x. + +Lemma Z_bin_comp_eq: + forall b x, Z_bin_comp b x = 2 * x + (if b then 1 else 0). +Proof. + unfold Z_bin_comp; intros. destruct b. + apply Zdouble_plus_one_mult. + rewrite Zdouble_mult. omega. +Qed. + +Lemma Z_bin_comp_decomp: + forall x, Z_bin_comp (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x. +Proof. + destruct x; simpl. + auto. + destruct p; auto. + destruct p; auto. simpl. + rewrite <- Pplus_one_succ_r. rewrite Pdouble_minus_one_o_succ_eq_xI. auto. +Qed. + +Lemma Z_bin_comp_decomp2: + forall x b y, Z_bin_decomp x = (b, y) -> x = Z_bin_comp b y. +Proof. + intros. rewrite <- (Z_bin_comp_decomp x). rewrite H; auto. +Qed. + +Lemma Z_bin_decomp_comp: + forall b x, Z_bin_decomp (Z_bin_comp b x) = (b, x). +Proof. + intros. destruct b; destruct x; simpl; auto. + destruct p; simpl; auto. + f_equal. f_equal. rewrite <- Pplus_one_succ_r. apply Psucc_o_double_minus_one_eq_xO. +Qed. + +Lemma Z_bin_comp_inj: + forall b1 b2 x1 x2, Z_bin_comp b1 x1 = Z_bin_comp b2 x2 -> (b1, x1) = (b2, x2). +Proof. + intros. repeat rewrite Z_bin_comp_eq in H. + destruct b1; destruct b2. + f_equal. omega. + omegaContradiction. + omegaContradiction. + f_equal. omega. +Qed. + +(** Fast normalization modulo [2^n]. *) + +Fixpoint Z_mod_two_p (x: Z) (n: nat) {struct n} : Z := + match n with + | O => 0 + | S m => let (b, y) := Z_bin_decomp x in Z_bin_comp b (Z_mod_two_p y m) + end. + +Lemma Z_mod_two_p_range: + forall n x, 0 <= Z_mod_two_p x n < two_power_nat n. +Proof. + induction n; simpl; intros. + rewrite two_power_nat_O. omega. + rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y]_eqn. + rewrite Z_bin_comp_eq. generalize (IHn y). destruct b; omega. +Qed. + +Lemma Z_mod_two_p_eq: + forall n x, Z_mod_two_p x n = Zmod x (two_power_nat n). +Proof. + assert (forall n x, exists y, x = y * two_power_nat n + Z_mod_two_p x n). + induction n; simpl; intros. + rewrite two_power_nat_O. exists x. ring. + rewrite two_power_nat_S. + destruct (Z_bin_decomp x) as [b y]_eqn. + destruct (IHn y) as [z EQ]. + exists z. rewrite (Z_bin_comp_decomp2 _ _ _ Heqp). + repeat rewrite Z_bin_comp_eq. rewrite EQ at 1. ring. + intros. + destruct (H n x) as [y EQ]. + symmetry. apply Zmod_unique with y. auto. apply Z_mod_two_p_range. +Qed. + (** The [unsigned] and [signed] functions return the Coq integer corresponding to the given machine integer, interpreted as unsigned or signed respectively. *) @@ -105,7 +203,7 @@ Definition signed (n: int) : Z := machine integer. The argument is treated modulo [modulus]. *) Definition repr (x: Z) : int := - mkint (Zmod x modulus) (Z_mod_lt x modulus modulus_pos). + mkint (Z_mod_two_p x wordsize) (Z_mod_two_p_range wordsize x). Definition zero := repr 0. Definition one := repr 1. @@ -179,26 +277,6 @@ Definition add_carry (x y cin: int): int := of the number. For [i] less than 0 or greater or equal to [wordsize], the characteristic function is [false]. *) -Definition Z_shift_add (b: bool) (x: Z) := - if b then 2 * x + 1 else 2 * x. - -Definition Z_bin_decomp (x: Z) : bool * Z := - match x with - | Z0 => (false, 0) - | Zpos p => - match p with - | xI q => (true, Zpos q) - | xO q => (false, Zpos q) - | xH => (true, 0) - end - | Zneg p => - match p with - | xI q => (true, Zneg q - 1) - | xO q => (false, Zneg q) - | xH => (true, -1) - end - end. - Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool := match n with | O => @@ -212,7 +290,7 @@ Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool := Fixpoint Z_of_bits (n: nat) (f: Z -> bool) (i: Z) {struct n}: Z := match n with | O => 0 - | S m => Z_shift_add (f i) (Z_of_bits m f (Zsucc i)) + | S m => Z_bin_comp (f i) (Z_of_bits m f (Zsucc i)) end. (** Bitwise logical "and", "or" and "xor" operations. *) @@ -392,6 +470,18 @@ Proof. generalize half_modulus_pos. omega. Qed. +Lemma unsigned_repr_eq: + forall x, unsigned (repr x) = Zmod x modulus. +Proof. + intros. simpl. apply Z_mod_two_p_eq. +Qed. + +Lemma signed_repr_eq: + forall x, signed (repr x) = if zlt (Zmod x modulus) half_modulus then Zmod x modulus else Zmod x modulus - modulus. +Proof. + intros. unfold signed. rewrite unsigned_repr_eq. auto. +Qed. + (** ** Modulo arithmetic *) (** We define and state properties of equality and arithmetic modulo a @@ -539,13 +629,13 @@ 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. - apply eqmod_mod_eq. auto with ints. exact H. + repeat rewrite Z_mod_two_p_eq. apply eqmod_mod_eq. auto with ints. exact H. Qed. Lemma eqm_unsigned_repr: forall z, eqm z (unsigned (repr z)). Proof. - unfold eqm, repr, unsigned; intros; simpl. apply eqmod_mod. auto with ints. + unfold eqm; intros. rewrite unsigned_repr_eq. apply eqmod_mod. auto with ints. Qed. Hint Resolve eqm_unsigned_repr: ints. @@ -568,7 +658,7 @@ Hint Resolve eqm_unsigned_repr_r: ints. Lemma eqm_signed_unsigned: forall x, eqm (signed x) (unsigned x). Proof. - intro; red; unfold signed. set (y := unsigned x). + intros; red. unfold signed. set (y := unsigned x). case (zlt y half_modulus); intro. apply eqmod_refl. red; exists (-1); ring. Qed. @@ -602,7 +692,8 @@ Qed. Theorem repr_unsigned: forall i, repr (unsigned i) = i. Proof. - destruct i; simpl. unfold repr. apply mkint_eq. apply Zmod_small; auto. + destruct i; simpl. unfold repr. apply mkint_eq. + rewrite Z_mod_two_p_eq. apply Zmod_small; auto. Qed. Hint Resolve repr_unsigned: ints. @@ -614,6 +705,8 @@ Proof. Qed. Hint Resolve repr_signed: ints. +Opaque repr. + Lemma eqm_repr_eq: forall x y, eqm x (unsigned y) -> repr x = y. Proof. intros. rewrite <- (repr_unsigned y). apply eqm_samerepr; auto. @@ -622,15 +715,15 @@ Qed. Theorem unsigned_repr: forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z. Proof. - intros. unfold repr, unsigned; simpl. - apply Zmod_small. unfold max_unsigned in H. fold modulus. omega. + intros. rewrite unsigned_repr_eq. + apply Zmod_small. unfold max_unsigned in H. omega. Qed. Hint Resolve unsigned_repr: ints. Theorem signed_repr: forall z, min_signed <= z <= max_signed -> signed (repr z) = z. Proof. - intros. unfold signed. case (zle 0 z); intro. + 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. @@ -665,12 +758,12 @@ Qed. Theorem unsigned_zero: unsigned zero = 0. Proof. - simpl. apply Zmod_0_l. + unfold zero; rewrite unsigned_repr_eq. apply Zmod_0_l. Qed. Theorem unsigned_one: unsigned one = 1. Proof. - simpl. apply Zmod_small. split. omega. + 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. @@ -679,7 +772,7 @@ Qed. Theorem unsigned_mone: unsigned mone = modulus - 1. Proof. - simpl unsigned. + 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. @@ -707,7 +800,7 @@ Qed. Theorem unsigned_repr_wordsize: unsigned iwordsize = Z_of_nat wordsize. Proof. - simpl. apply Zmod_small. + unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small. generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. Qed. @@ -795,7 +888,8 @@ Theorem unsigned_add_carry: unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) * modulus. Proof. intros. - unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r. simpl. + unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r. + rewrite unsigned_repr_eq. generalize (unsigned_range x) (unsigned_range y). intros. destruct (zlt (unsigned x + unsigned y) modulus). rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. @@ -1056,37 +1150,6 @@ Qed. (** ** Properties of binary decompositions *) -Lemma Z_shift_add_bin_decomp: - forall x, - Z_shift_add (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x. -Proof. - destruct x; simpl. - auto. - destruct p; reflexivity. - destruct p; try reflexivity. simpl. - assert (forall z, 2 * (z + 1) - 1 = 2 * z + 1). intro; omega. - generalize (H (Zpos p)); simpl. congruence. -Qed. - -Lemma Z_bin_decomp_shift_add: - forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x). -Proof. - intros. - intros. unfold Z_shift_add. destruct b; destruct x; simpl; auto. - destruct p; simpl; auto. f_equal. f_equal. - rewrite <- Pplus_one_succ_r. apply Psucc_o_double_minus_one_eq_xO. -Qed. - -Lemma Z_shift_add_inj: - forall b1 x1 b2 x2, - Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2. -Proof. - intros. - assert ((b1, x1) = (b2, x2)). - repeat rewrite <- Z_bin_decomp_shift_add. rewrite H; auto. - split; congruence. -Qed. - Lemma Z_of_bits_exten: forall f1 f2 n i1 i2, (forall i, 0 <= i < Z_of_nat n -> f1 (i + i1) = f2 (i + i2)) -> @@ -1108,13 +1171,13 @@ Proof. Z_of_bits n (bits_of_Z n x) 0 = k * two_power_nat n + x). induction n; intros; simpl. rewrite two_power_nat_O. exists (-x). omega. - rewrite two_power_nat_S. simpl bits_of_Z. caseEq (Z_bin_decomp x). intros b y ZBD. - rewrite zeq_true. destruct (IHn y) as [k EQ]. + rewrite two_power_nat_S. destruct (Z_bin_decomp x) as [b y]_eqn. + rewrite zeq_true. destruct (IHn y) as [k EQ]. replace (Z_of_bits n (fun i => if zeq i 0 then b else bits_of_Z n y (i - 1)) 1) with (Z_of_bits n (bits_of_Z n y) 0). rewrite EQ. exists k. - rewrite <- (Z_shift_add_bin_decomp x). rewrite ZBD. simpl fst; simpl snd. - unfold Z_shift_add; destruct b; ring. + rewrite (Z_bin_comp_decomp2 _ _ _ Heqp). + repeat rewrite Z_bin_comp_eq. ring. apply Z_of_bits_exten. intros. rewrite zeq_false. decEq. omega. omega. intro. exact (H wordsize x). @@ -1123,18 +1186,17 @@ Qed. Lemma bits_of_Z_zero: forall n x, bits_of_Z n 0 x = false. Proof. - induction n; simpl; intros. auto. case (zeq x 0); intro. auto. auto. + induction n; simpl; intros. auto. destruct (zeq x 0); auto. Qed. Remark Z_bin_decomp_2xm1: forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1). Proof. intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ. - generalize (Z_shift_add_bin_decomp (2 * x - 1)). - rewrite EQ; simpl fst; simpl snd. - replace (2 * x - 1) with (Z_shift_add true (x - 1)). - intro. elim (Z_shift_add_inj _ _ _ _ H); intros. - congruence. unfold Z_shift_add. omega. + apply Z_bin_comp_inj. + rewrite <- (Z_bin_comp_decomp2 _ _ _ EQ). + rewrite Z_bin_comp_eq. + omega. Qed. Lemma bits_of_Z_two_p: @@ -1171,7 +1233,7 @@ Proof. rewrite two_power_nat_O. omega. rewrite two_power_nat_S. generalize (IHn (Zsucc i)). - intro. destruct (f i); unfold Z_shift_add; omega. + intro. rewrite Z_bin_comp_eq. destruct (f i); omega. Qed. Lemma Z_of_bits_range_1: @@ -1196,7 +1258,7 @@ Lemma bits_of_Z_of_bits_gen: Proof. induction n; intros; simpl. simpl in H. omegaContradiction. - rewrite Z_bin_decomp_shift_add. + rewrite Z_bin_decomp_comp. destruct (zeq i 0). f_equal. omega. rewrite IHn. f_equal. omega. @@ -1243,10 +1305,10 @@ Proof. destruct (Z_bin_decomp x) as [b x1]_eqn. destruct (zeq i 0). subst i. simpl in H. assert (x = 0) by omega. subst x. simpl in Heqp. congruence. - apply IHn. - rewrite <- (Z_shift_add_bin_decomp x) in H. rewrite Heqp in H. simpl in H. + apply IHn. + rewrite (Z_bin_comp_decomp2 _ _ _ Heqp) in H. replace i with (Zsucc (i-1)) in H by omega. rewrite two_p_S in H. - unfold Z_shift_add in H. destruct b; omega. + rewrite Z_bin_comp_eq in H. destruct b; omega. omega. Qed. @@ -1274,7 +1336,7 @@ Proof. intros. simpl. rewrite inj_S in H. rewrite inj_S in H0. rewrite <- (IHn f g h (Zsucc j)). assert (j <= j < j + Zsucc(Z_of_nat n)). omega. - unfold Z_shift_add. + repeat rewrite Z_bin_comp_eq. rewrite <- H0; auto. caseEq (f j); intros; caseEq (g j); intros; simpl orb. generalize (H j H1). rewrite H2; rewrite H3. simpl andb; congruence. @@ -1293,7 +1355,7 @@ Proof. simpl. repeat rewrite Zplus_0_r. rewrite two_power_nat_O. omega. rewrite inj_S. rewrite two_power_nat_S. simpl Z_of_bits. rewrite IHm. replace (i + Zsucc (Z_of_nat m)) with (Zsucc i + Z_of_nat m) by omega. - unfold Z_shift_add. destruct (f i); ring. + repeat rewrite Z_bin_comp_eq. ring. Qed. Lemma Z_of_bits_truncate: @@ -1320,10 +1382,8 @@ Lemma Z_of_bits_complement: Proof. induction n; intros; simpl Z_of_bits. auto. - rewrite two_power_nat_S. rewrite IHn. -Opaque Zmult Zplus Zminus. - destruct (f i); simpl. ring. ring. -Transparent Zmult Zplus Zminus. + rewrite two_power_nat_S. rewrite IHn. repeat rewrite Z_bin_comp_eq. + destruct (f i); simpl negb; ring. Qed. Lemma Z_of_bits_true: @@ -2124,8 +2184,8 @@ Lemma Z_bin_decomp_range: forall x n, 0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n. Proof. - intros. rewrite <- (Z_shift_add_bin_decomp x) in H. - unfold Z_shift_add in H. destruct (fst (Z_bin_decomp x)); omega. + intros. rewrite <- (Z_bin_comp_decomp x) in H. rewrite Z_bin_comp_eq in H. + destruct (fst (Z_bin_decomp x)); omega. Qed. Lemma Z_one_bits_powerserie: @@ -2139,16 +2199,16 @@ Proof. simpl. rewrite two_power_nat_O in H0. assert (x = 0). omega. subst x. omega. rewrite two_power_nat_S in H0. simpl Z_one_bits. - generalize (Z_shift_add_bin_decomp x). - generalize (Z_bin_decomp_range x _ H0). - case (Z_bin_decomp x). simpl. intros b y RANGE SHADD. - subst x. unfold Z_shift_add. - destruct b. simpl powerserie. rewrite <- IHn. - rewrite two_p_is_exp. change (two_p 1) with 2. ring. - auto. omega. omega. auto. - rewrite <- IHn. - rewrite two_p_is_exp. change (two_p 1) with 2. ring. - auto. omega. omega. auto. + destruct (Z_bin_decomp x) as [b y]_eqn. + rewrite (Z_bin_comp_decomp2 _ _ _ Heqp). + assert (EQ: y * two_p (i + 1) = powerserie (Z_one_bits n y (i + 1))). + apply IHn. omega. + replace y with (snd (Z_bin_decomp x)). apply Z_bin_decomp_range; auto. + rewrite Heqp; auto. + rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ. + rewrite Z_bin_comp_eq. + destruct b; simpl powerserie; rewrite <- EQ; ring. + omega. omega. intros. rewrite <- H. change (two_p 0) with 1. omega. omega. exact H0. Qed. @@ -2239,11 +2299,12 @@ Proof. rewrite inj_S in H. assert (x = 0 \/ 0 < x) by omega. destruct H0. subst x; simpl. decEq. omega. apply Z_one_bits_zero. - replace (two_p x) with (Z_shift_add false (two_p (x-1))). - rewrite Z_bin_decomp_shift_add. + replace (two_p x) with (Z_bin_comp false (two_p (x-1))). + rewrite Z_bin_decomp_comp. replace (i + x) with ((i + 1) + (x - 1)) by omega. apply IHn. omega. - unfold Z_shift_add. rewrite <- two_p_S. decEq; omega. omega. + rewrite Z_bin_comp_eq. rewrite <- two_p_S. + rewrite Zplus_0_r. decEq; omega. omega. Qed. Lemma is_power2_two_p: @@ -2415,19 +2476,19 @@ Lemma sign_bit_of_Z_rec: Proof. induction n; intros. rewrite two_power_nat_S in H. rewrite two_power_nat_O in *. simpl. - caseEq (Z_bin_decomp x); intros b x1 ZBD. rewrite zeq_true. - generalize (Z_shift_add_bin_decomp x). rewrite ZBD; simpl. intros. subst x. - unfold Z_shift_add in *. - destruct b. rewrite zlt_false. auto. omega. rewrite zlt_true. auto. omega. - rewrite inj_S. remember (S n) as sn. simpl. rewrite two_power_nat_S in H. - generalize (Z_shift_add_bin_decomp x). destruct (Z_bin_decomp x) as [b x1]. - simpl. intros. rewrite zeq_false. + generalize (Z_bin_comp_decomp x). destruct (Z_bin_decomp x) as [b y]; simpl. + intros; subst x. rewrite Z_bin_comp_eq in *. + destruct b. rewrite zlt_false. auto. omega. rewrite zlt_true. auto. omega. + rewrite inj_S. remember (S n) as sn. simpl. rewrite two_power_nat_S in H. + generalize (Z_bin_comp_decomp x). destruct (Z_bin_decomp x) as [b y]; simpl. + intros; subst x. rewrite Z_bin_comp_eq in *. + rewrite zeq_false. replace (Zsucc (Z_of_nat n) - 1) with (Z_of_nat n). rewrite IHn. - rewrite <- H0. subst sn. rewrite two_power_nat_S. - destruct (zlt x1 (two_power_nat n)). - rewrite zlt_true. auto. unfold Z_shift_add; destruct b; omega. - rewrite zlt_false. auto. unfold Z_shift_add; destruct b; omega. - subst x. unfold Z_shift_add in H. destruct b; omega. + subst sn. rewrite two_power_nat_S. + destruct (zlt y (two_power_nat n)). + rewrite zlt_true. auto. destruct b; omega. + rewrite zlt_false. auto. destruct b; omega. + destruct b; omega. omega. omega. Qed. @@ -2661,7 +2722,9 @@ Proof. rewrite H8. rewrite Zdiv_shift; auto. unfold add. apply eqm_samerepr. apply eqm_add. apply eqm_unsigned_repr. - destruct (zeq (sx mod two_p uy) 0); simpl; apply eqmod_mod; apply modulus_pos. + 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. -- cgit v1.2.3