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: Bvector.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
35 (*#* Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
37 include "Bool/Bool.ma".
39 include "Bool/Sumbool.ma".
41 include "Arith/Arith.ma".
44 Open Local Scope nat_scope.
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.
59 (En effet une d\233\finition comme :
60 Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) :=
63 | (Vcons a p v') => (Vcons (f a) p (Vunaire p v'))
65 provoque ce message d'erreur :
66 Coq < Error: Inference of annotation not yet implemented in this case).
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
73 | (cons x _) => (Value x)
75 : (A:Set)(list A)->(option A).
76 tail = [A:Set; l:(list A)]Cases l of
80 : (A:Set)(list A)->(list A).
81 length = [A:Set] Fix length {length [l:(list A)] : nat :=
84 | (cons _ m) => (S (length m))
86 : (A:Set)(list A)->nat.
87 map = [A,B:Set; f:(A->B)] Fix map {map [l:(list A)] : (list B) :=
90 | (cons a t) => (cons (f a) (map t))
92 : (A,B:Set)(A->B)->(list A)->(list B)
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.
113 cic:/Coq/Bool/Bvector/VECTORS/A.var
116 inline procedural "cic:/Coq/Bool/Bvector/vector.ind".
118 inline procedural "cic:/Coq/Bool/Bvector/Vhead.con" as definition.
120 inline procedural "cic:/Coq/Bool/Bvector/Vtail.con" as definition.
122 inline procedural "cic:/Coq/Bool/Bvector/Vlast.con" as definition.
124 inline procedural "cic:/Coq/Bool/Bvector/Vconst.con" as definition.
126 inline procedural "cic:/Coq/Bool/Bvector/Vshiftout.con" as lemma.
128 inline procedural "cic:/Coq/Bool/Bvector/Vshiftin.con" as lemma.
130 inline procedural "cic:/Coq/Bool/Bvector/Vshiftrepeat.con" as lemma.
133 Lemma S_minus_S : (n,p:nat) (gt n (S p)) -> (S (minus n (S p)))=(minus n p).
139 inline procedural "cic:/Coq/Bool/Bvector/Vtrunc.con" as lemma.
141 inline procedural "cic:/Coq/Bool/Bvector/Vextend.con" as lemma.
144 cic:/Coq/Bool/Bvector/VECTORS/f.var
147 inline procedural "cic:/Coq/Bool/Bvector/Vunary.con" as lemma.
150 cic:/Coq/Bool/Bvector/VECTORS/g.var
153 inline procedural "cic:/Coq/Bool/Bvector/Vbinary.con" as lemma.
159 (* suppressed: incompatible with Coq-Art book
160 Implicit Arguments Vnil [A].
161 Implicit Arguments Vcons [A n].
165 Section BOOLEAN_VECTORS
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).
180 inline procedural "cic:/Coq/Bool/Bvector/Bvector.con" as definition.
182 inline procedural "cic:/Coq/Bool/Bvector/Bnil.con" as definition.
184 inline procedural "cic:/Coq/Bool/Bvector/Bcons.con" as definition.
186 inline procedural "cic:/Coq/Bool/Bvector/Bvect_true.con" as definition.
188 inline procedural "cic:/Coq/Bool/Bvector/Bvect_false.con" as definition.
190 inline procedural "cic:/Coq/Bool/Bvector/Blow.con" as definition.
192 inline procedural "cic:/Coq/Bool/Bvector/Bhigh.con" as definition.
194 inline procedural "cic:/Coq/Bool/Bvector/Bsign.con" as definition.
196 inline procedural "cic:/Coq/Bool/Bvector/Bneg.con" as definition.
198 inline procedural "cic:/Coq/Bool/Bvector/BVand.con" as definition.
200 inline procedural "cic:/Coq/Bool/Bvector/BVor.con" as definition.
202 inline procedural "cic:/Coq/Bool/Bvector/BVxor.con" as definition.
204 inline procedural "cic:/Coq/Bool/Bvector/BshiftL.con" as definition.
206 inline procedural "cic:/Coq/Bool/Bvector/BshiftRl.con" as definition.
208 inline procedural "cic:/Coq/Bool/Bvector/BshiftRa.con" as definition.
210 inline procedural "cic:/Coq/Bool/Bvector/BshiftL_iter.con" as definition.
212 inline procedural "cic:/Coq/Bool/Bvector/BshiftRl_iter.con" as definition.
214 inline procedural "cic:/Coq/Bool/Bvector/BshiftRa_iter.con" as definition.