\ / 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;
]
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
#A #n #vA cases vA //
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 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 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