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___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
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 2004/02/10 15:38:01 marche 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ètre trop important pour
50 se contenter de la fonction "length".
51 La première idé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ée est de faire un type dépendant dans lequel la
55 longueur est un paramètre de construction. Cela complique un
56 peu les inductions structurelles, la solution qui a ma préférence
57 est alors d'utiliser un terme de preuve comme définition.
59 (En effet une dé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'éléments d'un ensemble A.
101 Si la taille est non nulle, on peut extraire la première composante et
102 le reste du vecteur, la dernière composante ou rajouter ou enlever
103 une composante (carry) ou repeter la dernière composante en fin de vecteur.
104 On peut aussi tronquer le vecteur de ses p dernières composantes ou
105 au contraire l'étendre (concaténer) d'un vecteur de longueur p.
106 Une fonction unaire sur A génère une fonction des vecteurs de taille n
107 dans les vecteurs de taille n en appliquant f terme à terme.
108 Une fonction binaire sur A génère une fonction des couple de vecteurs
109 de taille n dans les vecteurs de taille n en appliquant f terme à 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éens de longueur fixe.
170 ATTENTION : le stockage s'effectue poids FAIBLE en tête.
171 On en extrait le bit de poids faible (head) et la fin du vecteur (tail).
172 On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs.
173 On calcule les dé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érant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique).
176 ATTENTION : Tous les décalages prennent la taille moins un comme paramè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.