From 05085e80668a4d1dedc522c6af343168870cc648 Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 10 Dec 2010 13:22:29 +0000 Subject: First release of Vector library. To avoid names¬ations 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 --- theories/Bool/Bvector.v | 189 +++++------------------------------------------- theories/Bool/IfProp.v | 2 +- theories/Bool/Sumbool.v | 2 +- theories/Bool/Zerob.v | 2 +- 4 files changed, 20 insertions(+), 175 deletions(-) (limited to 'theories/Bool') 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. -- cgit v1.2.3