diff options
Diffstat (limited to 'theories7/ZArith/Zbinary.v')
| -rw-r--r-- | theories7/ZArith/Zbinary.v | 425 |
1 files changed, 425 insertions, 0 deletions
diff --git a/theories7/ZArith/Zbinary.v b/theories7/ZArith/Zbinary.v new file mode 100644 index 00000000..c3efbe1e --- /dev/null +++ b/theories7/ZArith/Zbinary.v @@ -0,0 +1,425 @@ +(************************************************************************) +(* 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: Zbinary.v,v 1.1.2.1 2004/07/16 19:31:42 herbelin Exp $ i*) + +(** Bit vectors interpreted as integers. + Contribution by Jean Duprat (ENS Lyon). *) + +Require Bvector. +Require ZArith. +Require Export Zpower. +Require Omega. + +(* +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`} +*) + + +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. +*) + +Definition bit_value [b:bool] : Z := +Cases b of + | true => `1` + | false => `0` +end. + +Lemma binary_value : (n:nat) (Bvector n) -> Z. +Proof. + Induction n; Intros. + Exact `0`. + + Inversion H0. + Exact (Zplus (bit_value a) (Zmult `2` (H H2))). +Defined. + +Lemma two_compl_value : (n:nat) (Bvector (S n)) -> Z. +Proof. + Induction n; Intros. + Inversion H. + Exact (Zopp (bit_value a)). + + Inversion H0. + Exact (Zplus (bit_value a) (Zmult `2` (H H2))). +Defined. + +(* +Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))). + = `5` + : Z +*) + +(* +Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))). + = `-3` + : 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] Cases z of + | ZERO => `0` + | ((POS p)) => Cases p of + | (xI q) => (POS q) + | (xO q) => (POS q) + | xH => `0` + end + | ((NEG p)) => Cases p of + | (xI q) => `(NEG q) - 1` + | (xO q) => (NEG q) + | xH => `-1` + end + end. + +V7only [ +Notation double_moins_un_add_un := + [p](sym_eq ? ? ? (double_moins_un_add_un_xI p)). +]. + +Lemma Zmod2_twice : (z:Z) + `z = (2*(Zmod2 z) + (bit_value (Zodd_bool z)))`. +Proof. + NewDestruct z; Simpl. + Trivial. + + NewDestruct p; Simpl; Trivial. + + NewDestruct p; Simpl. + NewDestruct p as [p|p|]; Simpl. + Rewrite <- (double_moins_un_add_un_xI p); Trivial. + + Trivial. + + Trivial. + + Trivial. + + Trivial. +Save. + +Lemma Z_to_binary : (n:nat) Z -> (Bvector n). +Proof. + Induction n; Intros. + Exact Bnil. + + Exact (Bcons (Zodd_bool H0) n0 (H (Zdiv2 H0))). +Defined. + +(* +Eval Compute in (Z_to_binary (5) `5`). + = (Vcons bool true (4) + (Vcons bool false (3) + (Vcons bool true (2) + (Vcons bool false (1) (Vcons bool false (0) (Vnil bool)))))) + : (Bvector (5)) +*) + +Lemma Z_to_two_compl : (n:nat) Z -> (Bvector (S n)). +Proof. + Induction n; Intros. + Exact (Bcons (Zodd_bool H) (0) Bnil). + + Exact (Bcons (Zodd_bool H0) (S n0) (H (Zmod2 H0))). +Defined. + +(* +Eval Compute in (Z_to_two_compl (3) `0`). + = (Vcons bool false (3) + (Vcons bool false (2) + (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))) + : (vector bool (4)) + +Eval Compute in (Z_to_two_compl (3) `5`). + = (Vcons bool true (3) + (Vcons bool false (2) + (Vcons bool true (1) (Vcons bool false (0) (Vnil bool))))) + : (vector bool (4)) + +Eval Compute in (Z_to_two_compl (3) `-5`). + = (Vcons bool true (3) + (Vcons bool true (2) + (Vcons bool false (1) (Vcons bool true (0) (Vnil bool))))) + : (vector bool (4)) +*) + +End ENCODING_VALUE. + +Section Z_BRIC_A_BRAC. + +(* +Bibliotheque de lemmes utiles dans la section suivante. +Utilise largement ZArith. +Meriterait d'etre reecrite. +*) + +Lemma binary_value_Sn : (n:nat) (b:bool) (bv : (Bvector n)) + (binary_value (S n) (Vcons bool b n bv))=`(bit_value b) + 2*(binary_value n bv)`. +Proof. + Intros; Auto. +Save. + +Lemma Z_to_binary_Sn : (n:nat) (b:bool) (z:Z) + `z>=0`-> + (Z_to_binary (S n) `(bit_value b) + 2*z`)=(Bcons b n (Z_to_binary n z)). +Proof. + NewDestruct b; NewDestruct z; Simpl; Auto. + Intro H; Elim H; Trivial. +Save. + +Lemma binary_value_pos : (n:nat) (bv:(Bvector n)) + `(binary_value n bv) >= 0`. +Proof. + NewInduction bv as [|a n v IHbv]; Simpl. + Omega. + + NewDestruct a; NewDestruct (binary_value n v); Simpl; Auto. + Auto with zarith. +Save. + +V7only [Notation add_un_double_moins_un_xO := is_double_moins_un.]. + +Lemma two_compl_value_Sn : (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)`. +Proof. + Intros; Auto. +Save. + +Lemma Z_to_two_compl_Sn : (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. + NewDestruct b; NewDestruct z as [|p|p]; Auto. + NewDestruct p as [p|p|]; Auto. + NewDestruct p as [p|p|]; Simpl; Auto. + Intros; Rewrite (add_un_double_moins_un_xO p); Trivial. +Save. + +Lemma Z_to_binary_Sn_z : (n:nat) (z:Z) + (Z_to_binary (S n) z)=(Bcons (Zodd_bool z) n (Z_to_binary n (Zdiv2 z))). +Proof. + Intros; Auto. +Save. + +Lemma Z_div2_value : (z:Z) + ` z>=0 `-> + `(bit_value (Zodd_bool z))+2*(Zdiv2 z) = z`. +Proof. + NewDestruct z as [|p|p]; Auto. + NewDestruct p; Auto. + Intro H; Elim H; Trivial. +Save. + +Lemma Zdiv2_pos : (z:Z) + ` z >= 0 ` -> + `(Zdiv2 z) >= 0 `. +Proof. + NewDestruct z as [|p|p]. + Auto. + + NewDestruct p; Auto. + Simpl; Intros; Omega. + + Intro H; Elim H; Trivial. + +Save. + +Lemma Zdiv2_two_power_nat : (z:Z) (n:nat) + ` z >= 0 ` -> + ` z < (two_power_nat (S n)) ` -> + `(Zdiv2 z) < (two_power_nat n) `. +Proof. + Intros. + Cut (Zlt (Zmult `2` (Zdiv2 z)) (Zmult `2` (two_power_nat n))); Intros. + Omega. + + Rewrite <- two_power_nat_S. + NewDestruct (Zeven_odd_dec z); Intros. + Rewrite <- Zeven_div2; Auto. + + Generalize (Zodd_div2 z H z0); Omega. +Save. + +(* + +Lemma Z_minus_one_or_zero : (z:Z) + `z >= -1` -> + `z < 1` -> + {`z=-1`} + {`z=0`}. +Proof. + NewDestruct z; Auto. + NewDestruct p; Auto. + Tauto. + + Tauto. + + Intros. + Right; Omega. + + NewDestruct p. + Tauto. + + Tauto. + + Intros; Left; Omega. +Save. +*) + +Lemma Z_to_two_compl_Sn_z : (n:nat) (z:Z) + (Z_to_two_compl (S n) z)=(Bcons (Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z))). +Proof. + Intros; Auto. +Save. + +Lemma Zeven_bit_value : (z:Z) + (Zeven z) -> + `(bit_value (Zodd_bool z))=0`. +Proof. + NewDestruct z; Unfold bit_value; Auto. + NewDestruct p; Tauto Orelse (Intro H; Elim H). + NewDestruct p; Tauto Orelse (Intro H; Elim H). +Save. + +Lemma Zodd_bit_value : (z:Z) + (Zodd z) -> + `(bit_value (Zodd_bool z))=1`. +Proof. + NewDestruct z; Unfold bit_value; Auto. + Intros; Elim H. + NewDestruct p; Tauto Orelse (Intros; Elim H). + NewDestruct p; Tauto Orelse (Intros; Elim H). +Save. + +Lemma Zge_minus_two_power_nat_S : (n:nat) (z:Z) + `z >= (-(two_power_nat (S n)))`-> + `(Zmod2 z) >= (-(two_power_nat n))`. +Proof. + Intros n z; Rewrite (two_power_nat_S n). + Generalize (Zmod2_twice z). + NewDestruct (Zeven_odd_dec z) as [H|H]. + Rewrite (Zeven_bit_value z H); Intros; Omega. + + Rewrite (Zodd_bit_value z H); Intros; Omega. +Save. + +Lemma Zlt_two_power_nat_S : (n:nat) (z:Z) + `z < (two_power_nat (S n))`-> + `(Zmod2 z) < (two_power_nat n)`. +Proof. + Intros n z; Rewrite (two_power_nat_S n). + Generalize (Zmod2_twice z). + NewDestruct (Zeven_odd_dec z) as [H|H]. + Rewrite (Zeven_bit_value z H); Intros; Omega. + + Rewrite (Zodd_bit_value z H); Intros; Omega. +Save. + +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 : (n:nat) (bv : (Bvector n)) + (Z_to_binary n (binary_value n bv))=bv. +Proof. + NewInduction bv as [|a n bv IHbv]. + Auto. + + Rewrite binary_value_Sn. + Rewrite Z_to_binary_Sn. + Rewrite IHbv; Trivial. + + Apply binary_value_pos. +Save. + +Lemma two_compl_to_Z_to_two_compl : (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. + NewInduction bv as [|a n bv IHbv]; Intro b. + NewDestruct b; Auto. + + Rewrite two_compl_value_Sn. + Rewrite Z_to_two_compl_Sn. + Rewrite IHbv; Trivial. +Save. + +Lemma Z_to_binary_to_Z : (n:nat) (z : Z) + `z >= 0 `-> + `z < (two_power_nat n) `-> + (binary_value n (Z_to_binary n z))=z. +Proof. + NewInduction n as [|n IHn]. + Unfold two_power_nat shift_nat; Simpl; Intros; Omega. + + Intros; Rewrite Z_to_binary_Sn_z. + Rewrite binary_value_Sn. + Rewrite IHn. + Apply Z_div2_value; Auto. + + Apply Zdiv2_pos; Trivial. + + Apply Zdiv2_two_power_nat; Trivial. +Save. + +Lemma Z_to_two_compl_to_Z : (n:nat) (z : Z) + `z >= -(two_power_nat n) `-> + `z < (two_power_nat n) `-> + (two_compl_value n (Z_to_two_compl n z))=z. +Proof. + NewInduction n as [|n IHn]. + Unfold two_power_nat shift_nat; Simpl; Intros. + Assert `z=-1`\/`z=0`. 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. +Save. + +End COHERENT_VALUE. + |