diff options
Diffstat (limited to 'theories/Bool')
| -rw-r--r-- | theories/Bool/Bvector.v | 95 | ||||
| -rw-r--r-- | theories/Bool/DecBool.v | 6 |
2 files changed, 63 insertions, 38 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index b58ed280..576993c9 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 6844 2005-03-16 13:09:55Z herbelin $ i*) +(*i $Id: Bvector.v 8866 2006-05-28 16:21:04Z herbelin $ i*) (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) @@ -18,37 +18,37 @@ 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 couple de vecteurs +de taille n dans les vecteurs de taille n en appliquant f terme à terme. *) -Variable A : Set. +Variable A : Type. -Inductive vector : nat -> Set := +Inductive vector : nat -> Type := | Vnil : vector 0 | Vcons : forall (a:A) (n:nat), vector n -> vector (S n). @@ -59,7 +59,7 @@ Defined. Definition Vtail : forall n:nat, vector (S n) -> vector n. Proof. - intros n v; inversion v; exact H0. + intros n v; inversion v as [|_ n0 H0 H1]; exact H0. Defined. Definition Vlast : forall n:nat, vector (S n) -> A. @@ -68,7 +68,7 @@ Proof. inversion v. exact a. - inversion v. + inversion v as [| n0 a H0 H1]. exact (f H0). Defined. @@ -85,7 +85,7 @@ Proof. induction n as [| n f]; intro v. exact Vnil. - inversion v. + inversion v as [| a n0 H0 H1]. exact (Vcons a n (f H0)). Defined. @@ -94,7 +94,7 @@ Proof. induction n as [| n f]; intros a v. exact (Vcons a 0 v). - inversion v. + inversion v as [| a0 n0 H0 H1 ]. exact (Vcons a (S n) (f a H0)). Defined. @@ -104,7 +104,7 @@ Proof. inversion v. exact (Vcons a 1 v). - inversion v. + inversion v as [| a n0 H0 H1 ]. exact (Vcons a (S (S n)) (f H0)). Defined. @@ -128,7 +128,7 @@ Proof. induction n as [| n f]; intros p v v0. simpl in |- *; exact v0. - inversion v. + inversion v as [| a n0 H0 H1]. simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). Defined. @@ -139,7 +139,7 @@ Proof. induction n as [| n g]; intro v. exact Vnil. - inversion v. + inversion v as [| a n0 H0 H1]. exact (Vcons (f a) n (g H0)). Defined. @@ -150,10 +150,35 @@ Proof. induction n as [| n h]; intros v v0. exact Vnil. - inversion v; inversion v0. + 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)). +Defined. + +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 @@ -164,14 +189,14 @@ 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). *) diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index b95b25fd..31ff029c 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: DecBool.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: DecBool.v 8866 2006-05-28 16:21:04Z herbelin $ i*) Set Implicit Arguments. -Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C := +Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C := if H then x else y. @@ -28,4 +28,4 @@ intros; case H; auto. intro; absurd A; trivial. Qed. -Unset Implicit Arguments.
\ No newline at end of file +Unset Implicit Arguments. |