1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Zbinary.v,v 1.6.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
35 (*#* Bit vectors interpreted as integers.
36 Contribution by Jean Duprat (ENS Lyon). *)
38 include "Bool/Bvector.ma".
40 include "ZArith/ZArith.ma".
42 include "ZArith/Zpower.ma".
45 L'\195\\169\valuation des vecteurs de bool\195\\169\ens se font \195\\160\ la fois en binaire et
46 en compl\195\\169\ment \195\\160\ deux. Le nombre appartient \195\\160\ Z.
47 On utilise donc Omega pour faire les calculs dans Z.
48 De plus, on utilise les fonctions 2^n o\195\\185\ n est un naturel, ici la longueur.
49 two_power_nat = [n:nat](POS (shift_nat n xH))
52 : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)`
54 : (x,y:Z){`x < y`}+{`x >= y`}
58 Section VALUE_OF_BOOLEAN_VECTORS
62 Les calculs sont effectu\195\\169\s dans la convention positive usuelle.
63 Les valeurs correspondent soit \195\\160\ l'\195\\169\criture binaire (nat),
64 soit au compl\195\\169\ment \195\\160\ deux (int).
65 On effectue le calcul suivant le sch\195\\169\ma de Horner.
66 Le compl\195\\169\ment \195\\160\ deux n'a de sens que sur les vecteurs de taille
67 sup\195\\169\rieure ou \195\\169\gale \195\\160\ un, le bit de signe \195\\169\tant \195\\169\valu\195\\169\ n\195\\169\gativement.
70 inline procedural "cic:/Coq/ZArith/Zbinary/bit_value.con" as definition.
72 inline procedural "cic:/Coq/ZArith/Zbinary/binary_value.con" as lemma.
74 inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_value.con" as lemma.
77 Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))).
83 Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))).
89 End VALUE_OF_BOOLEAN_VECTORS
93 Section ENCODING_VALUE
97 On calcule la valeur binaire selon un schema de Horner.
98 Le calcul s'arrete \195\\160\ la longueur du vecteur sans v\195\\169\rification.
99 On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient
100 de la division z=2q+r avec 0<=r<=1.
101 La valeur en compl\195\\169\ment \195\\160\ deux est calcul\195\\169\e selon un schema de Horner
102 avec Zmod2, le param\195\\168\tre est la taille moins un.
105 inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2.con" as definition.
107 inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2_twice.con" as lemma.
109 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary.con" as lemma.
112 Eval Compute in (Z_to_binary (5) `5`).
113 = (Vcons bool true (4)
114 (Vcons bool false (3)
116 (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))))
120 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl.con" as lemma.
123 Eval Compute in (Z_to_two_compl (3) `0`).
124 = (Vcons bool false (3)
125 (Vcons bool false (2)
126 (Vcons bool false (1) (Vcons bool false (0) (Vnil bool)))))
129 Eval Compute in (Z_to_two_compl (3) `5`).
130 = (Vcons bool true (3)
131 (Vcons bool false (2)
132 (Vcons bool true (1) (Vcons bool false (0) (Vnil bool)))))
135 Eval Compute in (Z_to_two_compl (3) `-5`).
136 = (Vcons bool true (3)
138 (Vcons bool false (1) (Vcons bool true (0) (Vnil bool)))))
147 Section Z_BRIC_A_BRAC
151 Bibliotheque de lemmes utiles dans la section suivante.
152 Utilise largement ZArith.
153 Meriterait d'etre reecrite.
156 inline procedural "cic:/Coq/ZArith/Zbinary/binary_value_Sn.con" as lemma.
158 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn.con" as lemma.
160 inline procedural "cic:/Coq/ZArith/Zbinary/binary_value_pos.con" as lemma.
162 inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_value_Sn.con" as lemma.
164 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn.con" as lemma.
166 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn_z.con" as lemma.
168 inline procedural "cic:/Coq/ZArith/Zbinary/Z_div2_value.con" as lemma.
170 inline procedural "cic:/Coq/ZArith/Zbinary/Pdiv2.con" as lemma.
172 inline procedural "cic:/Coq/ZArith/Zbinary/Zdiv2_two_power_nat.con" as lemma.
176 Lemma Z_minus_one_or_zero : (z:Z)
199 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn_z.con" as lemma.
201 inline procedural "cic:/Coq/ZArith/Zbinary/Zeven_bit_value.con" as lemma.
203 inline procedural "cic:/Coq/ZArith/Zbinary/Zodd_bit_value.con" as lemma.
205 inline procedural "cic:/Coq/ZArith/Zbinary/Zge_minus_two_power_nat_S.con" as lemma.
207 inline procedural "cic:/Coq/ZArith/Zbinary/Zlt_two_power_nat_S.con" as lemma.
214 Section COHERENT_VALUE
218 On v\195\\169\rifie que dans l'intervalle de d\195\\169\finition les fonctions sont
219 r\195\\169\ciproques l'une de l'autre.
220 Elles utilisent les lemmes du bric-a-brac.
223 inline procedural "cic:/Coq/ZArith/Zbinary/binary_to_Z_to_binary.con" as lemma.
225 inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_to_Z_to_two_compl.con" as lemma.
227 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_to_Z.con" as lemma.
229 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_to_Z.con" as lemma.