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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
  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 2004/02/10 15:38:01 marche 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'évaluation des vecteurs de booléens se font à la fois en binaire et
  46 en complément à deux. Le nombre appartient à Z.
  47 On utilise donc Omega pour faire les calculs dans Z.
  48 De plus, on utilise les fonctions 2^n où 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és dans la convention positive usuelle.
  63 Les valeurs correspondent soit à l'écriture binaire (nat),
  64 soit au complément à deux (int).
  65 On effectue le calcul suivant le schéma de Horner.
  66 Le complément à deux n'a de sens que sur les vecteurs de taille
  67 supérieure ou égale à un, le bit de signe étant évalué né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 à la longueur du vecteur sans vé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ément à deux est calculée selon un schema de Horner
 102 avec Zmod2, le paramè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érifie que dans l'intervalle de définition les fonctions sont
 219 ré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