summaryrefslogtreecommitdiff
path: root/theories/Bool
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Bvector.v95
-rw-r--r--theories/Bool/DecBool.v6
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.