diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /theories/Bool/Bvector.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Bool/Bvector.v')
-rw-r--r-- | theories/Bool/Bvector.v | 196 |
1 files changed, 98 insertions, 98 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 576993c9..659630c5 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Bvector.v 8866 2006-05-28 16:21:04Z herbelin $ i*) +(*i $Id: Bvector.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) @@ -16,34 +16,34 @@ Require Import Arith. Open Local Scope nat_scope. -(* +(** On s'inspire de List.v pour fabriquer les vecteurs de bits. -La dimension du vecteur est un paramètre trop important pour +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. +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, car le -mécanisme d'inférence du type du filtrage n'est pas aussi puissant que -celui implanté par les tactiques d'élimination. +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, car le +mécanisme d'inférence du type du filtrage n'est pas aussi puissant que +celui implanté par les tactiques d'élimination. *) 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. +(** +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 couples de vecteurs +de taille n dans les vecteurs de taille n en appliquant f terme à terme. *) Variable A : Type. @@ -54,129 +54,129 @@ Inductive vector : nat -> Type := Definition Vhead : forall n:nat, vector (S n) -> A. Proof. - intros n v; inversion v; exact a. + intros n v; inversion v; exact a. Defined. Definition Vtail : forall n:nat, vector (S n) -> vector n. Proof. - intros n v; inversion v as [|_ n0 H0 H1]; exact H0. + intros n v; inversion v as [|_ n0 H0 H1]; 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 as [| n0 a H0 H1]. - exact (f H0). + induction n as [| n f]; intro v. + inversion v. + exact a. + + inversion v as [| n0 a H0 H1]. + exact (f H0). Defined. Definition Vconst : forall (a:A) (n:nat), vector n. Proof. - induction n as [| n v]. - exact Vnil. + induction n as [| n v]. + exact Vnil. - exact (Vcons a n v). + 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 as [| a n0 H0 H1]. - exact (Vcons a n (f H0)). + 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 a (S n) (f a H0)). + induction n as [| n f]; intros a v. + exact (Vcons a 0 v). + + inversion v as [| a0 n0 H0 H1 ]. + 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 as [| a n0 H0 H1 ]. - exact (Vcons a (S (S n)) (f H0)). + 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 *. + 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 as [| a n0 H0 H1]. - simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). + induction n as [| n f]; intros p v v0. + simpl in |- *; exact v0. + + inversion v as [| a n0 H0 H1]. + 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 as [| a n0 H0 H1]. - exact (Vcons (f a) n (g H0)). + induction n as [| n g]; intro v. + exact Vnil. + + inversion v as [| a n0 H0 H1]. + 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 as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3]. - exact (Vcons (g a a0) n (h H0 H2)). + 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. Definition Vid : forall n:nat, vector n -> vector n. Proof. -destruct n; intro X. -exact Vnil. -exact (Vcons (Vhead _ X) _ (Vtail _ X)). + destruct n; intro X. + exact Vnil. + exact (Vcons (Vhead _ X) _ (Vtail _ X)). Defined. Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v). Proof. -destruct v; auto. + 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). + intros. + exact (Vid_eq _ v). Qed. Lemma V0_eq : forall (v : vector 0), v = Vnil. Proof. -intros. -exact (Vid_eq _ v). + intros. + exact (Vid_eq _ v). Qed. End VECTORS. @@ -188,15 +188,15 @@ 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. +(** +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 +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 +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). *) @@ -234,24 +234,24 @@ 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) := + Bvector (S n) := match p with - | O => bv - | S p' => BshiftL n (BshiftL_iter n bv p') false + | 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) := + Bvector (S n) := match p with - | O => bv - | S p' => BshiftRl n (BshiftRl_iter n bv p') false + | 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) := + Bvector (S n) := match p with - | O => bv - | S p' => BshiftRa n (BshiftRa_iter n bv p') + | O => bv + | S p' => BshiftRa n (BshiftRa_iter n bv p') end. End BOOLEAN_VECTORS. |