X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fvectors.ma;h=e680e91a7170a48ce231d9c4408f7028f2bbe2e8;hb=2b51cf74b9a5f37d0f91780ceae4b8f4d0ee38a1;hp=be90270e05ba1cc35ae059d737dc5c442a72f8a6;hpb=aa0fefefb9a2911739877f20897e00e16f7d3fd7;p=helm.git

diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
index be90270e0..e680e91a7 100644
--- a/matita/matita/lib/basics/vectors.ma
+++ b/matita/matita/lib/basics/vectors.ma
@@ -79,6 +79,20 @@ lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d.
   ]
 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 ≝
 match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
@@ -128,6 +142,33 @@ lemma change_vec_cons_tail :∀A,n,vA,a,b,i.
 #A #n #vA cases vA //
 qed.
 
+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 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.
+
+
 (*
 lemma length_make_listi: ∀A,a,n,i. 
   |make_listi A a n i| = n.