bit vectors

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 718 insertions, 60 deletions

diff --git a/.depend b/.depend
index 191c123b22..4f7d287eea 100644
--- a/.depend
+++ b/.depend
@@ -930,17 +930,17 @@ parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \
     library/libnames.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     interp/ppextend.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
     interp/topconstr.cmx lib/util.cmx parsing/pcoq.cmi 
-parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \
-    parsing/coqast.cmi lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi \
-    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi \
-    interp/symbols.cmi kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
+parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
+    lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi library/libnames.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \
+    kernel/term.cmi parsing/termast.cmi interp/topconstr.cmi lib/util.cmi \
     parsing/ppconstr.cmi 
-parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \
-    parsing/coqast.cmx lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx \
-    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx interp/ppextend.cmx pretyping/rawterm.cmx \
-    interp/symbols.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
+parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
+    lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx library/libnames.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \
+    kernel/term.cmx parsing/termast.cmx interp/topconstr.cmx lib/util.cmx \
     parsing/ppconstr.cmi 
 parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
diff --git a/.depend.coq b/.depend.coq
index 46d0e731ba..f665c04dc7 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -103,6 +103,7 @@ theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/B
 theories/Bool/DecBool.vo: theories/Bool/DecBool.v
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
 theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
+theories/Bool/Bvector.vo: theories/Bool/Bvector.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo
 theories/ZArith/Wf_Z.vo: theories/ZArith/Wf_Z.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo
 theories/ZArith/Zsyntax.vo: theories/ZArith/Zsyntax.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo
 theories/ZArith/ZArith.vo: theories/ZArith/ZArith.v theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zpower.vo theories/ZArith/Zdiv.vo theories/ZArith/Zlogarithm.vo theories/ZArith/Zbool.vo
@@ -120,6 +121,7 @@ theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v theories/ZArith/ZArith_base.vo
 theories/ZArith/Zwf.vo: theories/ZArith/Zwf.v theories/ZArith/ZArith_base.vo theories/Arith/Wf_nat.vo contrib/omega/Omega.vo
 theories/ZArith/ZArith_base.vo: theories/ZArith/ZArith_base.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zhints.vo
 theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/ZArith_base.vo theories/Bool/Sumbool.vo
+theories/ZArith/Zbinary.vo: theories/ZArith/Zbinary.v theories/Bool/Bvector.vo theories/ZArith/ZArith.vo theories/ZArith/Zpower.vo contrib/omega/Omega.vo
 theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo
 theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo
 theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo
@@ -186,54 +188,6 @@ theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo
 theories/Reals/RealsB.vo: theories/Reals/RealsB.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/RealsB.vo contrib/omega/Omega.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/RealsB.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
-theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/RealsB.vo theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/RealsB.vo
-theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/RealsB.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/RealsB.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
-theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
-theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
-theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Arith/Max.vo
-theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo
-theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binome.vo
-theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplet.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binome.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo
-theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo
-theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo
-theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo
-theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
-theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
-theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
-theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
-theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo
-theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo
-theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
-theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
-theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
-theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/RealsB.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
-theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo
diff --git a/Makefile b/Makefile
index d0fc1ed2c2..b06646c50f 100644
--- a/Makefile
+++ b/Makefile
@@ -501,7 +501,8 @@ SORTINGVO=theories/Sorting/Heap.vo \
  
 BOOLVO=theories/Bool/Bool.vo  		theories/Bool/IfProp.vo \
        theories/Bool/Zerob.vo 		theories/Bool/DecBool.vo \
-	theories/Bool/Sumbool.vo 	theories/Bool/BoolEq.vo
+	theories/Bool/Sumbool.vo 	theories/Bool/BoolEq.vo \
+	theories/Bool/Bvector.vo
 
 ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/ZArith.vo      theories/ZArith/auxiliary.vo \
@@ -511,7 +512,7 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
 	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo \
 	 theories/ZArith/Zwf.vo		theories/ZArith/ZArith_base.vo \
-	 theories/ZArith/Zbool.vo
+	 theories/ZArith/Zbool.vo	theories/ZArith/Zbinary.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
new file mode 100644
index 0000000000..f26a83f837
--- /dev/null
+++ b/theories/Bool/Bvector.v
@@ -0,0 +1,263 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
+
+Require Export Bool.
+Require Export Sumbool.
+Require Arith.
+
+(*  
+On s'inspire de PolyList pour fabriquer les vecteurs de bits.
+La dimension du vecteur est un paramètre trop important pour
+se contenter de la fonction "length".
+La première idée est de faire un record avec la liste et la longueur.
+Malheureusement, cette verification a posteriori amene a faire
+de nombreux lemmes pour gerer les longueurs.
+La seconde idée est de faire un type dépendant dans lequel la
+longueur est un paramètre de construction. Cela complique un
+peu les inductions structurelles, la solution qui a ma préférence
+est alors d'utiliser un terme de preuve comme définition.
+
+(En effet une définition comme :
+Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) :=
+Cases v of
+	| Vnil => Vnil
+	| (Vcons a p v') => (Vcons (f a) p (Vunaire p v'))
+end.
+provoque ce message d'erreur :
+Coq < Error: Inference of annotation not yet implemented in this case).
+
+
+	Inductive list [A : Set]  : Set :=
+		nil : (list A) | cons : A->(list A)->(list A).
+	head = [A:Set; l:(list A)] Cases l of
+			| nil => Error
+ 			| (cons x _) => (Value x)
+ 			end
+     		: (A:Set)(list A)->(option A).
+	tail = [A:Set; l:(list A)]Cases l of
+                   			| nil => (nil A)
+                   			| (cons _ m) => m
+                   			end
+     		: (A:Set)(list A)->(list A).
+	length = [A:Set] Fix length {length [l:(list A)] : nat :=
+      		Cases l of
+       			| nil => O
+      			| (cons _ m) => (S (length m))
+      		end}
+     		: (A:Set)(list A)->nat.
+	map = [A,B:Set; f:(A->B)] Fix map {map [l:(list A)] : (list B) :=
+		Cases l of
+			| nil => (nil B)
+			| (cons a t) => (cons (f a) (map t))
+		end}
+		: (A,B:Set)(A->B)->(list A)->(list B)
+*)
+
+Section VECTORS.
+
+(* 
+Un vecteur est une liste de taille n d'éléments d'un ensemble A.
+Si la taille est non nulle, on peut extraire la première composante et 
+le reste du vecteur, la dernière composante ou rajouter ou enlever 
+une composante (carry) ou repeter la dernière composante en fin de vecteur.
+On peut aussi tronquer le vecteur de ses p dernières composantes ou
+au contraire l'étendre (concaténer) d'un vecteur de longueur p.
+Une fonction unaire sur A génère une fonction des vecteurs de taille n
+dans les vecteurs de taille n en appliquant f terme à terme.
+Une fonction binaire sur A génère une fonction des couple de vecteurs 
+de taille n dans les vecteurs de taille n en appliquant f terme à terme.
+*)
+
+Variable A : Set.
+
+Inductive vector: nat -> Set :=
+	| Vnil : (vector O)
+	| Vcons  : (a:A) (n:nat) (vector n) -> (vector (S n)).
+
+Definition Vhead : (n:nat) (vector (S n)) -> A.
+Proof.
+	Intros; Inversion H; Exact a.
+Defined.
+
+Definition Vtail : (n:nat) (vector (S n)) -> (vector n).
+Proof.
+	Intros; Inversion H; Exact H1.
+Defined.
+
+Definition Vlast : (n:nat) (vector (S n)) -> A.
+Proof.
+	Induction n; Intros.
+	Inversion H.
+	Exact a.
+
+	Inversion H0.
+	Exact (H H2).
+Defined.
+
+Definition Vconst : (a:A) (n:nat) (vector n).
+Proof.
+	Induction n; Intros.
+	Exact Vnil.
+
+	Exact (Vcons a n0 H).
+Defined.
+
+Lemma Vshiftout : (n:nat) (vector (S n)) -> (vector n).
+Proof.
+	Induction n; Intros.
+	Exact Vnil.
+
+	Inversion H0.
+	Exact (Vcons a n0 (H H2)).
+Defined.
+
+Lemma Vshiftin : (n:nat) A -> (vector n) -> (vector (S n)).
+Proof.
+	Induction n; Intros.
+	Exact (Vcons H O H0).
+
+	Inversion H1.
+	Exact (Vcons a (S n0) (H H0 H3)).
+Defined.
+
+Lemma Vshiftrepeat : (n:nat) (vector (S n)) -> (vector (S (S n))).
+Proof.
+	Induction n; Intros.
+	Inversion H.
+	Exact (Vcons a (1) H).
+
+	Inversion H0.
+	Exact (Vcons a (S (S n0)) (H H2)).
+Defined.
+
+(*
+Lemma S_minus_S : (n,p:nat) (gt n (S p)) -> (S (minus n (S p)))=(minus n p).
+Proof.
+  Intros.
+Save.
+*)
+
+Lemma Vtrunc : (n,p:nat) (gt n p) ->  (vector n) -> (vector (minus n p)).
+Proof.
+	Induction p; Intros.
+	Rewrite <- minus_n_O.
+	Exact H0.
+
+	Apply (Vshiftout (minus n (S n0))).
+
+Rewrite minus_Sn_m.
+Apply H.
+Auto with *.
+Exact H1.
+Auto with *.
+Defined.
+
+Lemma Vextend : (n,p:nat) (vector n) ->  (vector p) -> (vector (plus n p)).
+Proof.
+	Induction n; Intros.
+	Simpl; Exact H0.
+
+	Inversion H0.
+	Simpl; Exact (Vcons a (plus n0 p) (H p H3 H1)).
+Defined.
+
+Variable f : A -> A.
+
+Lemma Vunary : (n:nat)(vector n)->(vector n).
+Proof.
+	Induction n; Intros.
+	Exact Vnil.
+
+	Inversion H0.
+	Exact (Vcons (f a) n0 (H H2)).
+Defined.
+
+Variable g : A -> A -> A.
+
+Lemma Vbinary : (n:nat)(vector n)->(vector n)->(vector n).
+Proof.
+	Induction n; Intros.
+	Exact Vnil.
+
+	Inversion H0; Inversion H1.
+	Exact (Vcons (g a a0) n0 (H H3 H5)).
+Defined.
+
+End VECTORS.
+
+Section BOOLEAN_VECTORS.
+
+(* 
+Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. 
+ATTENTION : le stockage s'effectue poids FAIBLE en tête.
+On en extrait le bit  de poids faible (head) et la fin du vecteur (tail).
+On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs.
+On calcule les décalages d'une position vers la gauche (vers les poids forts, on
+utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en 
+insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique).
+ATTENTION : Tous les décalages prennent la taille moins un comme paramètre
+(ils ne travaillent que sur des vecteurs au moins de longueur un).
+*)
+
+Definition Bvector := (vector bool).
+
+Definition Bnil := (Vnil bool).
+
+Definition Bcons := (Vcons bool).
+
+Definition Bvect_true := (Vconst bool true).
+
+Definition Bvect_false := (Vconst bool false).
+
+Definition Blow := (Vhead bool).
+
+Definition Bhigh := (Vtail bool).
+
+Definition Bsign := (Vlast bool).
+
+Definition Bneg := (Vunary bool negb).
+
+Definition BVand := (Vbinary bool andb).
+
+Definition BVor := (Vbinary bool orb).
+
+Definition BVxor := (Vbinary bool xorb).
+
+Definition BshiftL := [n:nat; bv : (Bvector (S n)); carry:bool] 
+	(Bcons carry n (Vshiftout bool n bv)).
+
+Definition BshiftRl := [n:nat; bv : (Bvector (S n)); carry:bool] 
+	(Bhigh (S n) (Vshiftin bool (S n) carry bv)).
+
+Definition BshiftRa := [n:nat; bv : (Bvector (S n))] 
+	(Bhigh (S n) (Vshiftrepeat bool n bv)).
+
+Fixpoint BshiftL_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) :=
+Cases p of
+	| O => bv
+	| (S p') => (BshiftL n (BshiftL_iter n bv p') false)
+end.
+
+Fixpoint BshiftRl_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) :=
+Cases p of
+	| O => bv
+	| (S p') => (BshiftRl n (BshiftRl_iter n bv p') false)
+end.
+
+Fixpoint BshiftRa_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) :=
+Cases p of
+	| O => bv
+	| (S p') => (BshiftRa n (BshiftRa_iter n bv p'))
+end.
+
+End BOOLEAN_VECTORS.
+
diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v
new file mode 100644
index 0000000000..2e55242074
--- /dev/null
+++ b/theories/ZArith/Zbinary.v
@@ -0,0 +1,440 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Bit vectors interpreted as integers. 
+    Contribution by Jean Duprat (ENS Lyon). *)
+
+Require Bvector.
+Require ZArith.
+Require Export Zpower.
+Require Omega.
+
+(*
+L'évaluation des vecteurs de booléens se font à la fois en binaire et
+en complément à deux. Le nombre appartient à Z. 
+On utilise donc Omega pour faire les calculs dans Z.
+De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur.
+	two_power_nat = [n:nat](POS (shift_nat n xH))
+     		: nat->Z
+	two_power_nat_S
+	     : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)`
+	Z_lt_ge_dec
+	     : (x,y:Z){`x < y`}+{`x >= y`}
+*)
+
+
+Section VALUE_OF_BOOLEAN_VECTORS.
+
+(*
+Les calculs sont effectués dans la convention positive usuelle.
+Les valeurs correspondent soit à l'écriture binaire (nat), 
+soit au complément à deux (int).
+On effectue le calcul suivant le schéma de Horner.
+Le complément à deux n'a de sens que sur les vecteurs de taille 
+supérieure ou égale à un, le bit de signe étant évalué négativement.
+*)
+
+Definition bit_value [b:bool] : Z :=
+Cases b of
+	| true => `1`
+	| false => `0`
+end.
+
+Lemma binary_value  : (n:nat) (Bvector n) -> Z.
+Proof.
+	Induction n; Intros.
+	Exact `0`.
+
+	Inversion H0.
+	Exact (Zplus (bit_value a) (Zmult `2` (H H2))).
+Defined.
+
+Lemma two_compl_value : (n:nat) (Bvector (S n)) -> Z.
+Proof.
+	Induction n; Intros.
+	Inversion H.
+	Exact (Zopp (bit_value a)).
+
+	Inversion H0.
+	Exact (Zplus (bit_value a) (Zmult `2` (H H2))).
+Defined.
+
+(*
+Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))).
+     = `5`
+     : Z
+*)
+
+(*
+Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))).
+     = `-3`
+     : Z
+*)
+
+End VALUE_OF_BOOLEAN_VECTORS.
+
+Section ENCODING_VALUE.
+
+(*
+On calcule la valeur binaire selon un schema de Horner.
+Le calcul s'arrete à la longueur du vecteur sans vérification.
+On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient
+de la division z=2q+r avec 0<=r<=1.
+La valeur en complément à deux est calculée selon un schema de Horner
+avec Zmod2, le paramètre est la taille moins un.
+*)
+
+Definition Zmod2 := [z:Z] Cases z of
+  	|  ZERO => `0`
+ 	| ((POS p)) => Cases p of
+      		| (xI q) => (POS q)
+    		| (xO q) => (POS q)
+    		| xH => `0`
+    		end
+ 	| ((NEG p)) => Cases p of
+      		| (xI q) => `(NEG q) - 1`
+    		| (xO q) => (NEG q)
+    		| xH => `-1`
+    		end
+ 	end.
+
+Lemma double_moins_un_add_un : (p:positive) 
+	(xI p)=(double_moins_un (add_un p)).
+Proof.
+	Induction p; Simpl; Intros.
+	Rewrite H; Auto.
+
+	Trivial.
+
+	Trivial.
+Save.
+
+Lemma Zmod2_twice : (z:Z)
+	`z = (2*(Zmod2 z) + (bit_value (Zodd_bool z)))`.
+Proof.
+	Destruct z; Simpl; Intros.
+	Trivial.
+
+	Case p; Simpl; Trivial.
+
+	Case p; Simpl; Intros.
+	Case p0; Simpl; Intros.
+	Rewrite (double_moins_un_add_un p1); Trivial.
+
+	Trivial.
+
+	Trivial.
+
+	Trivial.
+
+	Trivial.
+Save.
+
+Lemma Z_to_binary : (n:nat) Z -> (Bvector n).
+Proof.
+	Induction n; Intros.
+	Exact Bnil.
+
+	Exact (Bcons (Zodd_bool H0) n0 (H (Zdiv2 H0))).
+Defined.
+
+(*
+Eval Compute in (Z_to_binary (5) `5`).
+     = (Vcons bool true (4)
+          (Vcons bool false (3)
+            (Vcons bool true (2)
+              (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))))
+     :  (Bvector (5))
+*)
+
+Lemma Z_to_two_compl : (n:nat) Z -> (Bvector (S n)).
+Proof.
+	Induction n; Intros.
+	Exact (Bcons (Zodd_bool H) (0) Bnil).
+
+	Exact (Bcons (Zodd_bool H0) (S n0) (H (Zmod2 H0))).
+Defined.
+
+(*
+Eval Compute in (Z_to_two_compl (3) `0`).
+     =  (Vcons bool false (3)
+          (Vcons bool false (2)
+            (Vcons bool false (1) (Vcons bool false (0) (Vnil bool)))))
+     :  (vector bool (4))
+
+Eval Compute in (Z_to_two_compl (3) `5`).
+     = (Vcons bool true (3)
+          (Vcons bool false (2)
+            (Vcons bool true (1) (Vcons bool false (0) (Vnil bool)))))
+     :  (vector bool (4))
+
+Eval Compute in (Z_to_two_compl (3) `-5`).
+     =  (Vcons bool true (3)
+          (Vcons bool true (2)
+            (Vcons bool false (1) (Vcons bool true (0) (Vnil bool)))))
+     :  (vector bool (4))
+*)	
+
+End ENCODING_VALUE.
+
+Section Z_BRIC_A_BRAC.
+
+(*
+Bibliotheque de lemmes utiles dans la section suivante.
+Utilise largement ZArith.
+Meriterait d'etre reecrite.
+*)
+
+Lemma binary_value_Sn : (n:nat) (b:bool) (bv : (Bvector n))
+	(binary_value (S n) (Vcons bool b n bv))=`(bit_value b) + 2*(binary_value n bv)`.
+Proof.
+	Intros; Auto.
+Save.
+
+Lemma Z_to_binary_Sn : (n:nat) (b:bool) (z:Z)
+	`z>=0`->
+	(Z_to_binary (S n) `(bit_value b) + 2*z`)=(Bcons b n (Z_to_binary n z)).
+Proof.
+	Destruct b; Destruct z; Simpl; Auto.
+	Intros. Elim H; Trivial.
+Save.
+
+Lemma binary_value_pos : (n:nat) (bv:(Bvector n))
+	`(binary_value n bv) >= 0`.
+Proof.
+	Induction bv; Intros; Simpl.
+	Omega.
+
+	Generalize H; Clear H; Case a; Case (binary_value n0 v); Simpl; Intros; 		Auto.
+	Omega.
+Save.
+
+Lemma add_un_double_moins_un_xO : (p:positive)
+	(add_un (double_moins_un p))=(xO p).
+Proof.
+	Induction p; Simpl; Intros.
+	Trivial.
+
+	Rewrite H; Trivial.
+
+	Trivial.
+Save.
+
+Lemma two_compl_value_Sn : (n:nat) (bv : (Bvector (S n))) (b:bool)
+	(two_compl_value (S n) (Bcons b (S n) bv)) =
+		`(bit_value b) + 2*(two_compl_value n bv)`.
+Proof.
+	Intros; Auto.
+Save.
+
+Lemma Z_to_two_compl_Sn : (n:nat) (b:bool) (z:Z) 
+	(Z_to_two_compl (S n) `(bit_value b) + 2*z`) =
+		(Bcons b (S n) (Z_to_two_compl n z)).
+Proof.
+	Destruct b; Destruct z; Auto.
+	Destruct p; Auto.
+	Destruct p0; Simpl; Auto.
+	Intros; Rewrite (add_un_double_moins_un_xO p1); Trivial.
+Save.
+
+Lemma Z_to_binary_Sn_z : (n:nat) (z:Z)
+	(Z_to_binary (S n) z)=(Bcons (Zodd_bool z) n (Z_to_binary n (Zdiv2 z))).
+Proof.
+	Intros; Auto.
+Save.
+
+Lemma Z_div2_value : (z:Z)
+	` z>=0 `->
+	 `(bit_value (Zodd_bool z))+2*(Zdiv2 z) = z`.
+Proof.
+	Destruct z; Auto.
+	Destruct p; Auto.
+  Intros; Elim H; Trivial.
+Save.
+
+Lemma Zdiv2_pos : (z:Z)
+	` z >= 0 ` ->
+	`(Zdiv2 z) >= 0 `.
+Proof.
+	Destruct z.
+	Auto.
+
+	Destruct p; Auto.
+	Simpl; Intros; Omega.
+
+  Intros; Elim H; Trivial.
+
+Save.
+
+Lemma Zdiv2_two_power_nat : (z:Z) (n:nat)
+	` z >= 0 ` ->
+	` z < (two_power_nat (S n)) ` ->
+	`(Zdiv2 z) < (two_power_nat n) `.
+Proof.
+	Intros.
+	Cut (Zlt (Zmult `2` (Zdiv2 z)) (Zmult `2` (two_power_nat n))); Intros.
+	Omega.
+
+	Rewrite <- two_power_nat_S.
+	Case (Zeven_odd_dec z); Intros.
+	Rewrite <- Zeven_div2; Auto.
+
+	Generalize (Zodd_div2 z H z0); Omega.
+Save.
+
+(*
+
+Lemma Z_minus_one_or_zero : (z:Z)
+	`z >= -1` ->
+	`z < 1` ->
+	{`z=-1`} + {`z=0`}.
+Proof.
+	Destruct z; Auto.
+	Destruct p; Auto.
+	Tauto.
+
+	Tauto.
+
+	Intros.
+	Right; Omega.
+
+	Destruct p.
+	Tauto.
+
+	Tauto.
+
+	Intros; Left; Omega.
+Save.
+*)
+
+Lemma Z_to_two_compl_Sn_z : (n:nat) (z:Z)
+	(Z_to_two_compl (S n) z)=(Bcons (Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z))).
+Proof.
+	Intros; Auto.
+Save.
+
+Lemma Zeven_bit_value : (z:Z)
+	(Zeven z) ->
+	`(bit_value (Zodd_bool z))=0`.
+Proof.
+	Destruct z; Unfold bit_value; Auto.
+	Destruct p; Tauto Orelse (Intros; Elim H).
+ 	Destruct p; Tauto Orelse (Intros; Elim H).
+Save.
+
+Lemma Zodd_bit_value : (z:Z)
+	(Zodd z) ->
+	`(bit_value (Zodd_bool z))=1`.
+Proof.
+	Destruct z; Unfold bit_value; Auto.
+  Intros; Elim H.
+  Destruct p; Tauto Orelse (Intros; Elim H).
+  Destruct p; Tauto Orelse (Intros; Elim H).
+Save.
+
+Lemma Zge_minus_two_power_nat_S : (n:nat) (z:Z)
+	`z >= (-(two_power_nat (S n)))`->
+	`(Zmod2 z) >= (-(two_power_nat n))`.
+Proof.
+	Intros n; Rewrite (two_power_nat_S n).
+	Intros z; Generalize (Zmod2_twice z).
+	Case (Zeven_odd_dec z); Intros.
+	Generalize (Zeven_bit_value z z0); Intros; Omega.
+
+	Generalize (Zodd_bit_value z z0); Intros; Omega.
+Save.
+
+Lemma Zlt_two_power_nat_S : (n:nat) (z:Z)
+	`z < (two_power_nat (S n))`->
+	`(Zmod2 z) < (two_power_nat n)`.
+Proof.
+	Intros n; Rewrite (two_power_nat_S n).
+	Intros z; Generalize (Zmod2_twice z).
+	Case (Zeven_odd_dec z); Intros.
+	Generalize (Zeven_bit_value z z0); Intros; Omega.
+
+	Generalize (Zodd_bit_value z z0); Intros; Omega.
+Save.
+
+End Z_BRIC_A_BRAC.
+
+Section COHERENT_VALUE.
+
+(*
+On vérifie que dans l'intervalle de définition les fonctions sont 
+réciproques l'une de l'autre.
+Elles utilisent les lemmes du bric-a-brac.
+*)
+
+Lemma binary_to_Z_to_binary : (n:nat) (bv : (Bvector n))
+	(Z_to_binary n (binary_value n bv))=bv.
+Proof.
+	Induction bv; Intros.
+	Auto.
+
+	Rewrite binary_value_Sn.
+	Rewrite Z_to_binary_Sn.
+	Rewrite H; Trivial.
+
+	Apply binary_value_pos.
+Save.
+		
+Lemma two_compl_to_Z_to_two_compl : (n:nat) (bv : (Bvector n)) (b:bool)
+	(Z_to_two_compl n (two_compl_value n (Bcons b n bv)))=
+		(Bcons b n bv).
+Proof.
+	Induction bv; Intros.
+	Case b; Auto.
+
+	Rewrite two_compl_value_Sn.
+	Rewrite Z_to_two_compl_Sn.
+	Rewrite H; Trivial.
+Save.
+
+Lemma Z_to_binary_to_Z : (n:nat) (z : Z)
+	`z >= 0 `->
+	`z < (two_power_nat n) `->
+	 (binary_value n (Z_to_binary n z))=z.
+Proof.
+	Induction n.
+	Unfold two_power_nat shift_nat; Simpl; Intros; Omega.
+
+	Intros; Rewrite Z_to_binary_Sn_z.
+	Rewrite binary_value_Sn.
+	Rewrite H.
+	Apply Z_div2_value; Auto.
+
+	Apply Zdiv2_pos; Trivial.
+
+	Apply Zdiv2_two_power_nat; Trivial.
+Save.
+
+Lemma Z_to_two_compl_to_Z : (n:nat) (z : Z)
+	`z >= -(two_power_nat n) `->
+	`z < (two_power_nat n) `->
+	(two_compl_value n (Z_to_two_compl n  z))=z.
+Proof.
+	Induction n.
+	Unfold two_power_nat shift_nat; Simpl; Intros.
+	Assert `z=-1`\/`z=0`. Omega.
+Intuition; Subst z; Trivial.
+
+	Intros; Rewrite Z_to_two_compl_Sn_z.
+	Rewrite two_compl_value_Sn.
+	Rewrite H.
+	Generalize (Zmod2_twice z); Omega.
+
+	Apply Zge_minus_two_power_nat_S; Auto.
+
+	Apply Zlt_two_power_nat_S; Auto.
+Save.
+
+End COHERENT_VALUE.
+