diff options
| -rw-r--r-- | theories/Bool/Bvector.v | 7 | ||||
| -rw-r--r-- | theories/ZArith/Zbinary.v | 30 |
2 files changed, 20 insertions, 17 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 86b59db26..aa69fccf1 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -196,6 +196,9 @@ Defined. End VECTORS. +Implicit Arguments Vnil [A]. +Implicit Arguments Vcons [A n]. + Section BOOLEAN_VECTORS. (* @@ -212,9 +215,9 @@ ATTENTION : Tous les décalages prennent la taille moins un comme paramètre Definition Bvector := vector bool. -Definition Bnil := Vnil bool. +Definition Bnil := @Vnil bool. -Definition Bcons := Vcons bool. +Definition Bcons := @Vcons bool. Definition Bvect_true := Vconst bool true. diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v index cd8872dac..c78e0a72f 100644 --- a/theories/ZArith/Zbinary.v +++ b/theories/ZArith/Zbinary.v @@ -17,10 +17,10 @@ Require Export Zpower. Require Import Omega. (* -L'évaluation des vecteurs de booléens se font à la fois en binaire et -en complément à deux. Le nombre appartient à Z. +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. +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 @@ -33,12 +33,12 @@ De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur. Section VALUE_OF_BOOLEAN_VECTORS. (* -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. +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 := @@ -84,11 +84,11 @@ Section ENCODING_VALUE. (* On calcule la valeur binaire selon un schema de Horner. -Le calcul s'arrete à la longueur du vecteur sans vérification. +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. +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) := @@ -186,7 +186,7 @@ Meriterait d'etre reecrite. Lemma binary_value_Sn : forall (n:nat) (b:bool) (bv:Bvector n), - binary_value (S n) (Vcons bool b n bv) = + binary_value (S n) (Vcons b bv) = (bit_value b + 2 * binary_value n bv)%Z. Proof. intros; auto. @@ -355,8 +355,8 @@ 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. +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. *) |