Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

2 files changed, 89 insertions, 82 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index e126ad35..47b9fc83 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Bool.v 9246 2006-10-17 14:01:18Z herbelin $ i*)
+(*i $Id: Bool.v 10812 2008-04-17 16:42:37Z letouzey $ i*)
 
 (** The type [bool] is defined in the prelude as
     [Inductive bool : Set := true : bool | false : bool] *)
@@ -126,9 +126,8 @@ Proof.
   destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity.
 Qed.
 
-
 (************************)
-(** * Logical combinators *)
+(** * A synonym of [if] on [bool] *)
 (************************)
  
 Definition ifb (b1 b2 b3:bool) : bool :=
@@ -137,31 +136,8 @@ Definition ifb (b1 b2 b3:bool) : bool :=
     | 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) := if b then false else true.
-
-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.
-
 (****************************)
 (** * De Morgan laws          *)
 (****************************)
@@ -220,7 +196,7 @@ Qed.
 
 
 Lemma if_negb :
-  forall (A:Set) (b:bool) (x y:A),
+  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.
@@ -332,12 +308,11 @@ Hint Resolve orb_comm orb_assoc: bool v62.
 (** * Properties of [andb]     *)
 (*******************************)
 
-Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true.
+Lemma andb_true_iff : 
+  forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true.
 Proof.
-  destruct a; destruct b; simpl in |- *; try (intro H; discriminate H);
-    auto with bool.
+ destruct b1; destruct b2; intuition.
 Qed.
-Hint Resolve andb_prop: bool v62.
 
 Lemma andb_true_eq :
   forall a b:bool, true = a && b -> true = a /\ true = b.
@@ -345,13 +320,6 @@ Proof.
   destruct a; destruct b; auto.
 Defined.
 
-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_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false.
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
@@ -715,3 +683,43 @@ Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b).
 Proof.
   destruct b; intuition.
 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') = 
+  (if b then if b' then a else a' else a').
+Proof.
+ destruct b; destruct b'; auto.
+Qed.
+
+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.
+Qed.
+
+(*****************************************)
+(** * Alternative versions of [andb] and [orb] 
+    with lazy behavior (for vm_compute)  *)
+(*****************************************)
+
+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.
+
+Open Local Scope lazy_bool_scope.
+
+Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b.
+Proof.
+ unfold andb; auto.
+Qed.
+
+Lemma orb_lazy_alt : forall a b : bool, a || b = a ||| b.
+Proof.
+ unfold orb; auto.
+Qed.
+
+
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 659630c5..0e8ea33c 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 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Bvector.v 11004 2008-05-28 09:09:12Z herbelin $ i*)
 
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
@@ -25,10 +25,10 @@ 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, car le
-mécanisme d'inférence du type du filtrage n'est pas aussi puissant que
-celui implanté par les tactiques d'élimination.
+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.
 *)
 
 Section VECTORS.
@@ -52,39 +52,39 @@ Inductive vector : nat -> Type :=
   | 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 Vhead (n:nat) (v:vector (S n)) :=
+  match v with
+  | Vcons a _ _ => a
+  end.
 
-Definition Vtail : forall n:nat, vector (S n) -> vector n.
-Proof.
-  intros n v; inversion v as [|_ n0 H0 H1]; exact H0.
-Defined.
+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.
 
-Definition Vconst : forall (a:A) (n:nat), vector n.
-Proof.
-  induction n as [| n v].
-  exact Vnil.
+Fixpoint Vconst (a:A) (n:nat) :=
+  match n return vector n with
+  | O => Vnil
+  | S n => Vcons a _ (Vconst a n)
+  end.
 
-  exact (Vcons a n v).
-Defined.
+(** 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.
@@ -123,25 +123,23 @@ Proof.
   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 as [| a n0 H0 H1].
-  simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
-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.
 
-Lemma Vunary : forall n:nat, vector n -> vector n.
-Proof.
-  induction n as [| n g]; intro v.
-  exact Vnil.
-  
-  inversion v as [| a n0 H0 H1].
-  exact (Vcons (f a) n (g H0)).
-Defined.
+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.
 
@@ -154,14 +152,15 @@ Proof.
   exact (Vcons (g a a0) n (h H0 H2)).
 Defined.
 
-Definition Vid : forall n:nat, vector n -> vector n.
-Proof.
-  destruct n; intro X.
-  exact Vnil.
-  exact (Vcons (Vhead _ X) _ (Vtail _ X)).
-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).
+Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
 Proof.
   destruct v; auto.
 Qed.