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

1 files changed, 49 insertions, 24 deletions

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).
 *)