helm/software/matita/contribs/procedural/Coq/Bool/Bvector.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: Bvector.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
  34
  35 (*#* Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
  36
  37 include "Bool/Bool.ma".
  38
  39 include "Bool/Sumbool.ma".
  40
  41 include "Arith/Arith.ma".
  42
  43 (* UNEXPORTED
  44 Open Local Scope nat_scope.
  45 *)
  46
  47 (*
  48 On s'inspire de PolyList pour fabriquer les vecteurs de bits.
  49 La dimension du vecteur est un param\232\tre trop important pour
  50 se contenter de la fonction "length".
  51 La premi\232\re id\233\e est de faire un record avec la liste et la longueur.
  52 Malheureusement, cette verification a posteriori amene a faire
  53 de nombreux lemmes pour gerer les longueurs.
  54 La seconde id\233\e est de faire un type d\233\pendant dans lequel la
  55 longueur est un param\232\tre de construction. Cela complique un
  56 peu les inductions structurelles, la solution qui a ma pr\233\f\233\rence
  57 est alors d'utiliser un terme de preuve comme d\233\finition.
  58
  59 (En effet une d\233\finition comme :
  60 Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) :=
  61 Cases v of
  62         | Vnil => Vnil
  63         | (Vcons a p v') => (Vcons (f a) p (Vunaire p v'))
  64 end.
  65 provoque ce message d'erreur :
  66 Coq < Error: Inference of annotation not yet implemented in this case).
  67
  68
  69         Inductive list [A : Set]  : Set :=
  70                 nil : (list A) | cons : A->(list A)->(list A).
  71         head = [A:Set; l:(list A)] Cases l of
  72                         | nil => Error
  73                         | (cons x _) => (Value x)
  74                         end
  75                 : (A:Set)(list A)->(option A).
  76         tail = [A:Set; l:(list A)]Cases l of
  77                                         | nil => (nil A)
  78                                         | (cons _ m) => m
  79                                         end
  80                 : (A:Set)(list A)->(list A).
  81         length = [A:Set] Fix length {length [l:(list A)] : nat :=
  82                 Cases l of
  83                         | nil => O
  84                         | (cons _ m) => (S (length m))
  85                 end}
  86                 : (A:Set)(list A)->nat.
  87         map = [A,B:Set; f:(A->B)] Fix map {map [l:(list A)] : (list B) :=
  88                 Cases l of
  89                         | nil => (nil B)
  90                         | (cons a t) => (cons (f a) (map t))
  91                 end}
  92                 : (A,B:Set)(A->B)->(list A)->(list B)
  93 *)
  94
  95 (* UNEXPORTED
  96 Section VECTORS
  97 *)
  98
  99 (*
 100 Un vecteur est une liste de taille n d'\233\l\233\ments d'un ensemble A.
 101 Si la taille est non nulle, on peut extraire la premi\232\re composante et
 102 le reste du vecteur, la derni\232\re composante ou rajouter ou enlever
 103 une composante (carry) ou repeter la derni\232\re composante en fin de vecteur.
 104 On peut aussi tronquer le vecteur de ses p derni\232\res composantes ou
 105 au contraire l'\233\tendre (concat\233\ner) d'un vecteur de longueur p.
 106 Une fonction unaire sur A g\233\n\232\re une fonction des vecteurs de taille n
 107 dans les vecteurs de taille n en appliquant f terme \224\ terme.
 108 Une fonction binaire sur A g\233\n\232\re une fonction des couple de vecteurs
 109 de taille n dans les vecteurs de taille n en appliquant f terme \224\ terme.
 110 *)
 111
 112 (* UNEXPORTED
 113 cic:/Coq/Bool/Bvector/VECTORS/A.var
 114 *)
 115
 116 inline procedural "cic:/Coq/Bool/Bvector/vector.ind".
 117
 118 inline procedural "cic:/Coq/Bool/Bvector/Vhead.con" as definition.
 119
 120 inline procedural "cic:/Coq/Bool/Bvector/Vtail.con" as definition.
 121
 122 inline procedural "cic:/Coq/Bool/Bvector/Vlast.con" as definition.
 123
 124 inline procedural "cic:/Coq/Bool/Bvector/Vconst.con" as definition.
 125
 126 inline procedural "cic:/Coq/Bool/Bvector/Vshiftout.con" as lemma.
 127
 128 inline procedural "cic:/Coq/Bool/Bvector/Vshiftin.con" as lemma.
 129
 130 inline procedural "cic:/Coq/Bool/Bvector/Vshiftrepeat.con" as lemma.
 131
 132 (*
 133 Lemma S_minus_S : (n,p:nat) (gt n (S p)) -> (S (minus n (S p)))=(minus n p).
 134 Proof.
 135   Intros.
 136 Save.
 137 *)
 138
 139 inline procedural "cic:/Coq/Bool/Bvector/Vtrunc.con" as lemma.
 140
 141 inline procedural "cic:/Coq/Bool/Bvector/Vextend.con" as lemma.
 142
 143 (* UNEXPORTED
 144 cic:/Coq/Bool/Bvector/VECTORS/f.var
 145 *)
 146
 147 inline procedural "cic:/Coq/Bool/Bvector/Vunary.con" as lemma.
 148
 149 (* UNEXPORTED
 150 cic:/Coq/Bool/Bvector/VECTORS/g.var
 151 *)
 152
 153 inline procedural "cic:/Coq/Bool/Bvector/Vbinary.con" as lemma.
 154
 155 (* UNEXPORTED
 156 End VECTORS
 157 *)
 158
 159 (* suppressed: incompatible with Coq-Art book
 160 Implicit Arguments Vnil [A].
 161 Implicit Arguments Vcons [A n].
 162 *)
 163
 164 (* UNEXPORTED
 165 Section BOOLEAN_VECTORS
 166 *)
 167
 168 (*
 169 Un vecteur de bits est un vecteur sur l'ensemble des bool\233\ens de longueur fixe.
 170 ATTENTION : le stockage s'effectue poids FAIBLE en t\234\te.
 171 On en extrait le bit  de poids faible (head) et la fin du vecteur (tail).
 172 On calcule la n\233\gation d'un vecteur, le et, le ou et le xor bit \224\ bit de 2 vecteurs.
 173 On calcule les d\233\calages d'une position vers la gauche (vers les poids forts, on
 174 utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en
 175 ins\233\rant un bit 'carry' (logique) ou en r\233\p\233\tant le bit de poids fort (arithm\233\tique).
 176 ATTENTION : Tous les d\233\calages prennent la taille moins un comme param\232\tre
 177 (ils ne travaillent que sur des vecteurs au moins de longueur un).
 178 *)
 179
 180 inline procedural "cic:/Coq/Bool/Bvector/Bvector.con" as definition.
 181
 182 inline procedural "cic:/Coq/Bool/Bvector/Bnil.con" as definition.
 183
 184 inline procedural "cic:/Coq/Bool/Bvector/Bcons.con" as definition.
 185
 186 inline procedural "cic:/Coq/Bool/Bvector/Bvect_true.con" as definition.
 187
 188 inline procedural "cic:/Coq/Bool/Bvector/Bvect_false.con" as definition.
 189
 190 inline procedural "cic:/Coq/Bool/Bvector/Blow.con" as definition.
 191
 192 inline procedural "cic:/Coq/Bool/Bvector/Bhigh.con" as definition.
 193
 194 inline procedural "cic:/Coq/Bool/Bvector/Bsign.con" as definition.
 195
 196 inline procedural "cic:/Coq/Bool/Bvector/Bneg.con" as definition.
 197
 198 inline procedural "cic:/Coq/Bool/Bvector/BVand.con" as definition.
 199
 200 inline procedural "cic:/Coq/Bool/Bvector/BVor.con" as definition.
 201
 202 inline procedural "cic:/Coq/Bool/Bvector/BVxor.con" as definition.
 203
 204 inline procedural "cic:/Coq/Bool/Bvector/BshiftL.con" as definition.
 205
 206 inline procedural "cic:/Coq/Bool/Bvector/BshiftRl.con" as definition.
 207
 208 inline procedural "cic:/Coq/Bool/Bvector/BshiftRa.con" as definition.
 209
 210 inline procedural "cic:/Coq/Bool/Bvector/BshiftL_iter.con" as definition.
 211
 212 inline procedural "cic:/Coq/Bool/Bvector/BshiftRl_iter.con" as definition.
 213
 214 inline procedural "cic:/Coq/Bool/Bvector/BshiftRa_iter.con" as definition.
 215
 216 (* UNEXPORTED
 217 End BOOLEAN_VECTORS
 218 *)
 219