← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Bool/Bvector.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Bool/Bvector.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Bvector.v 11004 2008-05-28 09:09:12Z herbelin $ i*)
 
10
 
 
11
(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
12
 
 
13
Require Export Bool.
 
14
Require Export Sumbool.
 
15
Require Import Arith.
 
16
 
 
17
Open Local Scope nat_scope.
 
18
 
 
19
(** 
 
20
On s'inspire de List.v pour fabriquer les vecteurs de bits.
 
21
La dimension du vecteur est un param�tre trop important pour
 
22
se contenter de la fonction "length".
 
23
La premi�re id�e est de faire un record avec la liste et la longueur.
 
24
Malheureusement, cette verification a posteriori amene a faire
 
25
de nombreux lemmes pour gerer les longueurs.
 
26
La seconde id�e est de faire un type d�pendant dans lequel la
 
27
longueur est un param�tre de construction. Cela complique un
 
28
peu les inductions structurelles et dans certains cas on
 
29
utilisera un terme de preuve comme d�finition, car le
 
30
m�canisme d'inf�rence du type du filtrage n'est pas toujours 
 
31
aussi puissant que celui implant� par les tactiques d'�limination.
 
32
*)
 
33
 
 
34
Section VECTORS.
 
35
 
 
36
(** 
 
37
Un vecteur est une liste de taille n d'�l�ments d'un ensemble A.
 
38
Si la taille est non nulle, on peut extraire la premi�re composante et 
 
39
le reste du vecteur, la derni�re composante ou rajouter ou enlever 
 
40
une composante (carry) ou repeter la derni�re composante en fin de vecteur.
 
41
On peut aussi tronquer le vecteur de ses p derni�res composantes ou
 
42
au contraire l'�tendre (concat�ner) d'un vecteur de longueur p.
 
43
Une fonction unaire sur A g�n�re une fonction des vecteurs de taille n
 
44
dans les vecteurs de taille n en appliquant f terme � terme.
 
45
Une fonction binaire sur A g�n�re une fonction des couples de vecteurs 
 
46
de taille n dans les vecteurs de taille n en appliquant f terme � terme.
 
47
*)
 
48
 
 
49
Variable A : Type.
 
50
 
 
51
Inductive vector : nat -> Type :=
 
52
  | Vnil : vector 0
 
53
  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
 
54
 
 
55
Definition Vhead (n:nat) (v:vector (S n)) :=
 
56
  match v with
 
57
  | Vcons a _ _ => a
 
58
  end.
 
59
 
 
60
Definition Vtail (n:nat) (v:vector (S n)) :=
 
61
  match v with
 
62
  | Vcons _ _ v => v
 
63
  end.
 
64
 
 
65
Definition Vlast : forall n:nat, vector (S n) -> A.
 
66
Proof.
 
67
  induction n as [| n f]; intro v.
 
68
  inversion v.
 
69
  exact a.
 
70
 
 
71
  inversion v as [| n0 a H0 H1].
 
72
  exact (f H0).
 
73
Defined.
 
74
 
 
75
Fixpoint Vconst (a:A) (n:nat) :=
 
76
  match n return vector n with
 
77
  | O => Vnil
 
78
  | S n => Vcons a _ (Vconst a n)
 
79
  end.
 
80
 
 
81
(** Shifting and truncating *)
 
82
 
 
83
Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
 
84
Proof.
 
85
  induction n as [| n f]; intro v.
 
86
  exact Vnil.
 
87
 
 
88
  inversion v as [| a n0 H0 H1].
 
89
  exact (Vcons a n (f H0)).
 
90
Defined.
 
91
 
 
92
Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
 
93
Proof.
 
94
  induction n as [| n f]; intros a v.
 
95
  exact (Vcons a 0 v).
 
96
  
 
97
  inversion v as [| a0 n0 H0 H1 ].
 
98
  exact (Vcons a (S n) (f a H0)).
 
99
Defined.
 
100
 
 
101
Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)).
 
102
Proof.
 
103
  induction n as [| n f]; intro v.
 
104
  inversion v.
 
105
  exact (Vcons a 1 v).
 
106
  
 
107
  inversion v as [| a n0 H0 H1 ].
 
108
  exact (Vcons a (S (S n)) (f H0)).
 
109
Defined.
 
110
 
 
111
Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p).
 
112
Proof.
 
113
  induction p as [| p f]; intros H v.
 
114
  rewrite <- minus_n_O.
 
115
  exact v.
 
116
  
 
117
  apply (Vshiftout (n - S p)).
 
118
  
 
119
  rewrite minus_Sn_m.
 
120
  apply f.
 
121
  auto with *.
 
122
  exact v.
 
123
  auto with *.
 
124
Defined.
 
125
 
 
126
(** Concatenation of two vectors *)
 
127
 
 
128
Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) :=
 
129
  match v with
 
130
  | Vnil => w
 
131
  | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w)
 
132
  end.
 
133
 
 
134
(** Uniform application on the arguments of the vector *)
 
135
 
 
136
Variable f : A -> A.
 
137
 
 
138
Fixpoint Vunary n (v:vector n) : vector n :=
 
139
  match v with
 
140
  | Vnil => Vnil
 
141
  | Vcons a n' v' => Vcons (f a) n' (Vunary n' v')
 
142
  end.
 
143
 
 
144
Variable g : A -> A -> A.
 
145
 
 
146
Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
 
147
Proof.
 
148
  induction n as [| n h]; intros v v0.
 
149
  exact Vnil.
 
150
  
 
151
  inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
 
152
  exact (Vcons (g a a0) n (h H0 H2)).
 
153
Defined.
 
154
 
 
155
(** Eta-expansion of a vector *)
 
156
 
 
157
Definition Vid n : vector n -> vector n :=
 
158
  match n with
 
159
  | O => fun _ => Vnil
 
160
  | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v)
 
161
  end.
 
162
 
 
163
Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
 
164
Proof.
 
165
  destruct v; auto.
 
166
Qed.
 
167
 
 
168
Lemma VSn_eq :
 
169
  forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v).
 
170
Proof.
 
171
  intros.
 
172
  exact (Vid_eq _ v).
 
173
Qed.
 
174
 
 
175
Lemma V0_eq : forall (v : vector 0), v = Vnil.
 
176
Proof.
 
177
  intros.
 
178
  exact (Vid_eq _ v).
 
179
Qed.
 
180
 
 
181
End VECTORS.
 
182
 
 
183
(* suppressed: incompatible with Coq-Art book 
 
184
Implicit Arguments Vnil [A].
 
185
Implicit Arguments Vcons [A n].
 
186
*)
 
187
 
 
188
Section BOOLEAN_VECTORS.
 
189
 
 
190
(**
 
191
Un vecteur de bits est un vecteur sur l'ensemble des bool�ens de longueur fixe. 
 
192
ATTENTION : le stockage s'effectue poids FAIBLE en t�te.
 
193
On en extrait le bit  de poids faible (head) et la fin du vecteur (tail).
 
194
On calcule la n�gation d'un vecteur, le et, le ou et le xor bit � bit de 2 vecteurs.
 
195
On calcule les d�calages d'une position vers la gauche (vers les poids forts, on
 
196
utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en 
 
197
ins�rant un bit 'carry' (logique) ou en r�p�tant le bit de poids fort (arithm�tique).
 
198
ATTENTION : Tous les d�calages prennent la taille moins un comme param�tre
 
199
(ils ne travaillent que sur des vecteurs au moins de longueur un).
 
200
*)
 
201
 
 
202
Definition Bvector := vector bool.
 
203
 
 
204
Definition Bnil := @Vnil bool.
 
205
 
 
206
Definition Bcons := @Vcons bool.
 
207
 
 
208
Definition Bvect_true := Vconst bool true.
 
209
 
 
210
Definition Bvect_false := Vconst bool false.
 
211
 
 
212
Definition Blow := Vhead bool.
 
213
 
 
214
Definition Bhigh := Vtail bool.
 
215
 
 
216
Definition Bsign := Vlast bool.
 
217
 
 
218
Definition Bneg := Vunary bool negb.
 
219
 
 
220
Definition BVand := Vbinary bool andb.
 
221
 
 
222
Definition BVor := Vbinary bool orb.
 
223
 
 
224
Definition BVxor := Vbinary bool xorb.
 
225
 
 
226
Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
 
227
  Bcons carry n (Vshiftout bool n bv).
 
228
 
 
229
Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
 
230
  Bhigh (S n) (Vshiftin bool (S n) carry bv).
 
231
 
 
232
Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
 
233
  Bhigh (S n) (Vshiftrepeat bool n bv).
 
234
 
 
235
Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
 
236
  Bvector (S n) :=
 
237
  match p with
 
238
    | O => bv
 
239
    | S p' => BshiftL n (BshiftL_iter n bv p') false
 
240
  end.
 
241
 
 
242
Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
 
243
  Bvector (S n) :=
 
244
  match p with
 
245
    | O => bv
 
246
    | S p' => BshiftRl n (BshiftRl_iter n bv p') false
 
247
  end.
 
248
 
 
249
Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
 
250
  Bvector (S n) :=
 
251
  match p with
 
252
    | O => bv
 
253
    | S p' => BshiftRa n (BshiftRa_iter n bv p')
 
254
  end.
 
255
 
 
256
End BOOLEAN_VECTORS.