Imported Upstream snapshot 8.3~beta0+13298

8 files changed, 271 insertions, 206 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 47b9fc83..7f54efa3 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -6,12 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Bool.v 10812 2008-04-17 16:42:37Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** The type [bool] is defined in the prelude as
     [Inductive bool : Set := true : bool | false : bool] *)
 
+(** Most of the lemmas in this file are trivial after breaking all booleans *)
+
+Ltac destr_bool :=
+ intros; destruct_all bool; simpl in *; trivial; try discriminate.
+
 (** Interpretation of booleans as propositions *)
+
 Definition Is_true (b:bool) :=
   match b with
     | true => True
@@ -33,42 +39,40 @@ Defined.
 
 Lemma diff_true_false : true <> false.
 Proof.
-  unfold not in |- *; intro contr; change (Is_true false) in |- *.
-  elim contr; simpl in |- *; trivial.
+  discriminate.
 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.
+Proof.
+  discriminate.
 Qed.
 Hint Resolve diff_false_true : bool v62.
 Hint Extern 1 (false <> true) => exact diff_false_true.
 
 Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
 Proof.
-  intros b H; rewrite H; auto with bool.
+  destr_bool.
 Qed.
 
 Lemma not_true_is_false : forall b:bool, b <> true -> b = false.
 Proof.
-  destruct b.
-  intros.
-  red in H; elim H.
-  reflexivity.
-  intros abs.
-  reflexivity.
+  destr_bool; intuition.
 Qed.
 
 Lemma not_false_is_true : forall b:bool, b <> false -> b = true.
 Proof.
-  destruct b.
-  intros.
-  reflexivity.
-  intro H; red in H; elim H.
-  reflexivity.
+  destr_bool; intuition.
+Qed.
+
+Lemma not_true_iff_false : forall b, b <> true <-> b = false.
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma not_false_iff_true : forall b, b <> false <-> b = true.
+Proof.
+  destr_bool; intuition.
 Qed.
 
 (**********************)
@@ -82,6 +86,11 @@ Definition leb (b1 b2:bool) :=
   end.
 Hint Unfold leb: bool v62.
 
+Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true.
+Proof.
+  destr_bool; intuition.
+Qed.
+
 (* Infix "<=" := leb : bool_scope. *)
 
 (*************)
@@ -99,37 +108,33 @@ Definition eqb (b1 b2:bool) : bool :=
 Lemma eqb_subst :
   forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
 Proof.
-  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.
+  destr_bool.
 Qed.
 
 Lemma eqb_reflx : forall b:bool, eqb b b = true.
 Proof.
-  intro b.
-  case b.
-  trivial with bool.
-  trivial with bool.
+  destr_bool.
 Qed.
 
 Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b.
 Proof.
-  destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
+  destr_bool.
+Qed.
+
+Lemma eqb_true_iff : forall a b:bool, eqb a b = true <-> a = b.
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma eqb_false_iff : forall a b:bool, eqb a b = false <-> a <> b.
+Proof.
+  destr_bool; intuition.
 Qed.
 
 (************************)
 (** * A synonym of [if] on [bool] *)
 (************************)
- 
+
 Definition ifb (b1 b2 b3:bool) : bool :=
   match b1 with
     | true => b2
@@ -144,12 +149,12 @@ Open Scope bool_scope.
 
 Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; reflexivity.
+  destr_bool.
 Qed.
 
 Lemma negb_andb : forall b1 b2:bool, negb (b1 && b2) = negb b1 || negb b2.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; reflexivity.
+  destr_bool.
 Qed.
 
 (********************************)
@@ -158,12 +163,12 @@ Qed.
 
 Lemma negb_involutive : forall b:bool, negb (negb b) = b.
 Proof.
-  destruct b; reflexivity.
+  destr_bool.
 Qed.
 
 Lemma negb_involutive_reverse : forall b:bool, b = negb (negb b).
 Proof.
-  destruct b; reflexivity.
+  destr_bool.
 Qed.
 
 Notation negb_elim := negb_involutive (only parsing).
@@ -171,35 +176,39 @@ Notation negb_intro := negb_involutive_reverse (only parsing).
 
 Lemma negb_sym : forall b b':bool, b' = negb b -> b = negb b'.
 Proof.
-  destruct b; destruct b'; intros; simpl in |- *; trivial with bool.
+  destr_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.
+  destr_bool.
 Qed.
 
 Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false.
 Proof.
-  destruct b.
-  trivial with bool.
-  trivial with bool.
+  destr_bool.
 Qed.
- 
+
 Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false.
 Proof.
-  destruct b.
-  trivial with bool.
-  trivial with bool.
+  destr_bool.
 Qed.
 
-
 Lemma if_negb :
   forall (A:Type) (b:bool) (x y:A),
     (if negb b then x else y) = (if b then y else x).
 Proof.
-  destruct b; trivial.
+  destr_bool.
+Qed.
+
+Lemma negb_true_iff : forall b, negb b = true <-> b = false.
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma negb_false_iff : forall b, negb b = false <-> b = true.
+Proof.
+  destr_bool; intuition.
 Qed.
 
 
@@ -207,46 +216,60 @@ Qed.
 (** * Properties of [orb]     *)
 (********************************)
 
+Lemma orb_true_iff :
+  forall b1 b2, b1 || b2 = true <-> b1 = true \/ b2 = true.
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma orb_false_iff :
+  forall b1 b2, b1 || b2 = false <-> b1 = false /\ b2 = false.
+Proof.
+  destr_bool; intuition.
+Qed.
+
 Lemma orb_true_elim :
   forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}.
 Proof.
-  destruct b1; simpl in |- *; auto with bool.
+  destruct b1; simpl; auto.
 Defined.
 
 Lemma orb_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.
+ intros; apply orb_true_iff; trivial.
 Qed.
 
 Lemma orb_true_intro :
   forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true.
 Proof.
-  destruct b1; auto with bool.
-  destruct 1; intros.
-  elim diff_true_false; auto with bool.
-  rewrite H; trivial with bool.
+ intros; apply orb_true_iff; trivial.
 Qed.
 Hint Resolve orb_true_intro: bool v62.
 
 Lemma orb_false_intro :
   forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.
 Proof.
-  intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool.
+ intros. subst. reflexivity.
 Qed.
 Hint Resolve orb_false_intro: bool v62.
 
+Lemma orb_false_elim :
+  forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.
+Proof.
+  intros. apply orb_false_iff; trivial.
+Qed.
+
 (** [true] is a zero for [orb] *)
 
 Lemma orb_true_r : forall b:bool, b || true = true.
 Proof.
-  auto with bool.
+  destr_bool.
 Qed.
 Hint Resolve orb_true_r: bool v62.
 
 Lemma orb_true_l : forall b:bool, true || b = true.
 Proof.
-  trivial with bool.
+  reflexivity.
 Qed.
 
 Notation orb_b_true := orb_true_r (only parsing).
@@ -256,34 +279,24 @@ Notation orb_true_b := orb_true_l (only parsing).
 
 Lemma orb_false_r : forall b:bool, b || false = b.
 Proof.
-  destruct b; trivial with bool.
+  destr_bool.
 Qed.
 Hint Resolve orb_false_r: bool v62.
 
 Lemma orb_false_l : forall b:bool, false || b = b.
 Proof.
-  destruct b; trivial with bool.
+  destr_bool.
 Qed.
 Hint Resolve orb_false_l: bool v62.
 
 Notation orb_b_false := orb_false_r (only parsing).
 Notation orb_false_b := orb_false_l (only parsing).
 
-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.
-
 (** Complementation *)
 
 Lemma orb_negb_r : forall b:bool, b || negb b = true.
 Proof.
-  destruct b; reflexivity.
+  destr_bool.
 Qed.
 Hint Resolve orb_negb_r: bool v62.
 
@@ -293,14 +306,14 @@ Notation orb_neg_b := orb_negb_r (only parsing).
 
 Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1.
 Proof.
-  destruct b1; destruct b2; reflexivity.
+  destr_bool.
 Qed.
 
 (** Associativity *)
 
 Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3.
 Proof.
-  destruct b1; destruct b2; destruct b3; reflexivity.
+  destr_bool.
 Qed.
 Hint Resolve orb_comm orb_assoc: bool v62.
 
@@ -308,38 +321,44 @@ Hint Resolve orb_comm orb_assoc: bool v62.
 (** * Properties of [andb]     *)
 (*******************************)
 
-Lemma andb_true_iff : 
+Lemma andb_true_iff :
   forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true.
 Proof.
- destruct b1; destruct b2; intuition.
+  destr_bool; intuition.
+Qed.
+
+Lemma andb_false_iff :
+  forall b1 b2:bool, b1 && b2 = false <-> b1 = false \/ b2 = false.
+Proof.
+  destr_bool; intuition.
 Qed.
 
 Lemma andb_true_eq :
   forall a b:bool, true = a && b -> true = a /\ true = b.
 Proof.
-  destruct a; destruct b; auto.
+  destr_bool. auto.
 Defined.
 
 Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+  intros. apply andb_false_iff. auto.
 Qed.
 
 Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+  intros. apply andb_false_iff. auto.
 Qed.
 
 (** [false] is a zero for [andb] *)
 
 Lemma andb_false_r : forall b:bool, b && false = false.
 Proof.
-  destruct b; auto with bool.
+  destr_bool.
 Qed.
 
 Lemma andb_false_l : forall b:bool, false && b = false.
 Proof.
-  trivial with bool.
+  reflexivity.
 Qed.
 
 Notation andb_b_false := andb_false_r (only parsing).
@@ -349,12 +368,12 @@ Notation andb_false_b := andb_false_l (only parsing).
 
 Lemma andb_true_r : forall b:bool, b && true = b.
 Proof.
-  destruct b; auto with bool.
+  destr_bool.
 Qed.
 
 Lemma andb_true_l : forall b:bool, true && b = b.
 Proof.
-  trivial with bool.
+  reflexivity.
 Qed.
 
 Notation andb_b_true := andb_true_r (only parsing).
@@ -363,7 +382,7 @@ Notation andb_true_b := andb_true_l (only parsing).
 Lemma andb_false_elim :
   forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}.
 Proof.
-  destruct b1; simpl in |- *; auto with bool.
+  destruct b1; simpl; auto.
 Defined.
 Hint Resolve andb_false_elim: bool v62.
 
@@ -371,8 +390,8 @@ Hint Resolve andb_false_elim: bool v62.
 
 Lemma andb_negb_r : forall b:bool, b && negb b = false.
 Proof.
-  destruct b; reflexivity.
-Qed.   
+  destr_bool.
+Qed.
 Hint Resolve andb_negb_r: bool v62.
 
 Notation andb_neg_b := andb_negb_r (only parsing).
@@ -381,14 +400,14 @@ Notation andb_neg_b := andb_negb_r (only parsing).
 
 Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1.
 Proof.
-  destruct b1; destruct b2; reflexivity.
+  destr_bool.
 Qed.
 
 (** Associativity *)
 
 Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3.
 Proof.
-  destruct b1; destruct b2; destruct b3; reflexivity.
+  destr_bool.
 Qed.
 
 Hint Resolve andb_comm andb_assoc: bool v62.
@@ -402,25 +421,25 @@ Hint Resolve andb_comm andb_assoc: bool v62.
 Lemma andb_orb_distrib_r :
   forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3.
 Proof.
-  destruct b1; destruct b2; destruct b3; reflexivity.
+  destr_bool.
 Qed.
 
 Lemma andb_orb_distrib_l :
  forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3.
 Proof.
-  destruct b1; destruct b2; destruct b3; reflexivity.
+  destr_bool.
 Qed.
 
 Lemma orb_andb_distrib_r :
   forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3).
 Proof.
-  destruct b1; destruct b2; destruct b3; reflexivity.
+  destr_bool.
 Qed.
 
 Lemma orb_andb_distrib_l :
   forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3).
 Proof.
-  destruct b1; destruct b2; destruct b3; reflexivity.
+  destr_bool.
 Qed.
 
 (* Compatibility *)
@@ -433,12 +452,12 @@ Notation demorgan4 := orb_andb_distrib_l (only parsing).
 
 Lemma absoption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; reflexivity.
+  destr_bool.
 Qed.
 
 Lemma absoption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; reflexivity.
+  destr_bool.
 Qed.
 
 (*********************************)
@@ -449,12 +468,12 @@ Qed.
 
 Lemma xorb_false_r : forall b:bool, xorb b false = b.
 Proof.
-  destruct b; trivial.
+  destr_bool.
 Qed.
 
 Lemma xorb_false_l : forall b:bool, xorb false b = b.
 Proof.
-  destruct b; trivial.
+  destr_bool.
 Qed.
 
 Notation xorb_false := xorb_false_r (only parsing).
@@ -464,12 +483,12 @@ Notation false_xorb := xorb_false_l (only parsing).
 
 Lemma xorb_true_r : forall b:bool, xorb b true = negb b.
 Proof.
-  trivial.
+  reflexivity.
 Qed.
 
 Lemma xorb_true_l : forall b:bool, xorb true b = negb b.
 Proof.
-  destruct b; trivial.
+  reflexivity.
 Qed.
 
 Notation xorb_true := xorb_true_r (only parsing).
@@ -479,14 +498,14 @@ Notation true_xorb := xorb_true_l (only parsing).
 
 Lemma xorb_nilpotent : forall b:bool, xorb b b = false.
 Proof.
-  destruct b; trivial.
+  destr_bool.
 Qed.
 
 (** Commutativity *)
 
 Lemma xorb_comm : forall b b':bool, xorb b b' = xorb b' b.
 Proof.
-  destruct b; destruct b'; trivial.
+  destr_bool.
 Qed.
 
 (** Associativity *)
@@ -494,61 +513,64 @@ Qed.
 Lemma xorb_assoc_reverse :
   forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b'').
 Proof.
-  destruct b; destruct b'; destruct b''; trivial.
+  destr_bool.
 Qed.
 
 Notation xorb_assoc := xorb_assoc_reverse (only parsing). (* Compatibility *)
 
 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.
+  destr_bool.
 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.
+  destr_bool.
 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.
+  destr_bool.
 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.
+  destr_bool.
 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.
+  destr_bool.
 Qed.
 
 (** Lemmas about the [b = true] embedding of [bool] to [Prop] *)
 
-Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. 
-Proof. 
-  intros b1 b2; case b1; case b2; intuition.
+Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true).
+Proof.
+  destr_bool; intuition.
+Qed.
+
+Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2.
+Proof.
+  apply eq_iff_eq_true.
 Qed.
 
 Notation bool_1 := eq_true_iff_eq (only parsing). (* Compatibility *)
 
 Lemma eq_true_negb_classical : forall b:bool, negb b <> true -> b = true.
 Proof.
-  destruct b; intuition.
+  destr_bool; intuition.
 Qed.
 
 Notation bool_3 := eq_true_negb_classical (only parsing). (* Compatibility *)
 
-Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true.  
+Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true.
 Proof.
-  destruct b; intuition.
+  destr_bool; intuition.
 Qed.
 
 Notation bool_6 := eq_true_not_negb (only parsing). (* Compatibility *)
@@ -589,17 +611,17 @@ Hint Unfold Is_true: bool.
 
 Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true.
 Proof.
-  destruct x; simpl in |- *; tauto.
+  destr_bool; tauto.
 Qed.
 
 Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x.
 Proof.
-  intros; rewrite H; auto with bool.
+  intros; subst; auto with bool.
 Qed.
 
 Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x.
 Proof.
-  intros; rewrite <- H; auto with bool.
+  intros; subst; auto with bool.
 Qed.
 
 Notation Is_true_eq_true2 := Is_true_eq_right (only parsing).
@@ -608,34 +630,34 @@ Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
 
 Lemma eqb_refl : forall x:bool, Is_true (eqb x x).
 Proof.
-  destruct x; simpl; auto with bool.
+  destr_bool.
 Qed.
 
 Lemma eqb_eq : forall x y:bool, Is_true (eqb x y) -> x = y.
 Proof.
-  destruct x; destruct y; simpl; tauto.
+  destr_bool; tauto.
 Qed.
 
 (** [Is_true] and connectives *)
 
-Lemma orb_prop_elim : 
+Lemma orb_prop_elim :
   forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b.
 Proof.
-  destruct a; destruct b; simpl; tauto.
+  destr_bool; tauto.
 Qed.
 
 Notation orb_prop2 := orb_prop_elim (only parsing).
 
-Lemma orb_prop_intro : 
+Lemma orb_prop_intro :
   forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b).
 Proof.
-  destruct a; destruct b; simpl; tauto.
+  destr_bool; tauto.
 Qed.
 
 Lemma andb_prop_intro :
   forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2).
 Proof.
-  destruct b1; destruct b2; simpl in |- *; tauto.
+  destr_bool; tauto.
 Qed.
 Hint Resolve andb_prop_intro: bool v62.
 
@@ -646,66 +668,65 @@ Notation andb_true_intro2 :=
 Lemma andb_prop_elim :
   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.
+  destr_bool; auto.
 Qed.
 Hint Resolve andb_prop_elim: bool v62.
 
 Notation andb_prop2 := andb_prop_elim (only parsing).
 
-Lemma eq_bool_prop_intro : 
-  forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. 
-Proof. 
-  destruct b1; destruct b2; simpl in *; intuition.
+Lemma eq_bool_prop_intro :
+  forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2.
+Proof.
+  destr_bool; tauto.
 Qed.
 
 Lemma eq_bool_prop_elim : forall b1 b2, b1 = b2 -> (Is_true b1 <-> Is_true b2).
-Proof. 
-  intros b1 b2; case b1; case b2; intuition.
-Qed. 
+Proof.
+  destr_bool; tauto.
+Qed.
 
 Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b.
 Proof.
-  destruct b; intuition.
+  destr_bool; tauto.
 Qed.
 
 Lemma negb_prop_intro : forall b, ~ Is_true b -> Is_true (negb b).
 Proof.
-  destruct b; simpl in *; intuition.
+  destr_bool; tauto.
 Qed.
 
 Lemma negb_prop_classical : forall b, ~ Is_true (negb b) -> Is_true b.
 Proof.
-  destruct b; intuition.
+  destr_bool; tauto.
 Qed.
 
 Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b).
 Proof.
-  destruct b; intuition.
+  destr_bool; tauto.
 Qed.
 
 (** Rewrite rules about andb, orb and if (used in romega) *)
 
-Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), 
-  (if b && b' then a else a') = 
+Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool),
+  (if b && b' then a else a') =
   (if b then if b' then a else a' else a').
 Proof.
- destruct b; destruct b'; auto.
+  destr_bool.
 Qed.
 
-Lemma negb_if : forall (A:Type)(a a':A)(b:bool), 
- (if negb b then a else a') = 
+Lemma negb_if : forall (A:Type)(a a':A)(b:bool),
+ (if negb b then a else a') =
  (if b then a' else a).
 Proof.
- destruct b; auto.
+  destr_bool.
 Qed.
 
 (*****************************************)
-(** * Alternative versions of [andb] and [orb] 
+(** * Alternative versions of [andb] and [orb]
     with lazy behavior (for vm_compute)  *)
 (*****************************************)
 
-Notation "a &&& b" := (if a then b else false) 
+Notation "a &&& b" := (if a then b else false)
  (at level 40, left associativity) : lazy_bool_scope.
 Notation "a ||| b" := (if a then true else b)
  (at level 50, left associativity) : lazy_bool_scope.
@@ -714,12 +735,51 @@ Open Local Scope lazy_bool_scope.
 
 Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b.
 Proof.
- unfold andb; auto.
+  reflexivity.
 Qed.
 
 Lemma orb_lazy_alt : forall a b : bool, a || b = a ||| b.
 Proof.
- unfold orb; auto.
+  reflexivity.
+Qed.
+
+(*****************************************)
+(** * Reflect: a specialized inductive type for
+    relating propositions and booleans,
+    as popularized by the Ssreflect library. *)
+(*****************************************)
+
+Inductive reflect (P : Prop) : bool -> Set :=
+  | ReflectT : P -> reflect P true
+  | ReflectF : ~ P -> reflect P false.
+Hint Constructors reflect : bool.
+
+(** Interest: a case on a reflect lemma or hyp performs clever
+    unification, and leave the goal in a convenient shape
+    (a bit like case_eq). *)
+
+(** Relation with iff : *)
+
+Lemma reflect_iff : forall P b, reflect P b -> (P<->b=true).
+Proof.
+ destruct 1; intuition; discriminate.
+Qed.
+
+Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b.
+Proof.
+ destr_bool; intuition.
 Qed.
 
+(** It would be nice to join [reflect_iff] and [iff_reflect]
+    in a unique [iff] statement, but this isn't allowed since
+    [iff] is in Prop. *)
+
+(** Reflect implies decidability of the proposition *)
+
+Lemma reflect_dec : forall P b, reflect P b -> {P}+{~P}.
+Proof.
+ destruct 1; auto.
+Qed.
 
+(** Reciprocally, from a decidability, we could state a
+    [reflect] as soon as we have a [bool_of_sumbool]. *)
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index 806ac70f..625cbd19 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BoolEq.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
 (* Cuihtlauac Alvarado - octobre 2000 *)
 
 (** Properties of a boolean equality   *)
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 0e8ea33c..7ecfa43f 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Bvector.v 11004 2008-05-28 09:09:12Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
@@ -16,34 +16,34 @@ Require Import Arith.
 
 Open Local Scope nat_scope.
 
-(** 
-On s'inspire de List.v 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 et dans certains cas on
-utilisera un terme de preuve comme définition, car le
-mécanisme d'inférence du type du filtrage n'est pas toujours 
-aussi puissant que celui implanté par les tactiques d'élimination.
+(**
+We build bit vectors in the spirit of List.v.
+The size of the vector is a parameter which is too important
+to be accessible only via function "length".
+The first idea is to build a record with both the list and the length.
+Unfortunately, this a posteriori verification leads to
+numerous lemmas for handling lengths.
+The second idea is to use a dependent type in which the length
+is a building parameter. This leads to structural induction that
+are slightly more complex and in some cases we will use a proof-term
+as definition, since the type inference mechanism for pattern-matching
+is sometimes weaker that the one implemented for elimination tactiques.
 *)
 
 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 couples de vecteurs 
-de taille n dans les vecteurs de taille n en appliquant f terme à terme.
+(**
+A vector is a list of size n whose elements belongs to a set A.
+If the size is non-zero, we can extract the first component and the
+rest of the vector, as well as the last component, or adding or
+removing a component (carry) or repeating the last component at the
+end of the vector.
+We can also truncate the vector and remove its p last components or
+reciprocally extend the vector by concatenation.
+A unary function over A generates a function on vectors of size n by
+applying f pointwise.
+A binary function over A generates a function on pairs of vectors of
+size n by applying f pointwise.
 *)
 
 Variable A : Type.
@@ -93,7 +93,7 @@ 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 as [| a0 n0 H0 H1 ].
   exact (Vcons a (S n) (f a H0)).
 Defined.
@@ -103,7 +103,7 @@ Proof.
   induction n as [| n f]; intro v.
   inversion v.
   exact (Vcons a 1 v).
-  
+
   inversion v as [| a n0 H0 H1 ].
   exact (Vcons a (S (S n)) (f H0)).
 Defined.
@@ -113,9 +113,9 @@ 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 *.
@@ -147,7 +147,7 @@ Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
 Proof.
   induction n as [| n h]; intros v v0.
   exact Vnil.
-  
+
   inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
   exact (Vcons (g a a0) n (h H0 H2)).
 Defined.
@@ -180,7 +180,7 @@ Qed.
 
 End VECTORS.
 
-(* suppressed: incompatible with Coq-Art book 
+(* suppressed: incompatible with Coq-Art book
 Implicit Arguments Vnil [A].
 Implicit Arguments Vcons [A n].
 *)
@@ -188,15 +188,16 @@ 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).
+A bit vector is a vector over booleans.
+Notice that the LEAST significant bit comes first (little-endian representation).
+We extract the least significant bit (head) and the rest of the vector (tail).
+We compute bitwise operation on vector: negation, and, or, xor.
+We compute size-preserving shifts: to the left (towards most significant bits,
+we hence use Vshiftout) and to the right (towards least significant bits,
+we use Vshiftin) by inserting a 'carry' bit (logical shift) or by repeating
+the most significant bit (arithmetical shift).
+NOTA BENE: all shift operations expect predecessor of size as parameter
+(they only work on non-empty vectors).
 *)
 
 Definition Bvector := vector bool.
@@ -232,22 +233,19 @@ Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
 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) :=
+Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : 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) :=
+Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : 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) :=
+Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
     | S p' => BshiftRa n (BshiftRa_iter n bv p')
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index af9acea1..90f7ee66 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: DecBool.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 0a98c32a..c2b5ed79 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: IfProp.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id$ i*)
 
 Require Import Bool.
 
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 0da72f56..06ab77cf 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sumbool.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ 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
@@ -39,18 +39,18 @@ Defined.
 Section connectives.
 
   Variables A B C D : Prop.
-  
+
   Hypothesis H1 : {A} + {B}.
   Hypothesis H2 : {C} + {D}.
-  
+
   Definition sumbool_and : {A /\ C} + {B \/ D}.
     case H1; case H2; auto.
   Defined.
-  
+
   Definition sumbool_or : {A \/ C} + {B /\ D}.
     case H1; case H2; auto.
   Defined.
-  
+
   Definition sumbool_not : {B} + {A}.
     case H1; auto.
   Defined.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index fe656777..5e9d4afa 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zerob.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id$ i*)
 
 Require Import Arith.
 Require Import Bool.
diff --git a/theories/Bool/vo.itarget b/theories/Bool/vo.itarget
new file mode 100644
index 00000000..24cbf4ed
--- /dev/null
+++ b/theories/Bool/vo.itarget
@@ -0,0 +1,7 @@
+BoolEq.vo
+Bool.vo
+Bvector.vo
+DecBool.vo
+IfProp.vo
+Sumbool.vo
+Zerob.vo