Imported Upstream version 8.4~betaupstream/8.4_beta

7 files changed, 57 insertions, 198 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 9509d9fd..d5d11cea 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Bool.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** The type [bool] is defined in the prelude as
     [Inductive bool : Set := true : bool | false : bool] *)
 
@@ -259,6 +257,11 @@ Proof.
   intros. apply orb_false_iff; trivial.
 Qed.
 
+Lemma orb_diag : forall b, b || b = b.
+Proof.
+ destr_bool.
+Qed.
+
 (** [true] is a zero for [orb] *)
 
 Lemma orb_true_r : forall b:bool, b || true = true.
@@ -364,6 +367,11 @@ Qed.
 Notation andb_b_false := andb_false_r (only parsing).
 Notation andb_false_b := andb_false_l (only parsing).
 
+Lemma andb_diag : forall b, b && b = b.
+Proof.
+ destr_bool.
+Qed.
+
 (** [true] is neutral for [andb] *)
 
 Lemma andb_true_r : forall b:bool, b && true = b.
@@ -547,6 +555,21 @@ Proof.
   destr_bool.
 Qed.
 
+Lemma negb_xorb_l : forall b b', negb (xorb b b') = xorb (negb b) b'.
+Proof.
+ destruct b,b'; trivial.
+Qed.
+
+Lemma negb_xorb_r : forall b b', negb (xorb b b') = xorb b (negb b').
+Proof.
+ destruct b,b'; trivial.
+Qed.
+
+Lemma xorb_negb_negb : forall b b', xorb (negb b) (negb b') = xorb b b'.
+Proof.
+ destruct b,b'; trivial.
+Qed.
+
 (** Lemmas about the [b = true] embedding of [bool] to [Prop] *)
 
 Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true).
@@ -768,7 +791,7 @@ Qed.
 Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b.
 Proof.
  destr_bool; intuition.
-Qed.
+Defined.
 
 (** It would be nice to join [reflect_iff] and [iff_reflect]
     in a unique [iff] statement, but this isn't allowed since
@@ -779,7 +802,7 @@ Qed.
 Lemma reflect_dec : forall P b, reflect P b -> {P}+{~P}.
 Proof.
  destruct 1; auto.
-Qed.
+Defined.
 
 (** 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 ee82caf1..d40e56bf 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -1,12 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BoolEq.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
 (* Cuihtlauac Alvarado - octobre 2000 *)
 
 (** Properties of a boolean equality   *)
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index daf3a9fb..0c218163 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -1,18 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Bvector.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
-Require Export Bool.
-Require Export Sumbool.
-Require Import Arith.
+Require Export Bool Sumbool.
+Require Vector.
+Export Vector.VectorNotations.
+Require Import Minus.
 
 Open Local Scope nat_scope.
 
@@ -30,161 +29,6 @@ as definition, since the type inference mechanism for pattern-matching
 is sometimes weaker that the one implemented for elimination tactiques.
 *)
 
-Section VECTORS.
-
-(**
-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.
-
-Inductive vector : nat -> Type :=
-  | Vnil : vector 0
-  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
-
-Definition Vhead (n:nat) (v:vector (S n)) :=
-  match v with
-  | Vcons a _ _ => a
-  end.
-
-Definition Vtail (n:nat) (v:vector (S n)) :=
-  match v with
-  | Vcons _ _ v => v
-  end.
-
-Definition Vlast : forall n:nat, vector (S n) -> A.
-Proof.
-  induction n as [| n f]; intro v.
-  inversion v.
-  exact a.
-
-  inversion v as [| n0 a H0 H1].
-  exact (f H0).
-Defined.
-
-Fixpoint Vconst (a:A) (n:nat) :=
-  match n return vector n with
-  | O => Vnil
-  | S n => Vcons a _ (Vconst a n)
-  end.
-
-(** Shifting and truncating *)
-
-Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
-Proof.
-  induction n as [| n f]; intro v.
-  exact Vnil.
-
-  inversion v as [| a n0 H0 H1].
-  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 as [| a0 n0 H0 H1 ].
-  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 as [| a n0 H0 H1 ].
-  exact (Vcons a (S (S n)) (f H0)).
-Defined.
-
-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.
-
-(** Concatenation of two vectors *)
-
-Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) :=
-  match v with
-  | Vnil => w
-  | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w)
-  end.
-
-(** Uniform application on the arguments of the vector *)
-
-Variable f : A -> A.
-
-Fixpoint Vunary n (v:vector n) : vector n :=
-  match v with
-  | Vnil => Vnil
-  | Vcons a n' v' => Vcons (f a) n' (Vunary n' v')
-  end.
-
-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 as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
-  exact (Vcons (g a a0) n (h H0 H2)).
-Defined.
-
-(** Eta-expansion of a vector *)
-
-Definition Vid n : vector n -> vector n :=
-  match n with
-  | O => fun _ => Vnil
-  | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v)
-  end.
-
-Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
-Proof.
-  destruct v; auto.
-Qed.
-
-Lemma VSn_eq :
-  forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v).
-Proof.
-  intros.
-  exact (Vid_eq _ v).
-Qed.
-
-Lemma V0_eq : forall (v : vector 0), v = Vnil.
-Proof.
-  intros.
-  exact (Vid_eq _ v).
-Qed.
-
-End VECTORS.
-
-(* suppressed: incompatible with Coq-Art book
-Implicit Arguments Vnil [A].
-Implicit Arguments Vcons [A n].
-*)
-
 Section BOOLEAN_VECTORS.
 
 (**
@@ -200,38 +44,38 @@ NOTA BENE: all shift operations expect predecessor of size as parameter
 (they only work on non-empty vectors).
 *)
 
-Definition Bvector := vector bool.
+Definition Bvector := Vector.t bool.
 
-Definition Bnil := @Vnil bool.
+Definition Bnil := @Vector.nil bool.
 
-Definition Bcons := @Vcons bool.
+Definition Bcons := @Vector.cons bool.
 
-Definition Bvect_true := Vconst bool true.
+Definition Bvect_true := Vector.const true.
 
-Definition Bvect_false := Vconst bool false.
+Definition Bvect_false := Vector.const false.
 
-Definition Blow := Vhead bool.
+Definition Blow := @Vector.hd bool.
 
-Definition Bhigh := Vtail bool.
+Definition Bhigh := @Vector.tl bool.
 
-Definition Bsign := Vlast bool.
+Definition Bsign := @Vector.last bool.
 
-Definition Bneg := Vunary bool negb.
+Definition Bneg n (v : Bvector n) := Vector.map negb v.
 
-Definition BVand := Vbinary bool andb.
+Definition BVand n (v : Bvector n) := Vector.map2 andb v.
 
-Definition BVor := Vbinary bool orb.
+Definition BVor n (v : Bvector n) := Vector.map2 orb v.
 
-Definition BVxor := Vbinary bool xorb.
+Definition BVxor n (v : Bvector n) := Vector.map2 xorb v.
 
 Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
-  Bcons carry n (Vshiftout bool n bv).
+  Bcons carry n (Vector.shiftout bv).
 
 Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
-  Bhigh (S n) (Vshiftin bool (S n) carry bv).
+  Bhigh (S n) (Vector.shiftin carry bv).
 
 Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
-  Bhigh (S n) (Vshiftrepeat bool n bv).
+  Bhigh (S n) (Vector.shiftrepeat bv).
 
 Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
@@ -252,3 +96,4 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   end.
 
 End BOOLEAN_VECTORS.
+
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index e49d1f97..3f03d2c1 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: DecBool.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Set Implicit Arguments.
 
 Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C :=
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 9cca05d4..6872eaea 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: IfProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Bool.
 
 Inductive IfProp (A B:Prop) : bool -> Prop :=
@@ -47,4 +45,4 @@ 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
+Qed.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 5b1822be..24b6a776 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sumbool.v 14641 2011-11-06 11:59:10Z herbelin $ 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.
@@ -68,4 +66,4 @@ Definition bool_of_sumbool :
   intros A B H.
   elim H; intro; [exists true | exists false]; assumption.
 Defined.
-Implicit Arguments bool_of_sumbool.
\ No newline at end of file
+Arguments bool_of_sumbool : default implicits.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index e67ba677..bac4c0d6 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zerob.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Arith.
 Require Import Bool.
 
@@ -39,4 +37,4 @@ Hint Resolve zerob_false_intro: bool.
 Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
 Proof.
   destruct n; [ inversion 1 | auto with bool ].
-Qed.
\ No newline at end of file
+Qed.