diff options
Diffstat (limited to 'theories7/ZArith/Zbinary.v')
| -rw-r--r-- | theories7/ZArith/Zbinary.v | 425 |
1 files changed, 0 insertions, 425 deletions
diff --git a/theories7/ZArith/Zbinary.v b/theories7/ZArith/Zbinary.v deleted file mode 100644 index c3efbe1e..00000000 --- a/theories7/ZArith/Zbinary.v +++ /dev/null @@ -1,425 +0,0 @@ -(************************************************************************) -(* 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. - |