aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-10 13:22:29 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-10 13:22:29 +0000
commit05085e80668a4d1dedc522c6af343168870cc648 (patch)
tree084048fdff9f8d460e75ece78d5297b583d952f4 /theories/Bool
parentd52641d2cda2af132c13dcb481f753d51e7af216 (diff)
First release of Vector library.
To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Bvector.v189
-rw-r--r--theories/Bool/IfProp.v2
-rw-r--r--theories/Bool/Sumbool.v2
-rw-r--r--theories/Bool/Zerob.v2
4 files changed, 20 insertions, 175 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 694ed15b4..0c2181638 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -9,6 +9,8 @@
(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
Require Export Bool Sumbool.
+Require Vector.
+Export Vector.VectorNotations.
Require Import Minus.
Open Local Scope nat_scope.
@@ -27,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 a0 (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.
(**
@@ -197,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
@@ -250,5 +97,3 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
End BOOLEAN_VECTORS.
-Implicit Arguments Vcons [[A] [n]] [].
-Implicit Arguments Vnil [[A]] [].
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 6550a4955..6872eaea3 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -45,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 942607faf..73a092143 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -66,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
+Implicit Arguments bool_of_sumbool.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index a7c739625..bac4c0d69 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -37,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.