aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Bvector.v136
1 files changed, 97 insertions, 39 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index d4d8386c4..e48dd9a5b 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -25,10 +25,10 @@ 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.
+peu les inductions structurelles et dans certains cas on
+utilisera un terme de preuve comme définition, car le
+mécanisme d'inférence du type du filtrage n'est pas toujours
+aussi puissant que celui implanté par les tactiques d'élimination.
*)
Section VECTORS.
@@ -52,39 +52,88 @@ Inductive vector : nat -> Type :=
| Vnil : vector 0
| Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
-Definition Vhead : forall n:nat, vector (S n) -> A.
-Proof.
- intros n v; inversion v; exact a.
-Defined.
+Definition Vhead (n:nat) (v:vector (S n)) :=
+ match v with
+ | Vcons a _ _ => a
+ end.
-Definition Vtail : forall n:nat, vector (S n) -> vector n.
-Proof.
- intros n v; inversion v as [|_ n0 H0 H1]; exact H0.
-Defined.
+Definition Vtail (n:nat) (v:vector (S n)) :=
+ match v with
+ | Vcons _ _ v => v
+ end.
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).
Defined.
-Definition Vconst : forall (a:A) (n:nat), vector n.
-Proof.
- induction n as [| n v].
- exact Vnil.
+(* This works...
- exact (Vcons a n v).
-Defined.
+Notation "'!rew' a -> b [ Heq ] 'in' t" := (eq_rect a _ t b Heq)
+ (at level 10, a, b at level 80).
+
+Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
+ match v with
+ | Vnil => I
+ | Vcons a n v =>
+ match v in vector q return n=q -> A with
+ | Vnil => fun _ => a
+ | Vcons _ q _ => fun Heq => Vlast q (!rew n -> (S q) [Heq] in v)
+ end (refl_equal n)
+ end.
+*)
+
+(* Remarks on the definition of Vlast...
+
+(* The ideal version... still now accepted, even with Program *)
+Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
+ match v with
+ | Vnil => I
+ | Vcons a _ Vnil => a
+ | Vcons a n v => Vlast (pred n) v
+ end.
+
+(* This version does not work because Program Fixpoint expands v with
+ violates the guard condition *)
+
+Program Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
+ match v in vector p return match p with O => True | _ => A end with
+ | Vnil => I
+ | Vcons a _ Vnil => a
+ | Vcons a _ (Vcons _ n _ as v) => Vlast n v
+ end.
+
+(* This version works *)
+
+Program Fixpoint Vlast (n:nat) (v:vector (S n)) { struct v } : A :=
+ match v in vector p return match p with O => True | _ => A end with
+ | Vnil => I
+ | Vcons a n v =>
+ match v with
+ | Vnil => a
+ | Vcons _ q _ => Vlast q v
+ end
+ end.
+*)
+
+Fixpoint Vconst (a:A) (n:nat) :=
+ match n return vector n with
+ | O => Vnil
+ | S n => Vcons a _ (Vconst a n)
+ end.
+
+(** Shifting and truncating *)
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)).
Defined.
@@ -123,28 +172,35 @@ Proof.
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)).
-Defined.
+(** Concatenation of two vectors *)
+
+Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) :=
+ match v with
+ | Vnil => w
+ | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w)
+ end.
+
+(** Uniform application on the arguments of the vector *)
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)).
-Defined.
+Fixpoint Vunary n (v:vector n) : vector n :=
+ match v with
+ | Vnil => Vnil
+ | Vcons a n' v' => Vcons (f a) n' (Vunary n' v')
+ end.
Variable g : A -> A -> A.
+(* Would need to have the constraint n = n' ...
+
+Fixpoint Vbinary n (v w:vector n) : vector n :=
+ match v, w with
+ | Vnil, Vnil => Vnil
+ | Vcons a n' v', Vcons b _ w' => Vcons (g a b) n' (Vbinary n' v' w')
+ end.
+*)
+
Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
Proof.
induction n as [| n h]; intros v v0.
@@ -154,14 +210,16 @@ Proof.
exact (Vcons (g a a0) n (h H0 H2)).
Defined.
+(** Eta-expansion of a vector *)
+
Definition Vid : forall n:nat, vector n -> vector n.
Proof.
- destruct n; intro X.
+ destruct n; intro v.
exact Vnil.
- exact (Vcons (Vhead _ X) _ (Vtail _ X)).
+ exact (Vcons (Vhead _ v) _ (Vtail _ v)).
Defined.
-Lemma Vid_eq : forall (n:nat) (v:vector n), v=(Vid n v).
+Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
Proof.
destruct v; auto.
Qed.