summaryrefslogtreecommitdiff
path: root/theories/Bool
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/Bool
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Bool.v84
-rw-r--r--theories/Bool/Bvector.v87
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.