diff options
Diffstat (limited to 'theories/Bool/Bvector.v')
-rw-r--r-- | theories/Bool/Bvector.v | 272 |
1 files changed, 272 insertions, 0 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v new file mode 100644 index 00000000..51d940cf --- /dev/null +++ b/theories/Bool/Bvector.v @@ -0,0 +1,272 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Bvector.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) + +(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) + +Require Export Bool. +Require Export Sumbool. +Require Import Arith. + +Open Local Scope nat_scope. + +(* +On s'inspire de PolyList pour fabriquer les vecteurs de bits. +La dimension du vecteur est un paramètre trop important pour +se contenter de la fonction "length". +La première idée est de faire un record avec la liste et la longueur. +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. + +(En effet une définition comme : +Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) := +Cases v of + | Vnil => Vnil + | (Vcons a p v') => (Vcons (f a) p (Vunaire p v')) +end. +provoque ce message d'erreur : +Coq < Error: Inference of annotation not yet implemented in this case). + + + Inductive list [A : Set] : Set := + nil : (list A) | cons : A->(list A)->(list A). + head = [A:Set; l:(list A)] Cases l of + | nil => Error + | (cons x _) => (Value x) + end + : (A:Set)(list A)->(option A). + tail = [A:Set; l:(list A)]Cases l of + | nil => (nil A) + | (cons _ m) => m + end + : (A:Set)(list A)->(list A). + length = [A:Set] Fix length {length [l:(list A)] : nat := + Cases l of + | nil => O + | (cons _ m) => (S (length m)) + end} + : (A:Set)(list A)->nat. + map = [A,B:Set; f:(A->B)] Fix map {map [l:(list A)] : (list B) := + Cases l of + | nil => (nil B) + | (cons a t) => (cons (f a) (map t)) + end} + : (A,B:Set)(A->B)->(list A)->(list B) +*) + +Section VECTORS. + +(* +Un vecteur est une liste de taille n d'éléments d'un ensemble A. +Si la taille est non nulle, on peut extraire la première composante et +le reste du vecteur, la dernière composante ou rajouter ou enlever +une composante (carry) ou repeter la dernière composante en fin de vecteur. +On peut aussi tronquer le vecteur de ses p dernières composantes ou +au contraire l'étendre (concaténer) d'un vecteur de longueur p. +Une fonction unaire sur A génère une fonction des vecteurs de taille n +dans les vecteurs de taille n en appliquant f terme à terme. +Une fonction binaire sur A génère une fonction des couple de vecteurs +de taille n dans les vecteurs de taille n en appliquant f terme à terme. +*) + +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 S_minus_S : (n,p:nat) (gt n (S p)) -> (S (minus n (S p)))=(minus n p). +Proof. + Intros. +Save. +*) + +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. + +(* suppressed: incompatible with Coq-Art book +Implicit Arguments Vnil [A]. +Implicit Arguments Vcons [A n]. +*) + +Section BOOLEAN_VECTORS. + +(* +Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. +ATTENTION : le stockage s'effectue poids FAIBLE en tête. +On en extrait le bit de poids faible (head) et la fin du vecteur (tail). +On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs. +On calcule les décalages d'une position vers la gauche (vers les poids forts, on +utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en +insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique). +ATTENTION : Tous les décalages prennent la taille moins un comme paramètre +(ils ne travaillent que sur des vecteurs au moins de longueur un). +*) + +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. |