Imported Upstream version 8.0pl1upstream/8.0pl1

8 files changed, 1101 insertions, 0 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
new file mode 100755
index 00000000..854eb9e3
--- /dev/null
+++ b/theories/Bool/Bool.v
@@ -0,0 +1,543 @@
+(************************************************************************)
+(*  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.29.2.1 2004/07/16 19:31:01 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) :=
+  match b with
+  | true => True
+  | false => False
+  end.
+Hint Unfold Is_true: bool.
+
+Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x.
+Proof.
+  intros; rewrite H; auto with bool.
+Qed.
+
+Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x.
+Proof.
+  intros; rewrite <- H; auto with bool.
+Qed.
+
+Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
+
+(*******************)
+(** Discrimination *)
+(*******************)
+
+Lemma diff_true_false : true <> false.
+Proof.
+unfold not in |- *; intro contr; change (Is_true false) in |- *.
+elim contr; simpl in |- *; trivial with bool.
+Qed.
+Hint Resolve diff_true_false: bool v62.
+
+Lemma diff_false_true : false <> true.
+Proof.
+red in |- *; intros H; apply diff_true_false.
+symmetry  in |- *.
+assumption.
+Qed.
+Hint Resolve diff_false_true: bool v62.
+
+Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
+intros b H; rewrite H; auto with bool.
+Qed.
+Hint Resolve eq_true_false_abs: bool.
+
+Lemma not_true_is_false : forall b:bool, b <> true -> b = false.
+destruct b.
+intros.
+red in H; elim H.
+reflexivity.
+intros abs.
+reflexivity.
+Qed.
+
+Lemma not_false_is_true : forall b:bool, b <> false -> b = true.
+destruct b.
+intros.
+reflexivity.
+intro H; red in H; elim H.
+reflexivity.
+Qed.
+
+(**********************)
+(** Order on booleans *)
+(**********************)
+
+Definition leb (b1 b2:bool) :=
+  match b1 with
+  | true => b2 = true
+  | false => True
+  end.
+Hint Unfold leb: bool v62.
+
+(*************)
+(** Equality *)
+(*************)
+
+Definition eqb (b1 b2:bool) : bool :=
+  match b1, b2 with
+  | true, true => true
+  | true, false => false
+  | false, true => false
+  | false, false => true
+  end.
+
+Lemma eqb_refl : forall x:bool, Is_true (eqb x x).
+destruct x; simpl in |- *; auto with bool.
+Qed.
+
+Lemma eqb_eq : forall x y:bool, Is_true (eqb x y) -> x = y.
+destruct x; destruct y; simpl in |- *; tauto.
+Qed.
+
+Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true.
+destruct x; simpl in |- *; tauto.
+Qed.
+ 
+Lemma Is_true_eq_true2 : forall x:bool, x = true -> Is_true x.
+destruct x; simpl in |- *; auto with bool.
+Qed.
+
+Lemma eqb_subst :
+ forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
+unfold eqb in |- *.
+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 : forall b:bool, eqb b b = true.
+intro b.
+case b.
+trivial with bool.
+trivial with bool.
+Qed.
+
+Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b.
+destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
+Qed.
+
+
+(************************)
+(** Logical combinators *)
+(************************)
+ 
+Definition ifb (b1 b2 b3:bool) : bool :=
+  match b1 with
+  | true => b2
+  | false => b3
+  end.
+
+Definition andb (b1 b2:bool) : bool := ifb b1 b2 false.
+
+Definition orb (b1 b2:bool) : bool := ifb b1 true b2.
+
+Definition implb (b1 b2:bool) : bool := ifb b1 b2 true.
+
+Definition xorb (b1 b2:bool) : bool :=
+  match b1, b2 with
+  | true, true => false
+  | true, false => true
+  | false, true => true
+  | false, false => false
+  end.
+
+Definition negb (b:bool) := match b with
+                            | true => false
+                            | false => true
+                            end.
+
+Infix "||" := orb (at level 50, left associativity) : bool_scope.
+Infix "&&" := andb (at level 40, left associativity) : bool_scope.
+
+Open Scope bool_scope.
+
+Delimit Scope bool_scope with bool.
+
+Bind Scope bool_scope with bool.
+
+(**************************)
+(** Lemmas about [negb]   *)
+(**************************)
+
+Lemma negb_intro : forall b:bool, b = negb (negb b).
+Proof.
+destruct b; reflexivity.
+Qed.
+
+Lemma negb_elim : forall b:bool, negb (negb b) = b.
+Proof.
+destruct b; reflexivity.
+Qed.
+       
+Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
+Qed.
+
+Lemma negb_andb : forall b1 b2:bool, negb (b1 && b2) = negb b1 || negb b2.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
+Qed.
+
+Lemma negb_sym : forall b b':bool, b' = negb b -> b = negb b'.
+Proof.
+destruct b; destruct b'; intros; simpl in |- *; trivial with bool.
+Qed.
+
+Lemma no_fixpoint_negb : forall b:bool, negb b <> b.
+Proof.
+destruct b; simpl in |- *; intro; apply diff_true_false;
+ auto with bool.
+Qed.
+
+Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false.
+destruct b.
+trivial with bool.
+trivial with bool.
+Qed.
+ 
+Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false.
+destruct b.
+trivial with bool.
+trivial with bool.
+Qed.
+
+
+Lemma if_negb :
+ forall (A:Set) (b:bool) (x y:A),
+   (if negb b then x else y) = (if b then y else x).
+Proof.
+  destruct b; trivial.
+Qed.
+
+
+(****************************)
+(** A few lemmas about [or] *)
+(****************************)
+
+Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true.
+destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+ auto with bool.
+Qed.
+
+Lemma orb_prop2 : forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.
+destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+ auto with bool.
+Qed.
+
+Lemma orb_true_intro :
+ forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true.
+destruct b1; auto with bool.
+destruct 1; intros.
+elim diff_true_false; auto with bool.
+rewrite H; trivial with bool.
+Qed.
+Hint Resolve orb_true_intro: bool v62.
+
+Lemma orb_b_true : forall b:bool, b || true = true.
+auto with bool.
+Qed.
+Hint Resolve orb_b_true: bool v62.
+
+Lemma orb_true_b : forall b:bool, true || b = true.
+trivial with bool.
+Qed.
+
+Definition orb_true_elim :
+  forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}.
+destruct b1; simpl in |- *; auto with bool.
+Defined.
+
+Lemma orb_false_intro :
+ forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.
+intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool.
+Qed.
+Hint Resolve orb_false_intro: bool v62.
+
+Lemma orb_b_false : forall b:bool, b || false = b.
+Proof.
+  destruct b; trivial with bool.
+Qed.
+Hint Resolve orb_b_false: bool v62.
+
+Lemma orb_false_b : forall b:bool, false || b = b.
+Proof.
+  destruct b; trivial with bool.
+Qed.
+Hint Resolve orb_false_b: bool v62.
+
+Lemma orb_false_elim :
+ forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.
+Proof.
+  destruct b1.
+  intros; elim diff_true_false; auto with bool.
+  destruct b2.
+  intros; elim diff_true_false; auto with bool.
+  auto with bool.
+Qed.
+
+Lemma orb_neg_b : forall b:bool, b || negb b = true.
+Proof.
+  destruct b; reflexivity.
+Qed.
+Hint Resolve orb_neg_b: bool v62.
+
+Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1.
+destruct b1; destruct b2; reflexivity.
+Qed.
+
+Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3.
+Proof.
+  destruct b1; destruct b2; destruct b3; reflexivity.
+Qed.
+
+Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62.
+
+(*****************************)
+(** A few lemmas about [and] *)
+(*****************************)
+
+Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true.
+
+Proof.
+  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+   auto with bool.
+Qed.
+Hint Resolve andb_prop: bool v62.
+
+Definition andb_true_eq :
+  forall a b:bool, true = a && b -> true = a /\ true = b.
+Proof.
+  destruct a; destruct b; auto.
+Defined.
+
+Lemma andb_prop2 :
+ forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b.
+Proof.
+  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
+   auto with bool.
+Qed.
+Hint Resolve andb_prop2: bool v62.
+
+Lemma andb_true_intro :
+ forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+Hint Resolve andb_true_intro: bool v62.
+
+Lemma andb_true_intro2 :
+ forall b1 b2:bool, Is_true b1 -> Is_true b2 -> Is_true (b1 && b2).
+Proof.
+  destruct b1; destruct b2; simpl in |- *; tauto.
+Qed.
+Hint Resolve andb_true_intro2: bool v62.
+
+Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
+destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+
+Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false.
+destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+
+Lemma andb_b_false : forall b:bool, b && false = false.
+destruct b; auto with bool.
+Qed.
+
+Lemma andb_false_b : forall b:bool, false && b = false.
+trivial with bool.
+Qed.
+
+Lemma andb_b_true : forall b:bool, b && true = b.
+destruct b; auto with bool.
+Qed.
+
+Lemma andb_true_b : forall b:bool, true && b = b.
+trivial with bool.
+Qed.
+
+Definition andb_false_elim :
+  forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}.
+destruct b1; simpl in |- *; auto with bool.
+Defined.
+Hint Resolve andb_false_elim: bool v62.
+
+Lemma andb_neg_b : forall b:bool, b && negb b = false.
+destruct b; reflexivity.
+Qed.   
+Hint Resolve andb_neg_b: bool v62.
+
+Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1.
+destruct b1; destruct b2; reflexivity.
+Qed.
+
+Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3.
+destruct b1; destruct b2; destruct b3; reflexivity.
+Qed.
+
+Hint Resolve andb_comm andb_assoc: bool v62.
+
+(*******************************)
+(** Properties of [xorb]       *)
+(*******************************)
+
+Lemma xorb_false : forall b:bool, xorb b false = b.
+Proof.
+  destruct b; trivial.
+Qed.
+
+Lemma false_xorb : forall b:bool, xorb false b = b.
+Proof.
+  destruct b; trivial.
+Qed.
+
+Lemma xorb_true : forall b:bool, xorb b true = negb b.
+Proof.
+  trivial.
+Qed.
+
+Lemma true_xorb : forall b:bool, xorb true b = negb b.
+Proof.
+  destruct b; trivial.
+Qed.
+
+Lemma xorb_nilpotent : forall b:bool, xorb b b = false.
+Proof.
+  destruct b; trivial.
+Qed.
+
+Lemma xorb_comm : forall b b':bool, xorb b b' = xorb b' b.
+Proof.
+  destruct b; destruct b'; trivial.
+Qed.
+
+Lemma xorb_assoc :
+ forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b'').
+Proof.
+  destruct b; destruct b'; destruct b''; trivial.
+Qed.
+
+Lemma xorb_eq : forall b b':bool, xorb b b' = false -> b = b'.
+Proof.
+  destruct b; destruct b'; trivial.
+  unfold xorb in |- *. intros. rewrite H. reflexivity.
+Qed.
+
+Lemma xorb_move_l_r_1 :
+ forall 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 :
+ forall 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 :
+ forall 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 :
+ forall 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 :
+ forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3.
+destruct b1; destruct b2; destruct b3; reflexivity.
+Qed.
+
+Lemma demorgan2 :
+ forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3.
+destruct b1; destruct b2; destruct b3; reflexivity.
+Qed.
+
+Lemma demorgan3 :
+ forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3).
+destruct b1; destruct b2; destruct b3; reflexivity.
+Qed.
+
+Lemma demorgan4 :
+ forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3).
+destruct b1; destruct b2; destruct b3; reflexivity.
+Qed.
+
+Lemma absoption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
+Qed.
+
+Lemma absoption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; reflexivity.
+Qed.
+
+
+(** Misc. equalities between booleans (to be used by Auto) *)
+
+Lemma bool_1 : forall b1 b2:bool, (b1 = true <-> b2 = true) -> b1 = b2. 
+Proof. 
+ intros b1 b2; case b1; case b2; intuition.
+Qed.
+
+Lemma bool_2 : forall b1 b2:bool, b1 = b2 -> b1 = true -> b2 = true.
+Proof. 
+ intros b1 b2; case b1; case b2; intuition.
+Qed. 
+
+Lemma bool_3 : forall b:bool, negb b <> true -> b = true.
+Proof.
+  destruct b; intuition.
+Qed.
+
+Lemma bool_4 : forall b:bool, b = true -> negb b <> true.  
+Proof.
+  destruct b; intuition.
+Qed.
+
+Lemma bool_5 : forall b:bool, negb b = true -> b <> true.
+Proof.
+  destruct b; intuition.
+Qed.
+
+Lemma bool_6 : forall b:bool, b <> true -> negb b = true.  
+Proof.
+  destruct b; intuition.
+Qed.
+
+Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
new file mode 100644
index 00000000..e038b3da
--- /dev/null
+++ b/theories/Bool/BoolEq.v
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  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.4.2.1 2004/07/16 19:31:02 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 : forall x:A, true = beq x x.
+
+  Variable beq_eq : forall x y:A, true = beq x y -> x = y.
+
+  Definition beq_eq_true : forall 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 : forall 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 : forall x y:A, false = beq x y -> x <> y.
+  Proof.
+    exact
+     (fun (x y:A) (H:false = beq x y) (e:x = y) => beq_eq_not_false x y e H).
+  Defined.
+
+  Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
+  Proof.
+    intros.
+    exists (beq x y).
+    constructor.
+  Defined.
+
+  Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y.
+  Proof.
+    intros x y H.
+    symmetry  in |- *.
+    apply not_true_is_false.
+    intro.
+    apply H.
+    apply beq_eq.
+    symmetry  in |- *.
+    assumption.
+  Defined.
+
+  Definition eq_dec : forall 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/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
new file mode 100644
index 00000000..51d940cf
--- /dev/null
+++ b/theories/Bool/Bvector.v
@@ -0,0 +1,272 @@
+(************************************************************************)
+(*  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.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
+
+Require Export Bool.
+Require Export Sumbool.
+Require Import Arith.
+
+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 0
+  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
+
+Definition Vhead : forall n:nat, vector (S n) -> A.
+Proof.
+	intros n v; inversion v; exact a.
+Defined.
+
+Definition Vtail : forall n:nat, vector (S n) -> vector n.
+Proof.
+	intros n v; inversion v; exact H0.
+Defined.
+
+Definition Vlast : forall n:nat, vector (S n) -> A.
+Proof.
+	induction n as [| n f]; intro v.
+	inversion v.
+	exact a.
+
+	inversion v.
+	exact (f H0).
+Defined.
+
+Definition Vconst : forall (a:A) (n:nat), vector n.
+Proof.
+	induction n as [| n v].
+	exact Vnil.
+
+	exact (Vcons a n v).
+Defined.
+
+Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
+Proof.
+	induction n as [| n f]; intro v.
+	exact Vnil.
+
+	inversion v.
+	exact (Vcons a n (f H0)).
+Defined.
+
+Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
+Proof.
+	induction n as [| n f]; intros a v.
+	exact (Vcons a 0 v).
+
+	inversion v.
+	exact (Vcons a (S n) (f a H0)).
+Defined.
+
+Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)).
+Proof.
+	induction 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 : forall n p:nat, n > p -> vector n -> vector (n - p).
+Proof.
+	induction p as [| p f]; intros H v.
+	rewrite <- minus_n_O.
+	exact v.
+
+	apply (Vshiftout (n - S p)).
+
+rewrite minus_Sn_m.
+apply f.
+auto with *.
+exact v.
+auto with *.
+Defined.
+
+Lemma Vextend : forall n p:nat, vector n -> vector p -> vector (n + p).
+Proof.
+	induction n as [| n f]; intros p v v0.
+	simpl in |- *; exact v0.
+
+	inversion v.
+	simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
+Defined.
+
+Variable f : A -> A.
+
+Lemma Vunary : forall n:nat, vector n -> vector n.
+Proof.
+	induction 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 : forall n:nat, vector n -> vector n -> vector n.
+Proof.
+	induction 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.
+
+(* suppressed: incompatible with Coq-Art book 
+Implicit Arguments Vnil [A].
+Implicit Arguments Vcons [A n].
+*)
+
+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) {struct p} :
+ Bvector (S n) :=
+  match p with
+  | O => bv
+  | S p' => BshiftL n (BshiftL_iter n bv p') false
+  end.
+
+Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
+ Bvector (S n) :=
+  match p with
+  | O => bv
+  | S p' => BshiftRl n (BshiftRl_iter n bv p') false
+  end.
+
+Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
+ Bvector (S n) :=
+  match p with
+  | O => bv
+  | S p' => BshiftRa n (BshiftRa_iter n bv p')
+  end.
+
+End BOOLEAN_VECTORS.
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
new file mode 100755
index 00000000..1998fb8e
--- /dev/null
+++ b/theories/Bool/DecBool.v
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*  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.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Set Implicit Arguments.
+
+Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C :=
+  if H then x else y.
+
+
+Theorem ifdec_left :
+ forall (A B:Prop) (C:Set) (H:{A} + {B}),
+   ~ B -> forall x y:C, ifdec H x y = x.
+intros; case H; auto.
+intro; absurd B; trivial.
+Qed.
+
+Theorem ifdec_right :
+ forall (A B:Prop) (C:Set) (H:{A} + {B}),
+   ~ A -> forall x y:C, ifdec H x y = y.
+intros; case H; auto.
+intro; absurd A; trivial.
+Qed.
+
+Unset Implicit Arguments.
\ No newline at end of file
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
new file mode 100755
index 00000000..a00449d8
--- /dev/null
+++ b/theories/Bool/IfProp.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  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.7.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Require Import Bool.
+
+Inductive IfProp (A B:Prop) : bool -> Prop :=
+  | Iftrue : A -> IfProp A B true
+  | Iffalse : B -> IfProp A B false.
+
+Hint Resolve Iftrue Iffalse: bool v62.
+
+Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A.
+destruct 1; intros; auto with bool.
+case diff_true_false; auto with bool.
+Qed.
+
+Lemma Iffalse_inv :
+ forall (A B:Prop) (b:bool), IfProp A B b -> b = false -> B.
+destruct 1; intros; auto with bool.
+case diff_true_false; trivial with bool.
+Qed.
+
+Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A.
+intros.
+inversion H.
+assumption.
+Qed.
+
+Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B.
+intros.
+inversion H.
+assumption.
+Qed.
+
+Lemma IfProp_or : forall (A B:Prop) (b:bool), IfProp A B b -> A \/ B.
+destruct 1; auto with bool.
+Qed.
+
+Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
+destruct b; intro H.
+left; inversion H; auto with bool.
+right; inversion H; auto with bool.
+Qed.
\ No newline at end of file
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
new file mode 100644
index 00000000..8188f038
--- /dev/null
+++ b/theories/Bool/Sumbool.v
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  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.12.2.1 2004/07/16 19:31:03 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 : forall b:bool, {b = true} + {b = false}.
+Proof.
+  destruct b; auto.
+Defined.
+
+Hint Resolve sumbool_of_bool: bool.
+
+Definition bool_eq_rec :
+  forall (b:bool) (P:bool -> Set),
+    (b = true -> P true) -> (b = false -> P false) -> P b.
+destruct b; auto.
+Defined.
+
+Definition bool_eq_ind :
+  forall (b:bool) (P:bool -> Prop),
+    (b = true -> P true) -> (b = false -> P false) -> P b.
+destruct 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.
+
+Hint 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 :
+  forall 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.
+Implicit Arguments bool_of_sumbool.
\ No newline at end of file
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
new file mode 100755
index 00000000..b654e556
--- /dev/null
+++ b/theories/Bool/Zerob.v
@@ -0,0 +1,38 @@
+(************************************************************************)
+(*  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.8.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+
+Require Import Arith.
+Require Import Bool.
+
+Open Local Scope nat_scope.
+
+Definition zerob (n:nat) : bool :=
+  match n with
+  | O => true
+  | S _ => false
+  end.
+
+Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
+destruct n; [ trivial with bool | inversion 1 ].
+Qed.
+Hint Resolve zerob_true_intro: bool.
+
+Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
+destruct n; [ trivial with bool | inversion 1 ].
+Qed.
+
+Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
+destruct n; [ destruct 1; auto with bool | trivial with bool ].
+Qed.
+Hint Resolve zerob_false_intro: bool.
+
+Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
+destruct n; [ intro H; inversion H | auto with bool ].
+Qed.
\ No newline at end of file
diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex
new file mode 100644
index 00000000..22ee38aa
--- /dev/null
+++ b/theories/Bool/intro.tex
@@ -0,0 +1,16 @@
+\section{Bool}\label{Bool}
+
+The BOOL library includes the following files:
+
+\begin{itemize}
+
+\item {\tt Bool.v} defines standard operations on booleans and states
+  and proves simple facts on them.
+\item {\tt IfProp.v} defines a disjunction which contains its proof
+  and states its properties.
+\item {\tt Zerob.v} defines the test against 0 on natural numbers and
+  states and proves properties of it.
+\item {\tt Orb.v} states and proves facts on the boolean or.
+\item {\tt DecBool.v} defines a conditional from a proof of
+  decidability and states its properties.
+\end{itemize}