diff options
author | 2003-11-29 16:15:58 +0000 | |
---|---|---|
committer | 2003-11-29 16:15:58 +0000 | |
commit | 9058fb97426307536f56c3e7447be2f70798e081 (patch) | |
tree | b9a5fcf2ace7ecec13ed264b93c33fc04b0f220f /theories7/Bool/Bvector.v | |
parent | 95ad10e5eb2efc9b63382e0e6a2f9ada8da2ea2d (diff) |
Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5026 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7/Bool/Bvector.v')
-rw-r--r-- | theories7/Bool/Bvector.v | 266 |
1 files changed, 266 insertions, 0 deletions
diff --git a/theories7/Bool/Bvector.v b/theories7/Bool/Bvector.v new file mode 100644 index 000000000..792d6a067 --- /dev/null +++ b/theories7/Bool/Bvector.v @@ -0,0 +1,266 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) + +Require Export Bool. +Require Export Sumbool. +Require Arith. + +V7only [Import nat_scope.]. +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 O) + | Vcons : (a:A) (n:nat) (vector n) -> (vector (S n)). + +Definition Vhead : (n:nat) (vector (S n)) -> A. +Proof. + Intros n v; Inversion v; Exact a. +Defined. + +Definition Vtail : (n:nat) (vector (S n)) -> (vector n). +Proof. + Intros n v; Inversion v; Exact H0. +Defined. + +Definition Vlast : (n:nat) (vector (S n)) -> A. +Proof. + NewInduction n as [|n f]; Intro v. + Inversion v. + Exact a. + + Inversion v. + Exact (f H0). +Defined. + +Definition Vconst : (a:A) (n:nat) (vector n). +Proof. + NewInduction n as [|n v]. + Exact Vnil. + + Exact (Vcons a n v). +Defined. + +Lemma Vshiftout : (n:nat) (vector (S n)) -> (vector n). +Proof. + NewInduction n as [|n f]; Intro v. + Exact Vnil. + + Inversion v. + Exact (Vcons a n (f H0)). +Defined. + +Lemma Vshiftin : (n:nat) A -> (vector n) -> (vector (S n)). +Proof. + NewInduction n as [|n f]; Intros a v. + Exact (Vcons a O v). + + Inversion v. + Exact (Vcons a (S n) (f a H0)). +Defined. + +Lemma Vshiftrepeat : (n:nat) (vector (S n)) -> (vector (S (S n))). +Proof. + NewInduction 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 : (n,p:nat) (gt n p) -> (vector n) -> (vector (minus n p)). +Proof. + NewInduction p as [|p f]; Intros H v. + Rewrite <- minus_n_O. + Exact v. + + Apply (Vshiftout (minus n (S p))). + +Rewrite minus_Sn_m. +Apply f. +Auto with *. +Exact v. +Auto with *. +Defined. + +Lemma Vextend : (n,p:nat) (vector n) -> (vector p) -> (vector (plus n p)). +Proof. + NewInduction n as [|n f]; Intros p v v0. + Simpl; Exact v0. + + Inversion v. + Simpl; Exact (Vcons a (plus n p) (f p H0 v0)). +Defined. + +Variable f : A -> A. + +Lemma Vunary : (n:nat)(vector n)->(vector n). +Proof. + NewInduction 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 : (n:nat)(vector n)->(vector n)->(vector n). +Proof. + NewInduction 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. + +(* +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]:(Bvector (S n)) := +Cases p of + | O => bv + | (S p') => (BshiftL n (BshiftL_iter n bv p') false) +end. + +Fixpoint BshiftRl_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := +Cases p of + | O => bv + | (S p') => (BshiftRl n (BshiftRl_iter n bv p') false) +end. + +Fixpoint BshiftRa_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := +Cases p of + | O => bv + | (S p') => (BshiftRa n (BshiftRa_iter n bv p')) +end. + +End BOOLEAN_VECTORS. + |