From ffaa382ed26728fb810522cea42c19bc92fad75f Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 27 Apr 2006 08:32:01 +0000 Subject: 2-3 lemmes en plus pour que les Bvectors soient effectivement utilisables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8744 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bvector.v | 73 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 49 insertions(+), 24 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 944485971..eafc1fabb 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -18,32 +18,32 @@ 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. @@ -154,6 +154,31 @@ Proof. exact (Vcons (g a a0) n (h H0 H2)). Defined. +Definition Vid : forall n:nat, vector n -> vector n. +Proof. +destruct n; intros. +exact Vnil. +exact (Vcons (Vhead _ H) _ (Vtail _ H)). +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). *) -- cgit v1.2.3