| Bit vectors. Contribution by Jean Duprat (ENS Lyon). |
Require Export Bool.
Require Export Sumbool.
Require Import Arith.
Open Local Scope nat_scope.
Section VECTORS.
Variable A : Set.
Inductive vector : nat -> Set :=
| 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 Vtail : forall n:nat, vector (S n) -> vector n.
Proof.
intros n v; inversion v; exact H0.
Defined.
Definition Vlast : forall n:nat, vector (S n) -> A.
Proof.
induction n as [| n f]; intro v.
inversion v.
exact a.
inversion v.
exact (f H0).
Defined.
Definition Vconst : forall (a:A) (n:nat), vector n.
Proof.
induction n as [| n v].
exact Vnil.
exact (Vcons a n v).
Defined.
Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
Proof.
induction n as [| n f]; intro v.
exact Vnil.
inversion v.
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.
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.
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.
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.
simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)).
Defined.
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.
exact (Vcons (f a) n (g H0)).
Defined.
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; inversion v0.
exact (Vcons (g a a0) n (h H0 H2)).
Defined.
End VECTORS.
Section BOOLEAN_VECTORS.
Definition Bvector := vector bool.
Definition Bnil := @Vnil bool.
Definition Bcons := @Vcons bool.
Definition Bvect_true := Vconst bool true.
Definition Bvect_false := Vconst bool false.
Definition Blow := Vhead bool.
Definition Bhigh := Vtail bool.
Definition Bsign := Vlast bool.
Definition Bneg := Vunary bool negb.
Definition BVand := Vbinary bool andb.
Definition BVor := Vbinary bool orb.
Definition BVxor := Vbinary bool xorb.
Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
Bcons carry n (Vshiftout bool n bv).
Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
Bhigh (S n) (Vshiftin bool (S n) carry bv).
Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
Bhigh (S n) (Vshiftrepeat bool n bv).
Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
Bvector (S n) :=
match p with
| O => bv
| S p' => BshiftL n (BshiftL_iter n bv p') false
end.
Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
Bvector (S n) :=
match p with
| O => bv
| S p' => BshiftRl n (BshiftRl_iter n bv p') false
end.
Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} :
Bvector (S n) :=
match p with
| O => bv
| S p' => BshiftRa n (BshiftRa_iter n bv p')
end.
End BOOLEAN_VECTORS.