Library Coq.ZArith.Zdigits
Bit vectors interpreted as integers.
Contribution by Jean Duprat (ENS Lyon).
Require Import Bvector.
Require Import ZArith.
Require Export Zpower.
Require Import Lia.
The evaluation of boolean vector is done both in binary and
two's complement. The computed number belongs to Z.
We hence use lia 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.
Lemma two_compl_value : forall n:nat, Bvector (S n) -> Z.
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 Z.div2 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 (Z.odd z))%Z.
Lemma Z_to_binary : forall n:nat, Z -> Bvector n.
Lemma Z_to_two_compl : forall n:nat, Z -> Bvector (S n).
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) ( b :: bv) =
(bit_value b + 2 * binary_value n bv)%Z.
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).
Lemma binary_value_pos :
forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z.
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.
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).
Lemma Z_to_binary_Sn_z :
forall (n:nat) (z:Z),
Z_to_binary (S n) z =
Bcons (Z.odd z) n (Z_to_binary n (Z.div2 z)).
Lemma Z_div2_value :
forall z:Z,
(z >= 0)%Z -> (bit_value (Z.odd z) + 2 * Z.div2 z)%Z = z.
Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Z.div2 z >= 0)%Z.
Lemma Zdiv2_two_power_nat :
forall (z:Z) (n:nat),
(z >= 0)%Z ->
(z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z.
Lemma Z_to_two_compl_Sn_z :
forall (n:nat) (z:Z),
Z_to_two_compl (S n) z =
Bcons (Z.odd z) (S n) (Z_to_two_compl n (Zmod2 z)).
Lemma Zeven_bit_value :
forall z:Z, Zeven.Zeven z -> bit_value (Z.odd z) = 0%Z.
Lemma Zodd_bit_value :
forall z:Z, Zeven.Zodd z -> bit_value (Z.odd z) = 1%Z.
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.
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.
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.
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.
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.
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.
End COHERENT_VALUE.