X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fvectors.ma;h=2ab0a87b1c32e1e5ac9be7141d537dada65dfa36;hb=7c9d99dfb049d726491b71f07ba6a9b088b30166;hp=677deb7260cacd2195af4c8a141c683d7e599391;hpb=d183f23928164d2de911298f5f2232be54e49300;p=helm.git

diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
index 677deb726..2ab0a87b1 100644
--- a/matita/matita/lib/basics/vectors.ma
+++ b/matita/matita/lib/basics/vectors.ma
@@ -9,13 +9,16 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-include "basics/finset.ma".
+include "basics/lists/list.ma".
 
 record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
 { vec :> list A;
   len: length ? vec = n
 }.
 
+lemma Vector_of_list ≝ λA,l. 
+  mk_Vector A (|l|) l (refl ??).
+
 lemma Vector_eq : ∀A,n,v1,v2.
   vec A n v1 = vec A n v2 → v1 = v2.
 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1; 
@@ -41,12 +44,57 @@ lemma vec_expand: ∀A,n,v.
 #A #n * #l cases l [normalize in ⊢ (%→?); #H destruct  |//]
 qed.
 
+lemma vector_nil: ∀A.∀v:Vector A 0. 
+  v = mk_Vector A 0 (nil A) (refl ??).
+#A * * // #a #tl normalize #H destruct
+qed. 
+
 definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
 mk_Vector A (n1+n2) (v1@v2).
 
 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
 mk_Vector B n (map ?? f v) 
   (trans_eq … (length_map …) (len A n v)).
+  
+lemma nth_default : ∀A,i,n.∀v:Vector A n.∀d1,d2. i < n →
+  nth i ? v d1 = nth i ? v d2.
+#A #i elim i -i
+  [#n #v #d1 #d2 #ltOn lapply v @(lt_O_n_elim … ltOn)
+   -v #m #v >(vec_expand … v) //
+  |#i #Hind #n #v #d1 #d2 #ltn lapply ltn lapply v @(lt_O_n_elim … (ltn_to_ltO … ltn))
+   -v -ltn #m #v #ltim >(vec_expand … v) @(Hind m (vec_tail A (S m) v) d1 d2 ?) 
+   @le_S_S_to_le //
+  ]
+qed.
+  
+lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d. 
+  (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
+#A #n elim n -n 
+  [#v1 #v2 #H >(vector_nil A v1) >(vector_nil A v2) //
+  |#n #Hind #v1 #v2 #d #H >(vec_expand … v1) >(vec_expand … v2)
+   >(Hind (vec_tail … v1) (vec_tail … v2) d)
+    [cut (vec_hd A n v1 = vec_hd A n v2) //
+     cut (∀i,d1,d2. i < S n → nth i A v1 d1 = nth i A v2 d2)
+       [#i #d1 #d2 #Hi >(nth_default ????? d) // >(nth_default ???? d2 d) // @H //]
+     -H #H @(H 0) //  
+    |#i #ltin @(H (S i)) @le_S_S //
+    ]
+  ]
+qed.
+
+lemma nth_vec_map :
+  ∀A,B,f,i,n.∀v:Vector A n.∀d.
+  f (nth i ? v d) = nth i ? (vec_map A B f n v) (f d).
+#A #B #f #i elim i
+[ *
+  [ #v #d >(vector_nil … v) %
+  | #n0 #v #d >(vec_expand … v) % ]
+| #i0 #IH *
+  [ #v #d >(vector_nil … v) normalize cases i0 // 
+  | #n #v #d >(vec_expand … v) whd in ⊢ (??(?%)%);
+    >(IH n (vec_tail A (S n) v) d) % ] ]
+qed.
+
 
 (* mapi: map with index to move in list.ma *)
 let rec change_vec (A:Type[0]) (n:nat) on n ≝
@@ -82,79 +130,58 @@ lemma nth_change_vec_neq : ∀A,j,i,n,v,a,d. i ≠ j →
   ]
 qed.
 
+lemma change_vec_same : ∀sig,n,v,i,d.
+  change_vec sig n v (nth i ? v d) i = v.
+#sig #n #v #i #d @(eq_vec … d)
+#i0 #Hi0 cases (decidable_eq_nat i i0) #Hi0
+[ >Hi0 >nth_change_vec //
+| >nth_change_vec_neq //
+]
+qed.
+
 lemma change_vec_cons_tail :∀A,n,vA,a,b,i.
   change_vec A (S n) (vec_cons ? a n vA) b (S i) =
   vec_cons ? a n (change_vec A n vA b i).
 #A #n #vA cases vA //
 qed.
 
-lemma vector_nil: ∀A.∀v:Vector A 0. 
-  v = mk_Vector A 0 (nil A) (refl ??).
-#A * * // #a #tl normalize #H destruct
-qed. 
-
-lemma nth_default : ∀A,i,n.∀v:Vector A n.∀d1,d2. i < n →
-  nth i ? v d1 = nth i ? v d2.
-#A #i elim i -i
-  [#n #v #d1 #d2 #ltOn lapply v @(lt_O_n_elim … ltOn)
-   -v #m #v >(vec_expand … v) //
-  |#i #Hind #n #v #d1 #d2 #ltn lapply ltn lapply v @(lt_O_n_elim … (ltn_to_ltO … ltn))
-   -v -ltn #m #v #ltim >(vec_expand … v) @(Hind m (vec_tail A (S m) v) d1 d2 ?) 
-   @le_S_S_to_le //
+lemma change_vec_commute : ∀A,n,v,a,b,i,j. i ≠ j → 
+  change_vec A n (change_vec A n v a i) b j
+  = change_vec A n (change_vec A n v b j) a i.
+#A #n #v #a #b #i #j #Hij @(eq_vec … a)
+#k #Hk cases (decidable_eq_nat k i) #Hki
+[ >Hki >nth_change_vec // >(nth_change_vec_neq ??????? (sym_not_eq … Hij))
+  >nth_change_vec //
+| cases (decidable_eq_nat k j) #Hkj
+  [ >Hkj >nth_change_vec // >(nth_change_vec_neq ??????? Hij) >nth_change_vec //
+  | >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
+    >(nth_change_vec_neq ??????? (sym_not_eq … Hkj))
+    >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
+    >(nth_change_vec_neq ??????? (sym_not_eq … Hkj)) //
   ]
+]
 qed.
-  
-lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d. 
-  (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
-#A #n elim n -n 
-  [#v1 #v2 #H >(vector_nil A v1) >(vector_nil A v2) //
-  |#n #Hind #v1 #v2 #d #H >(vec_expand … v1) >(vec_expand … v2)
-   >(Hind (vec_tail … v1) (vec_tail … v2) d)
-    [cut (vec_hd A n v1 = vec_hd A n v2) //
-     cut (∀i,d1,d2. i < S n → nth i A v1 d1 = nth i A v2 d2)
-       [#i #d1 #d2 #Hi >(nth_default ????? d) // >(nth_default ???? d2 d) // @H //]
-     -H #H @(H 0) //  
-    |#i #ltin @(H (S i)) @le_S_S //
-    ]
-  ]
-qed.
-
-(*
-lemma length_make_listi: ∀A,a,n,i. 
-  |make_listi A a n i| = n.
-#A #a #n elim n // #m #Hind normalize //
-qed.
-definition change_vec ≝ λA,n,v,a,i.
-  make_veci A (λj.if (eqb i j) then a else (nth j A v a)) n 0.
-
-let rec mapi (A,B:Type[0]) (f: nat → A → B) (l:list A) (i:nat) on l: list B ≝
- match l with 
- [ nil ⇒ nil ? 
- | cons x tl ⇒ f i x :: (mapi A B f tl (S i))].
- 
-lemma length_mapi: ∀A,B,l.∀f:nat→A→B.∀i. 
-  |mapi ?? f l i| = |l|.
-#A #B #l #f elim l // #a #tl #Hind normalize //
-qed.
-
-let rec make_listi (A:Type[0]) (a:nat→A) (n,i:nat) on n : list A ≝
-match n with
-[ O ⇒ [ ]
-| S m ⇒ a i::(make_listi A a m (S i))
-].
 
-lemma length_make_listi: ∀A,a,n,i. 
-  |make_listi A a n i| = n.
-#A #a #n elim n // #m #Hind normalize //
+lemma change_vec_change_vec : ∀A,n,v,a,b,i. 
+  change_vec A n (change_vec A n v a i) b i = change_vec A n v b i.
+#A #n #v #a #b #i @(eq_vec … a) #i0 #Hi0
+cases (decidable_eq_nat i i0) #Hii0
+[ >Hii0 >nth_change_vec // >nth_change_vec //
+| >nth_change_vec_neq // >nth_change_vec_neq //
+  >nth_change_vec_neq // ]
 qed.
 
-definition vec_mapi ≝ λA,B.λf:nat→A→B.λn.λv:Vector A n.λi.
-mk_Vector B n (mapi ?? f v i) 
-  (trans_eq … (length_mapi …) (len A n v)).
-  
-definition make_veci ≝ λA.λa:nat→A.λn,i.
-mk_Vector A n (make_listi A a n i) (length_make_listi A a n i).
-*)
+lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d.
+  nth i ? v2 d = t → 
+  (∀j.i ≠ j → nth j ? v1 d = nth j ? v2 d) → 
+  v2 = change_vec ?? v1 t i.
+#sig #n #v1 #v2 #i #t #d #H1 #H2 @(eq_vec … d)
+#i0 #Hlt cases (decidable_eq_nat i0 i) #Hii0
+[ >Hii0 >nth_change_vec //
+| >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ]
+qed-.
+
+(* map *) 
 
 let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
    match l1 with
@@ -192,4 +219,4 @@ lemma pmap_change : ∀A,B,C,f,n,vA,vB,a,b,i.
 #A #B #C #f #n elim n //
 #m #Hind #vA #vB #a #b >(vec_expand … vA) >(vec_expand … vB) * //
 #i >pmap_vec_cons >pmap_vec_cons >change_vec_cons_tail @eq_f @Hind 
-qed.
+qed.
\ No newline at end of file