7 files changed, 1071 insertions, 0 deletions

diff --git a/theories7/Bool/Bool.v b/theories7/Bool/Bool.v
new file mode 100755
index 00000000..cd75cf30
--- /dev/null
+++ b/theories7/Bool/Bool.v
@@ -0,0 +1,544 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Bool.v,v 1.2.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+(** Booleans  *)
+
+(** The type [bool] is defined in the prelude as
+    [Inductive bool : Set := true : bool | false : bool] *)
+
+(** Interpretation of booleans as Proposition *)
+Definition Is_true := [b:bool](Cases b of
+                                 true  => True
+                               | false => False
+                               end).
+Hints Unfold Is_true : bool.
+
+Lemma Is_true_eq_left : (x:bool)x=true -> (Is_true x).
+Proof.
+  Intros; Rewrite H; Auto with bool.
+Qed.
+
+Lemma Is_true_eq_right : (x:bool)true=x -> (Is_true x).
+Proof.
+  Intros; Rewrite <- H; Auto with bool.
+Qed.
+
+Hints Immediate Is_true_eq_right Is_true_eq_left : bool.
+
+(*******************)
+(** Discrimination *)
+(*******************)
+
+Lemma diff_true_false : ~true=false.
+Proof.
+Unfold not; Intro contr; Change (Is_true false).
+Elim contr; Simpl; Trivial with bool.
+Qed.
+Hints Resolve diff_true_false : bool v62.
+
+Lemma diff_false_true : ~false=true.
+Proof.
+Red; Intros H; Apply diff_true_false.
+Symmetry.
+Assumption.
+Qed.
+Hints Resolve diff_false_true : bool v62.
+
+Lemma eq_true_false_abs : (b:bool)(b=true)->(b=false)->False.
+Intros b H; Rewrite H; Auto with bool.
+Qed.
+Hints Resolve eq_true_false_abs : bool.
+
+Lemma not_true_is_false : (b:bool)~b=true->b=false.
+NewDestruct b.
+Intros.
+Red in H; Elim H.
+Reflexivity.
+Intros abs.
+Reflexivity.
+Qed.
+
+Lemma not_false_is_true : (b:bool)~b=false->b=true.
+NewDestruct b.
+Intros.
+Reflexivity.
+Intro H; Red in H; Elim H.
+Reflexivity.
+Qed.
+
+(**********************)
+(** Order on booleans *)
+(**********************)
+
+Definition leb := [b1,b2:bool]
+  Cases b1 of 
+  | true => b2=true
+  | false => True 
+  end.
+Hints Unfold leb : bool v62.
+
+(*************)
+(** Equality *)
+(*************)
+
+Definition eqb : bool->bool->bool :=
+ [b1,b2:bool]
+    Cases b1 b2 of
+      true  true  => true
+    | true  false => false
+    | false true  => false
+    | false false => true
+    end.
+
+Lemma eqb_refl : (x:bool)(Is_true (eqb x x)).
+NewDestruct x; Simpl; Auto with bool.
+Qed.
+
+Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y.
+NewDestruct x; NewDestruct y; Simpl; Tauto.
+Qed.
+
+Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true.
+NewDestruct x; Simpl; Tauto.
+Qed.
+ 
+Lemma Is_true_eq_true2 : (x:bool)  x=true -> (Is_true x).
+NewDestruct x; Simpl; Auto with bool.
+Qed.
+
+Lemma eqb_subst : 
+  (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2).
+Unfold eqb .
+Intros P b1.
+Intros b2.
+Case b1.
+Case b2.
+Trivial with bool.
+Intros H.
+Inversion_clear H.
+Case b2.
+Intros H.
+Inversion_clear H.
+Trivial with bool.
+Qed.
+
+Lemma eqb_reflx : (b:bool)(eqb b b)=true.
+Intro b.
+Case b.
+Trivial with bool.
+Trivial with bool.
+Qed.
+
+Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b.
+NewDestruct a; NewDestruct b; Simpl; Intro;
+  Discriminate H Orelse Reflexivity.
+Qed.
+
+
+(************************)
+(** Logical combinators *)
+(************************)
+ 
+Definition ifb : bool -> bool -> bool -> bool
+     := [b1,b2,b3:bool](Cases b1 of true => b2 | false => b3 end).
+
+Definition andb : bool -> bool -> bool
+     := [b1,b2:bool](ifb b1 b2 false).
+
+Definition orb : bool -> bool -> bool
+     := [b1,b2:bool](ifb b1 true b2).
+
+Definition implb : bool -> bool -> bool
+     := [b1,b2:bool](ifb b1 b2 true).
+
+Definition xorb :  bool -> bool -> bool
+     := [b1,b2:bool]
+    Cases b1 b2 of
+      true  true  => false
+    | true  false => true
+    | false true  => true
+    | false false => false
+    end.
+
+Definition negb := [b:bool]Cases b of
+                             true  => false
+                           | false => true
+                           end.
+
+Infix "||" orb  (at level 4, left associativity) : bool_scope.
+Infix "&&" andb (at level 3, no associativity) : bool_scope
+  V8only (at level 40, left associativity).
+
+Open Scope bool_scope.
+
+Delimits Scope bool_scope with bool.
+
+Bind Scope bool_scope with bool.
+
+(**************************)
+(** Lemmas about [negb]   *)
+(**************************)
+
+Lemma negb_intro : (b:bool)b=(negb (negb b)).
+Proof.
+NewDestruct b; Reflexivity.
+Qed.
+
+Lemma negb_elim : (b:bool)(negb (negb b))=b.
+Proof.
+NewDestruct b; Reflexivity.
+Qed.
+       
+Lemma negb_orb : (b1,b2:bool)
+  (negb (orb b1 b2)) = (andb (negb b1) (negb b2)).
+Proof.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+Qed.
+
+Lemma negb_andb : (b1,b2:bool)
+  (negb (andb b1 b2)) = (orb (negb b1) (negb b2)).
+Proof.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+Qed.
+
+Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')).
+Proof.
+NewDestruct b; NewDestruct b'; Intros; Simpl; Trivial with bool.
+Qed.
+
+Lemma no_fixpoint_negb : (b:bool)~(negb b)=b.
+Proof.
+NewDestruct b; Simpl; Intro; Apply diff_true_false; Auto with bool.
+Qed.
+
+Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false.
+NewDestruct b.
+Trivial with bool.
+Trivial with bool.
+Qed.
+ 
+Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false.
+NewDestruct b.
+Trivial with bool.
+Trivial with bool.
+Qed.
+
+
+Lemma if_negb : (A:Set) (b:bool) (x,y:A) (if (negb b) then x else y)=(if b then y else x).
+Proof.
+  NewDestruct b;Trivial.
+Qed.
+
+
+(****************************)
+(** A few lemmas about [or] *)
+(****************************)
+
+Lemma orb_prop : 
+  (a,b:bool)(orb a b)=true -> (a = true)\/(b = true).
+NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+Qed.
+
+Lemma orb_prop2 : 
+  (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b).
+NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
+Qed.
+
+Lemma orb_true_intro 
+    : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true.
+NewDestruct b1; Auto with bool.
+NewDestruct 1; Intros.
+Elim diff_true_false; Auto with bool.
+Rewrite H; Trivial with bool.
+Qed.
+Hints Resolve orb_true_intro : bool v62.
+
+Lemma orb_b_true : (b:bool)(orb b true)=true.
+Auto with bool.
+Qed.
+Hints Resolve orb_b_true : bool v62.
+
+Lemma orb_true_b : (b:bool)(orb true b)=true.
+Trivial with bool.
+Qed.
+
+Definition orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
+NewDestruct b1; Simpl; Auto with bool.
+Defined.
+
+Lemma orb_false_intro 
+    : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false.
+Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool.
+Qed.
+Hints Resolve orb_false_intro : bool v62.
+
+Lemma orb_b_false : (b:bool)(orb b false)=b.
+Proof.
+  NewDestruct b; Trivial with bool.
+Qed.
+Hints Resolve orb_b_false : bool v62.
+
+Lemma orb_false_b : (b:bool)(orb false b)=b.
+Proof.
+  NewDestruct b; Trivial with bool.
+Qed.
+Hints Resolve orb_false_b : bool v62.
+
+Lemma orb_false_elim : 
+    (b1,b2:bool)(orb b1 b2)=false -> (b1=false)/\(b2=false).
+Proof.
+  NewDestruct b1.
+  Intros; Elim diff_true_false; Auto with bool.
+  NewDestruct b2.
+  Intros; Elim diff_true_false; Auto with bool.
+  Auto with bool.
+Qed.
+
+Lemma orb_neg_b :
+  (b:bool)(orb b (negb b))=true.
+Proof.
+  NewDestruct b; Reflexivity.
+Qed.
+Hints Resolve orb_neg_b : bool v62.
+
+Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1).
+NewDestruct b1; NewDestruct b2; Reflexivity.
+Qed.
+
+Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3).
+Proof.
+  NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Qed.
+
+Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62.
+
+(*****************************)
+(** A few lemmas about [and] *)
+(*****************************)
+
+Lemma andb_prop : 
+  (a,b:bool)(andb a b) = true -> (a = true)/\(b = true).
+
+Proof.
+  NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H);
+  Auto with bool.
+Qed.
+Hints Resolve andb_prop : bool v62.
+
+Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b.
+Proof.
+  NewDestruct a; NewDestruct b; Auto.
+Defined.
+
+Lemma andb_prop2 : 
+  (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b).
+Proof.
+  NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H);
+  Auto with bool.
+Qed.
+Hints Resolve andb_prop2 : bool v62.
+
+Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true.
+Proof.
+  NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
+Qed.
+Hints Resolve andb_true_intro : bool v62.
+
+Lemma andb_true_intro2 : 
+  (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)).
+Proof.
+  NewDestruct b1; NewDestruct b2; Simpl; Tauto.
+Qed.
+Hints Resolve andb_true_intro2 : bool v62.
+
+Lemma andb_false_intro1 
+    : (b1,b2:bool)(b1=false)->(andb b1 b2)=false.
+NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
+Qed.
+
+Lemma andb_false_intro2 
+    : (b1,b2:bool)(b2=false)->(andb b1 b2)=false.
+NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
+Qed.
+
+Lemma andb_b_false : (b:bool)(andb b false)=false.
+NewDestruct b; Auto with bool.
+Qed.
+
+Lemma andb_false_b : (b:bool)(andb false b)=false.
+Trivial with bool.
+Qed.
+
+Lemma andb_b_true : (b:bool)(andb b true)=b.
+NewDestruct b; Auto with bool.
+Qed.
+
+Lemma andb_true_b : (b:bool)(andb true b)=b.
+Trivial with bool.
+Qed.
+
+Definition andb_false_elim : 
+    (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}.
+NewDestruct b1; Simpl; Auto with bool.
+Defined.
+Hints Resolve andb_false_elim : bool v62.
+
+Lemma andb_neg_b :
+   (b:bool)(andb b (negb b))=false.
+NewDestruct b; Reflexivity.
+Qed.   
+Hints Resolve andb_neg_b : bool v62.
+
+Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1).
+NewDestruct b1; NewDestruct b2; Reflexivity.
+Qed.
+
+Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3).
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Qed.
+
+Hints Resolve andb_sym andb_assoc : bool v62.
+
+(*******************************)
+(** Properties of [xorb]       *)
+(*******************************)
+
+Lemma xorb_false : (b:bool) (xorb b false)=b.
+Proof.
+  NewDestruct b; Trivial.
+Qed.
+
+Lemma false_xorb : (b:bool) (xorb false b)=b.
+Proof.
+  NewDestruct b; Trivial.
+Qed.
+
+Lemma xorb_true : (b:bool) (xorb b true)=(negb b).
+Proof.
+  Trivial.
+Qed.
+
+Lemma true_xorb : (b:bool) (xorb true b)=(negb b).
+Proof.
+  NewDestruct b; Trivial.
+Qed.
+
+Lemma xorb_nilpotent : (b:bool) (xorb b b)=false.
+Proof.
+  NewDestruct b; Trivial.
+Qed.
+
+Lemma xorb_comm : (b,b':bool) (xorb b b')=(xorb b' b).
+Proof.
+  NewDestruct b; NewDestruct b'; Trivial.
+Qed.
+
+Lemma xorb_assoc : (b,b',b'':bool) (xorb (xorb b b') b'')=(xorb b (xorb b' b'')).
+Proof.
+  NewDestruct b; NewDestruct b'; NewDestruct b''; Trivial.
+Qed.
+
+Lemma xorb_eq : (b,b':bool) (xorb b b')=false -> b=b'.
+Proof.
+  NewDestruct b; NewDestruct b'; Trivial.
+  Unfold xorb. Intros. Rewrite H. Reflexivity.
+Qed.
+
+Lemma xorb_move_l_r_1 : (b,b',b'':bool) (xorb b b')=b'' -> b'=(xorb b b'').
+Proof.
+  Intros. Rewrite <- (false_xorb b'). Rewrite <- (xorb_nilpotent b). Rewrite xorb_assoc.
+  Rewrite H. Reflexivity.
+Qed.
+
+Lemma xorb_move_l_r_2 : (b,b',b'':bool) (xorb b b')=b'' -> b=(xorb b'' b').
+Proof.
+  Intros. Rewrite xorb_comm in H. Rewrite (xorb_move_l_r_1 b' b b'' H). Apply xorb_comm.
+Qed.
+
+Lemma xorb_move_r_l_1 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b' b)=b''.
+Proof.
+  Intros. Rewrite H. Rewrite <- xorb_assoc. Rewrite xorb_nilpotent. Apply false_xorb.
+Qed.
+
+Lemma xorb_move_r_l_2 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b b'')=b'.
+Proof.
+  Intros. Rewrite H. Rewrite xorb_assoc. Rewrite xorb_nilpotent. Apply xorb_false.
+Qed.
+
+(*******************************)
+(** De Morgan's law            *)
+(*******************************)
+
+Lemma demorgan1 : (b1,b2,b3:bool)
+  (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)).
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Qed.
+
+Lemma demorgan2 : (b1,b2,b3:bool)
+  (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)).
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Qed.
+
+Lemma demorgan3 : (b1,b2,b3:bool)
+  (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)).
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Qed.
+
+Lemma demorgan4 : (b1,b2,b3:bool)
+  (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)).
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
+Qed.
+
+Lemma absoption_andb : (b1,b2:bool)
+  (andb b1 (orb b1 b2)) = b1.
+Proof.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+Qed.
+
+Lemma absoption_orb : (b1,b2:bool)
+  (orb b1 (andb b1 b2)) = b1.
+Proof.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
+Qed.
+
+
+(** Misc. equalities between booleans (to be used by Auto) *)
+
+Lemma bool_1 : (b1,b2:bool)(b1=true <-> b2=true) -> b1=b2. 
+Proof. 
+ Intros b1 b2; Case b1; Case b2; Intuition.
+Qed.
+
+Lemma bool_2 : (b1,b2:bool)b1=b2 -> b1=true -> b2=true.
+Proof. 
+ Intros b1 b2; Case b1; Case b2; Intuition.
+Qed. 
+
+Lemma bool_3 : (b:bool) ~(negb b)=true -> b=true.
+Proof.
+  NewDestruct b; Intuition.
+Qed.
+
+Lemma bool_4 : (b:bool) b=true -> ~(negb b)=true.  
+Proof.
+  NewDestruct b; Intuition.
+Qed.
+
+Lemma bool_5 : (b:bool) (negb b)=true -> ~b=true.
+Proof.
+  NewDestruct b; Intuition.
+Qed.
+
+Lemma bool_6 : (b:bool) ~b=true -> (negb b)=true.  
+Proof.
+  NewDestruct b; Intuition.
+Qed.
+
+Hints Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
diff --git a/theories7/Bool/BoolEq.v b/theories7/Bool/BoolEq.v
new file mode 100644
index 00000000..b670dbdd
--- /dev/null
+++ b/theories7/Bool/BoolEq.v
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: BoolEq.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+(* Cuihtlauac Alvarado - octobre 2000 *)
+
+(** Properties of a boolean equality   *)
+
+
+Require Export Bool.
+
+Section Bool_eq_dec.
+
+  Variable A : Set.
+
+  Variable beq : A -> A -> bool.
+
+  Variable beq_refl : (x:A)true=(beq x x).
+
+  Variable beq_eq : (x,y:A)true=(beq x y)->x=y.
+
+  Definition beq_eq_true : (x,y:A)x=y->true=(beq x y).
+  Proof.
+    Intros x y H.
+    Case H.
+    Apply beq_refl.
+  Defined.
+
+  Definition beq_eq_not_false : (x,y:A)x=y->~false=(beq x y).
+  Proof.
+    Intros x y e.
+    Rewrite <- beq_eq_true; Trivial; Discriminate.
+  Defined.
+
+  Definition beq_false_not_eq : (x,y:A)false=(beq x y)->~x=y.
+  Proof.
+    Exact [x,y:A; H:(false=(beq x y)); e:(x=y)](beq_eq_not_false x y e H).
+  Defined.
+
+  Definition exists_beq_eq : (x,y:A){b:bool | b=(beq x y)}.
+  Proof.
+    Intros.
+    Exists (beq x y).
+    Constructor.
+  Defined.
+
+  Definition not_eq_false_beq : (x,y:A)~x=y->false=(beq x y).
+  Proof.
+    Intros x y H.
+    Symmetry.
+    Apply not_true_is_false.
+    Intro.
+    Apply H.
+    Apply beq_eq.
+    Symmetry.
+    Assumption.
+  Defined.
+
+  Definition eq_dec : (x,y:A){x=y}+{~x=y}.
+  Proof.
+    Intros x y; Case (exists_beq_eq x y).
+    Intros b; Case b; Intro H.
+      Left; Apply beq_eq; Assumption.
+      Right; Apply beq_false_not_eq; Assumption.
+  Defined.
+
+End Bool_eq_dec.
diff --git a/theories7/Bool/Bvector.v b/theories7/Bool/Bvector.v
new file mode 100644
index 00000000..e6545381
--- /dev/null
+++ b/theories7/Bool/Bvector.v
@@ -0,0 +1,266 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Bvector.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
+
+Require Export Bool.
+Require Export Sumbool.
+Require Arith.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
+
+(*  
+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 n v; Inversion v; Exact a.
+Defined.
+
+Definition Vtail : (n:nat) (vector (S n)) -> (vector n).
+Proof.
+	Intros n v; Inversion v; Exact H0.
+Defined.
+
+Definition Vlast : (n:nat) (vector (S n)) -> A.
+Proof.
+	NewInduction n as [|n f]; Intro v.
+	Inversion v.
+	Exact a.
+
+	Inversion v.
+	Exact (f H0).
+Defined.
+
+Definition Vconst : (a:A) (n:nat) (vector n).
+Proof.
+	NewInduction n as [|n v].
+	Exact Vnil.
+
+	Exact (Vcons a n v).
+Defined.
+
+Lemma Vshiftout : (n:nat) (vector (S n)) -> (vector n).
+Proof.
+	NewInduction n as [|n f]; Intro v.
+	Exact Vnil.
+
+	Inversion v.
+	Exact (Vcons a n (f H0)).
+Defined.
+
+Lemma Vshiftin : (n:nat) A -> (vector n) -> (vector (S n)).
+Proof.
+	NewInduction n as [|n f]; Intros a v.
+	Exact (Vcons a O v).
+
+	Inversion v.
+	Exact (Vcons a (S n) (f a H0)).
+Defined.
+
+Lemma Vshiftrepeat : (n:nat) (vector (S n)) -> (vector (S (S n))).
+Proof.
+	NewInduction n as [|n f]; Intro v.
+	Inversion v.
+	Exact (Vcons a (1) v).
+
+	Inversion v.
+	Exact (Vcons a (S (S n)) (f H0)).
+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.
+	NewInduction p as [|p f]; Intros H v.
+	Rewrite <- minus_n_O.
+	Exact v.
+
+	Apply (Vshiftout (minus n (S p))).
+
+Rewrite minus_Sn_m.
+Apply f.
+Auto with *.
+Exact v.
+Auto with *.
+Defined.
+
+Lemma Vextend : (n,p:nat) (vector n) ->  (vector p) -> (vector (plus n p)).
+Proof.
+	NewInduction n as [|n f]; Intros p v v0.
+	Simpl; Exact v0.
+
+	Inversion v.
+	Simpl; Exact (Vcons a (plus n p) (f p H0 v0)).
+Defined.
+
+Variable f : A -> A.
+
+Lemma Vunary : (n:nat)(vector n)->(vector n).
+Proof.
+	NewInduction n as [|n g]; Intro v.
+	Exact Vnil.
+
+	Inversion v.
+	Exact (Vcons (f a) n (g H0)).
+Defined.
+
+Variable g : A -> A -> A.
+
+Lemma Vbinary : (n:nat)(vector n)->(vector n)->(vector n).
+Proof.
+	NewInduction n as [|n h]; Intros v v0.
+	Exact Vnil.
+
+	Inversion v; Inversion v0.
+	Exact (Vcons (g a a0) n (h H0 H2)).
+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/theories7/Bool/DecBool.v b/theories7/Bool/DecBool.v
new file mode 100755
index 00000000..c22cd032
--- /dev/null
+++ b/theories7/Bool/DecBool.v
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: DecBool.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
+   := [A,B,C,H,x,y]if H then [_]x else [_]y.
+
+
+Theorem ifdec_left : (A,B:Prop)(C:Set)(H:{A}+{B})~B->(x,y:C)(ifdec H x y)=x.
+Intros; Case H; Auto.
+Intro; Absurd B; Trivial.
+Qed.
+
+Theorem ifdec_right : (A,B:Prop)(C:Set)(H:{A}+{B})~A->(x,y:C)(ifdec H x y)=y.
+Intros; Case H; Auto.
+Intro; Absurd A; Trivial.
+Qed.
+
+Unset Implicit Arguments.
diff --git a/theories7/Bool/IfProp.v b/theories7/Bool/IfProp.v
new file mode 100755
index 00000000..bcfa4be3
--- /dev/null
+++ b/theories7/Bool/IfProp.v
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: IfProp.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+Require Bool.
+
+Inductive IfProp [A,B:Prop] : bool-> Prop 
+  := Iftrue  : A -> (IfProp A B true)
+  |  Iffalse : B -> (IfProp A B false).
+
+Hints Resolve Iftrue Iffalse : bool v62.
+
+Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
+NewDestruct 1; Intros; Auto with bool.
+Case diff_true_false; Auto with bool.
+Qed.
+
+Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
+NewDestruct 1; Intros; Auto with bool.
+Case diff_true_false; Trivial with bool.
+Qed.
+
+Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A.
+Intros.
+Inversion H.
+Assumption.
+Qed.
+
+Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B.
+Intros.
+Inversion H.
+Assumption.
+Qed.
+
+Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
+NewDestruct 1; Auto with bool.
+Qed.
+
+Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
+NewDestruct b; Intro H.
+Left; Inversion H; Auto with bool.
+Right; Inversion H; Auto with bool.
+Qed.
diff --git a/theories7/Bool/Sumbool.v b/theories7/Bool/Sumbool.v
new file mode 100644
index 00000000..8d55cbb6
--- /dev/null
+++ b/theories7/Bool/Sumbool.v
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Sumbool.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+(** Here are collected some results about the type sumbool (see INIT/Specif.v)
+   [sumbool A B], which is written [{A}+{B}], is the informative
+   disjunction "A or B", where A and B are logical propositions.
+   Its extraction is isomorphic to the type of booleans. *)
+
+(** A boolean is either [true] or [false], and this is decidable *)
+
+Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}.
+Proof.
+  NewDestruct b; Auto.
+Defined.
+
+Hints Resolve sumbool_of_bool : bool.
+
+Definition bool_eq_rec : (b:bool)(P:bool->Set)
+                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
+NewDestruct b; Auto.
+Defined.
+
+Definition bool_eq_ind : (b:bool)(P:bool->Prop)
+                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
+NewDestruct b; Auto.
+Defined.
+
+
+(*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
+
+(** Logic connectives on type [sumbool] *)
+
+Section connectives.
+
+Variables A,B,C,D : Prop.
+
+Hypothesis H1 : {A}+{B}.
+Hypothesis H2 : {C}+{D}.
+
+Definition sumbool_and : {A/\C}+{B\/D}.
+Proof.
+Case H1; Case H2; Auto.
+Defined.
+
+Definition sumbool_or : {A\/C}+{B/\D}.
+Proof.
+Case H1; Case H2; Auto.
+Defined.
+
+Definition sumbool_not : {B}+{A}.
+Proof.
+Case H1; Auto.
+Defined.
+
+End connectives.
+
+Hints Resolve sumbool_and sumbool_or sumbool_not : core.
+
+
+(** Any decidability function in type [sumbool] can be turned into a function
+    returning a boolean with the corresponding specification: *)
+
+Definition bool_of_sumbool : 
+  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
+Proof.
+Intros A B H.
+Elim H; [ Intro; Exists true; Assumption
+        | Intro; Exists false; Assumption ].
+Defined.
+Implicits bool_of_sumbool.
diff --git a/theories7/Bool/Zerob.v b/theories7/Bool/Zerob.v
new file mode 100755
index 00000000..24e48c28
--- /dev/null
+++ b/theories7/Bool/Zerob.v
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Zerob.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+Require Arith.
+Require Bool.
+
+V7only [Import nat_scope.].
+Open Local Scope nat_scope.
+
+Definition zerob : nat->bool 
+      := [n:nat]Cases n of O => true | (S _) => false end.
+
+Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true.
+NewDestruct n; [Trivial with bool | Inversion 1].
+Qed.
+Hints Resolve zerob_true_intro : bool.
+
+Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O).
+NewDestruct n; [Trivial with bool | Inversion 1].
+Qed.
+
+Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false.
+NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool].
+Qed.
+Hints Resolve zerob_false_intro : bool.
+
+Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O).
+NewDestruct n; [Intro H; Inversion H | Auto with bool].
+Qed.