summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zdigits.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zdigits.v')
-rw-r--r--theories/ZArith/Zdigits.v347
1 files changed, 347 insertions, 0 deletions
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
new file mode 100644
index 00000000..0a6c9498
--- /dev/null
+++ b/theories/ZArith/Zdigits.v
@@ -0,0 +1,347 @@
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** Bit vectors interpreted as integers.
+ Contribution by Jean Duprat (ENS Lyon). *)
+
+Require Import Bvector.
+Require Import ZArith.
+Require Export Zpower.
+Require Import Omega.
+
+(** The evaluation of boolean vector is done both in binary and
+ two's complement. The computed number belongs to Z.
+ We hence use Omega to perform computations in Z.
+ Moreover, we use functions [2^n] where [n] is a natural number
+ (here the vector length).
+*)
+
+
+Section VALUE_OF_BOOLEAN_VECTORS.
+
+(** Computations are done in the usual convention.
+ The values correspond either to the binary coding (nat) or
+ to the two's complement coding (int).
+ We perform the computation via Horner scheme.
+ The two's complement coding only makes sense on vectors whose
+ size is greater or equal to one (a sign bit should be present).
+*)
+
+ Definition bit_value (b:bool) : Z :=
+ match b with
+ | true => 1%Z
+ | false => 0%Z
+ end.
+
+ Lemma binary_value : forall n:nat, Bvector n -> Z.
+ Proof.
+ simple induction n; intros.
+ exact 0%Z.
+
+ inversion H0.
+ exact (bit_value a + 2 * H H2)%Z.
+ Defined.
+
+ Lemma two_compl_value : forall n:nat, Bvector (S n) -> Z.
+ Proof.
+ simple induction n; intros.
+ inversion H.
+ exact (- bit_value a)%Z.
+
+ inversion H0.
+ exact (bit_value a + 2 * H H2)%Z.
+ Defined.
+
+End VALUE_OF_BOOLEAN_VECTORS.
+
+Section ENCODING_VALUE.
+
+(** We compute the binary value via a Horner scheme.
+ Computation stops at the vector length without checks.
+ We define a function Zmod2 similar to Zdiv2 returning the
+ quotient of division z=2q+r with 0<=r<=1.
+ The two's complement value is also computed via a Horner scheme
+ with Zmod2, the parameter is the size minus one.
+*)
+
+ Definition Zmod2 (z:Z) :=
+ match z with
+ | Z0 => 0%Z
+ | Zpos p => match p with
+ | xI q => Zpos q
+ | xO q => Zpos q
+ | xH => 0%Z
+ end
+ | Zneg p =>
+ match p with
+ | xI q => (Zneg q - 1)%Z
+ | xO q => Zneg q
+ | xH => (-1)%Z
+ end
+ end.
+
+
+ Lemma Zmod2_twice :
+ forall z:Z, z = (2 * Zmod2 z + bit_value (Zeven.Zodd_bool z))%Z.
+ Proof.
+ destruct z; simpl in |- *.
+ trivial.
+
+ destruct p; simpl in |- *; trivial.
+
+ destruct p; simpl in |- *.
+ destruct p as [p| p| ]; simpl in |- *.
+ rewrite <- (Pdouble_minus_one_o_succ_eq_xI p); trivial.
+
+ trivial.
+
+ trivial.
+
+ trivial.
+
+ trivial.
+ Qed.
+
+ Lemma Z_to_binary : forall n:nat, Z -> Bvector n.
+ Proof.
+ simple induction n; intros.
+ exact Bnil.
+
+ exact (Bcons (Zeven.Zodd_bool H0) n0 (H (Zeven.Zdiv2 H0))).
+ Defined.
+
+ Lemma Z_to_two_compl : forall n:nat, Z -> Bvector (S n).
+ Proof.
+ simple induction n; intros.
+ exact (Bcons (Zeven.Zodd_bool H) 0 Bnil).
+
+ exact (Bcons (Zeven.Zodd_bool H0) (S n0) (H (Zmod2 H0))).
+ Defined.
+
+End ENCODING_VALUE.
+
+Section Z_BRIC_A_BRAC.
+
+ (** Some auxiliary lemmas used in the next section. Large use of ZArith.
+ Deserve to be properly rewritten.
+ *)
+
+ Lemma binary_value_Sn :
+ forall (n:nat) (b:bool) (bv:Bvector n),
+ binary_value (S n) (Vcons bool b n bv) =
+ (bit_value b + 2 * binary_value n bv)%Z.
+ Proof.
+ intros; auto.
+ Qed.
+
+ Lemma Z_to_binary_Sn :
+ forall (n:nat) (b:bool) (z:Z),
+ (z >= 0)%Z ->
+ Z_to_binary (S n) (bit_value b + 2 * z) = Bcons b n (Z_to_binary n z).
+ Proof.
+ destruct b; destruct z; simpl in |- *; auto.
+ intro H; elim H; trivial.
+ Qed.
+
+ Lemma binary_value_pos :
+ forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z.
+ Proof.
+ induction bv as [| a n v IHbv]; simpl in |- *.
+ omega.
+
+ destruct a; destruct (binary_value n v); simpl in |- *; auto.
+ auto with zarith.
+ Qed.
+
+ Lemma two_compl_value_Sn :
+ forall (n:nat) (bv:Bvector (S n)) (b:bool),
+ two_compl_value (S n) (Bcons b (S n) bv) =
+ (bit_value b + 2 * two_compl_value n bv)%Z.
+ Proof.
+ intros; auto.
+ Qed.
+
+ Lemma Z_to_two_compl_Sn :
+ forall (n:nat) (b:bool) (z:Z),
+ Z_to_two_compl (S n) (bit_value b + 2 * z) =
+ Bcons b (S n) (Z_to_two_compl n z).
+ Proof.
+ destruct b; destruct z as [| p| p]; auto.
+ destruct p as [p| p| ]; auto.
+ destruct p as [p| p| ]; simpl in |- *; auto.
+ intros; rewrite (Psucc_o_double_minus_one_eq_xO p); trivial.
+ Qed.
+
+ Lemma Z_to_binary_Sn_z :
+ forall (n:nat) (z:Z),
+ Z_to_binary (S n) z =
+ Bcons (Zeven.Zodd_bool z) n (Z_to_binary n (Zeven.Zdiv2 z)).
+ Proof.
+ intros; auto.
+ Qed.
+
+ Lemma Z_div2_value :
+ forall z:Z,
+ (z >= 0)%Z -> (bit_value (Zeven.Zodd_bool z) + 2 * Zeven.Zdiv2 z)%Z = z.
+ Proof.
+ destruct z as [| p| p]; auto.
+ destruct p; auto.
+ intro H; elim H; trivial.
+ Qed.
+
+ Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Zeven.Zdiv2 z >= 0)%Z.
+ Proof.
+ destruct z as [| p| p].
+ auto.
+
+ destruct p; auto.
+ simpl in |- *; intros; omega.
+
+ intro H; elim H; trivial.
+ Qed.
+
+ Lemma Zdiv2_two_power_nat :
+ forall (z:Z) (n:nat),
+ (z >= 0)%Z ->
+ (z < two_power_nat (S n))%Z -> (Zeven.Zdiv2 z < two_power_nat n)%Z.
+ Proof.
+ intros.
+ cut (2 * Zeven.Zdiv2 z < 2 * two_power_nat n)%Z; intros.
+ omega.
+
+ rewrite <- two_power_nat_S.
+ destruct (Zeven.Zeven_odd_dec z); intros.
+ rewrite <- Zeven.Zeven_div2; auto.
+
+ generalize (Zeven.Zodd_div2 z H z0); omega.
+ Qed.
+
+ Lemma Z_to_two_compl_Sn_z :
+ forall (n:nat) (z:Z),
+ Z_to_two_compl (S n) z =
+ Bcons (Zeven.Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z)).
+ Proof.
+ intros; auto.
+ Qed.
+
+ Lemma Zeven_bit_value :
+ forall z:Z, Zeven.Zeven z -> bit_value (Zeven.Zodd_bool z) = 0%Z.
+ Proof.
+ destruct z; unfold bit_value in |- *; auto.
+ destruct p; tauto || (intro H; elim H).
+ destruct p; tauto || (intro H; elim H).
+ Qed.
+
+ Lemma Zodd_bit_value :
+ forall z:Z, Zeven.Zodd z -> bit_value (Zeven.Zodd_bool z) = 1%Z.
+ Proof.
+ destruct z; unfold bit_value in |- *; auto.
+ intros; elim H.
+ destruct p; tauto || (intros; elim H).
+ destruct p; tauto || (intros; elim H).
+ Qed.
+
+ Lemma Zge_minus_two_power_nat_S :
+ forall (n:nat) (z:Z),
+ (z >= - two_power_nat (S n))%Z -> (Zmod2 z >= - two_power_nat n)%Z.
+ Proof.
+ intros n z; rewrite (two_power_nat_S n).
+ generalize (Zmod2_twice z).
+ destruct (Zeven.Zeven_odd_dec z) as [H| H].
+ rewrite (Zeven_bit_value z H); intros; omega.
+
+ rewrite (Zodd_bit_value z H); intros; omega.
+ Qed.
+
+ Lemma Zlt_two_power_nat_S :
+ forall (n:nat) (z:Z),
+ (z < two_power_nat (S n))%Z -> (Zmod2 z < two_power_nat n)%Z.
+ Proof.
+ intros n z; rewrite (two_power_nat_S n).
+ generalize (Zmod2_twice z).
+ destruct (Zeven.Zeven_odd_dec z) as [H| H].
+ rewrite (Zeven_bit_value z H); intros; omega.
+
+ rewrite (Zodd_bit_value z H); intros; omega.
+ Qed.
+
+End Z_BRIC_A_BRAC.
+
+Section COHERENT_VALUE.
+
+(** We check that the functions are reciprocal on the definition interval.
+ This uses earlier library lemmas.
+*)
+
+ Lemma binary_to_Z_to_binary :
+ forall (n:nat) (bv:Bvector n), Z_to_binary n (binary_value n bv) = bv.
+ Proof.
+ induction bv as [| a n bv IHbv].
+ auto.
+
+ rewrite binary_value_Sn.
+ rewrite Z_to_binary_Sn.
+ rewrite IHbv; trivial.
+
+ apply binary_value_pos.
+ Qed.
+
+ Lemma two_compl_to_Z_to_two_compl :
+ forall (n:nat) (bv:Bvector n) (b:bool),
+ Z_to_two_compl n (two_compl_value n (Bcons b n bv)) = Bcons b n bv.
+ Proof.
+ induction bv as [| a n bv IHbv]; intro b.
+ destruct b; auto.
+
+ rewrite two_compl_value_Sn.
+ rewrite Z_to_two_compl_Sn.
+ rewrite IHbv; trivial.
+ Qed.
+
+ Lemma Z_to_binary_to_Z :
+ forall (n:nat) (z:Z),
+ (z >= 0)%Z ->
+ (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z.
+ Proof.
+ induction n as [| n IHn].
+ unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros; omega.
+
+ intros; rewrite Z_to_binary_Sn_z.
+ rewrite binary_value_Sn.
+ rewrite IHn.
+ apply Z_div2_value; auto.
+
+ apply Pdiv2; trivial.
+
+ apply Zdiv2_two_power_nat; trivial.
+ Qed.
+
+ Lemma Z_to_two_compl_to_Z :
+ forall (n:nat) (z:Z),
+ (z >= - two_power_nat n)%Z ->
+ (z < two_power_nat n)%Z -> two_compl_value n (Z_to_two_compl n z) = z.
+ Proof.
+ induction n as [| n IHn].
+ unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros.
+ assert (z = (-1)%Z \/ z = 0%Z). omega.
+ intuition; subst z; trivial.
+
+ intros; rewrite Z_to_two_compl_Sn_z.
+ rewrite two_compl_value_Sn.
+ rewrite IHn.
+ generalize (Zmod2_twice z); omega.
+
+ apply Zge_minus_two_power_nat_S; auto.
+
+ apply Zlt_two_power_nat_S; auto.
+ Qed.
+
+End COHERENT_VALUE.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:42:29 +0000