helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Zbinary.v,v 1.6.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
  34
  35 (*#* Bit vectors interpreted as integers.
  36     Contribution by Jean Duprat (ENS Lyon). *)
  37
  38 include "Bool/Bvector.ma".
  39
  40 include "ZArith/ZArith.ma".
  41
  42 include "ZArith/Zpower.ma".
  43
  44 (*
  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))
  50                 : nat->Z
  51         two_power_nat_S
  52              : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)`
  53         Z_lt_ge_dec
  54              : (x,y:Z){`x < y`}+{`x >= y`}
  55 *)
  56
  57 (* UNEXPORTED
  58 Section VALUE_OF_BOOLEAN_VECTORS
  59 *)
  60
  61 (*
  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.
  68 *)
  69
  70 inline procedural "cic:/Coq/ZArith/Zbinary/bit_value.con" as definition.
  71
  72 inline procedural "cic:/Coq/ZArith/Zbinary/binary_value.con" as lemma.
  73
  74 inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_value.con" as lemma.
  75
  76 (*
  77 Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))).
  78      = `5`
  79      : Z
  80 *)
  81
  82 (*
  83 Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))).
  84      = `-3`
  85      : Z
  86 *)
  87
  88 (* UNEXPORTED
  89 End VALUE_OF_BOOLEAN_VECTORS
  90 *)
  91
  92 (* UNEXPORTED
  93 Section ENCODING_VALUE
  94 *)
  95
  96 (*
  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.
 103 *)
 104
 105 inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2.con" as definition.
 106
 107 inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2_twice.con" as lemma.
 108
 109 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary.con" as lemma.
 110
 111 (*
 112 Eval Compute in (Z_to_binary (5) `5`).
 113      = (Vcons bool true (4)
 114           (Vcons bool false (3)
 115             (Vcons bool true (2)
 116               (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))))
 117      :  (Bvector (5))
 118 *)
 119
 120 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl.con" as lemma.
 121
 122 (*
 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)))))
 127      :  (vector bool (4))
 128
 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)))))
 133      :  (vector bool (4))
 134
 135 Eval Compute in (Z_to_two_compl (3) `-5`).
 136      =  (Vcons bool true (3)
 137           (Vcons bool true (2)
 138             (Vcons bool false (1) (Vcons bool true (0) (Vnil bool)))))
 139      :  (vector bool (4))
 140 *)
 141
 142 (* UNEXPORTED
 143 End ENCODING_VALUE
 144 *)
 145
 146 (* UNEXPORTED
 147 Section Z_BRIC_A_BRAC
 148 *)
 149
 150 (*
 151 Bibliotheque de lemmes utiles dans la section suivante.
 152 Utilise largement ZArith.
 153 Meriterait d'etre reecrite.
 154 *)
 155
 156 inline procedural "cic:/Coq/ZArith/Zbinary/binary_value_Sn.con" as lemma.
 157
 158 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn.con" as lemma.
 159
 160 inline procedural "cic:/Coq/ZArith/Zbinary/binary_value_pos.con" as lemma.
 161
 162 inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_value_Sn.con" as lemma.
 163
 164 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn.con" as lemma.
 165
 166 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_Sn_z.con" as lemma.
 167
 168 inline procedural "cic:/Coq/ZArith/Zbinary/Z_div2_value.con" as lemma.
 169
 170 inline procedural "cic:/Coq/ZArith/Zbinary/Pdiv2.con" as lemma.
 171
 172 inline procedural "cic:/Coq/ZArith/Zbinary/Zdiv2_two_power_nat.con" as lemma.
 173
 174 (*
 175
 176 Lemma Z_minus_one_or_zero : (z:Z)
 177         `z >= -1` ->
 178         `z < 1` ->
 179         {`z=-1`} + {`z=0`}.
 180 Proof.
 181         NewDestruct z; Auto.
 182         NewDestruct p; Auto.
 183         Tauto.
 184
 185         Tauto.
 186
 187         Intros.
 188         Right; Omega.
 189
 190         NewDestruct p.
 191         Tauto.
 192
 193         Tauto.
 194
 195         Intros; Left; Omega.
 196 Save.
 197 *)
 198
 199 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_Sn_z.con" as lemma.
 200
 201 inline procedural "cic:/Coq/ZArith/Zbinary/Zeven_bit_value.con" as lemma.
 202
 203 inline procedural "cic:/Coq/ZArith/Zbinary/Zodd_bit_value.con" as lemma.
 204
 205 inline procedural "cic:/Coq/ZArith/Zbinary/Zge_minus_two_power_nat_S.con" as lemma.
 206
 207 inline procedural "cic:/Coq/ZArith/Zbinary/Zlt_two_power_nat_S.con" as lemma.
 208
 209 (* UNEXPORTED
 210 End Z_BRIC_A_BRAC
 211 *)
 212
 213 (* UNEXPORTED
 214 Section COHERENT_VALUE
 215 *)
 216
 217 (*
 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.
 221 *)
 222
 223 inline procedural "cic:/Coq/ZArith/Zbinary/binary_to_Z_to_binary.con" as lemma.
 224
 225 inline procedural "cic:/Coq/ZArith/Zbinary/two_compl_to_Z_to_two_compl.con" as lemma.
 226
 227 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_binary_to_Z.con" as lemma.
 228
 229 inline procedural "cic:/Coq/ZArith/Zbinary/Z_to_two_compl_to_Z.con" as lemma.
 230
 231 (* UNEXPORTED
 232 End COHERENT_VALUE
 233 *)
 234