diff options
Diffstat (limited to 'theories/Bool/Bvector.v')
-rw-r--r-- | theories/Bool/Bvector.v | 136 |
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. |