Library Coq.ZArith.Zbinary
Bit vectors interpreted as integers.
Contribution by Jean Duprat (ENS Lyon).
L'évaluation des vecteurs de booléens se font à la fois en binaire et
en complément à deux. Le nombre appartient à Z.
On utilise donc Omega pour faire les calculs dans Z.
De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
two_power_nat = n:nat(POS (shift_nat n xH))
: nat->Z
two_power_nat_S
: (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)`
Z_lt_ge_dec
: (x,y:Z){`x < y`}+{`x >= y`}
Les calculs sont effectués dans la convention positive usuelle.
Les valeurs correspondent soit à l'écriture binaire (nat),
soit au complément à deux (int).
On effectue le calcul suivant le schéma de Horner.
Le complément à deux n'a de sens que sur les vecteurs de taille
supérieure ou égale à un, le bit de signe étant évalué négativement.
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.
On calcule la valeur binaire selon un schema de Horner.
Le calcul s'arrete à la longueur du vecteur sans vérification.
On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient
de la division z=2q+r avec 0<=r<=1.
La valeur en complément à deux est calculée selon un schema de Horner
avec Zmod2, le paramètre est la taille moins un.
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.
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.
Bibliotheque de lemmes utiles dans la section suivante.
Utilise largement ZArith.
Mériterait d'être récrite.
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.
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 (Zeven.Zodd_bool z) n (Z_to_binary n (Zeven.Zdiv2 z)).
Lemma Z_div2_value :
forall z:Z,
(z >= 0)%Z -> (bit_value (Zeven.Zodd_bool z) + 2 * Zeven.Zdiv2 z)%Z = z.
Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Zeven.Zdiv2 z >= 0)%Z.
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.
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)).
Lemma Zeven_bit_value :
forall z:Z, Zeven.Zeven z -> bit_value (Zeven.Zodd_bool z) = 0%Z.
Lemma Zodd_bit_value :
forall z:Z, Zeven.Zodd z -> bit_value (Zeven.Zodd_bool 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.
On vérifie que dans l'intervalle de définition les fonctions sont
réciproques l'une de l'autre. Elles utilisent les lemmes du bric-a-brac.
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.