A few integrations

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 8a41a15dc7a4e9a82490967b4aee8d9901552165..a4ba4cce1ee217651b21a3779204aa3637185af0 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -92,6 +92,15 @@ lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
 #A #a1 #a2 #l1 #l2 #Heq destruct //
 qed.
 
+(* option cons *)
+
+definition option_cons ≝ λsig.λc:option sig.λl.
+  match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
+
+lemma opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l). 
+#A * //
+qed.
+
 (* comparing lists *)
 
 lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 → 
@@ -199,6 +208,10 @@ lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
 #A #l elim l // 
 qed.
 
+lemma length_tail1 : ∀A,l.0 < |l| → |tail A l| < |l|.
+#A * normalize //
+qed.
+
 lemma length_append: ∀A.∀l1,l2:list A. 
   |l1@l2| = |l1|+|l2|.
 #A #l1 elim l1 // normalize /2/
@@ -218,6 +231,19 @@ lemma lenght_to_nil: ∀A.∀l:list A.
 #A * // #a #tl normalize #H destruct
 qed.
  
+lemma lists_length_split : 
+ ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
+#A #l1 elim l1
+[ #l2 %{[ ]} %{l2} % % %
+| #hd1 #tl1 #IH *
+  [ %{[ ]} %{(hd1::tl1)} %2 % %
+  | #hd2 #tl2 cases (IH tl2) #x * #y *
+    [ * #IH1 #IH2 %{(hd2::x)} %{y} % normalize % //
+    | * #IH1 #IH2 %{(hd1::x)} %{y} %2 normalize % // ]
+  ]
+]
+qed.
+
 (****************** traversing two lists in parallel *****************)
 lemma list_ind2 : 
   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.

diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
index a48f04d0fe8dbbfa585262f441fd76a5e78d7c72..a2b7c0186440434fb708a7d570425756480aec0e 100644 (file)
--- a/matita/matita/lib/basics/vectors.ma
+++ b/matita/matita/lib/basics/vectors.ma
@@ -171,43 +171,17 @@ cases (decidable_eq_nat i i0) #Hii0
   >nth_change_vec_neq // ]
 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 //
-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