From: Andrea Asperti Date: Thu, 7 Feb 2013 09:15:07 +0000 (+0000) Subject: A few integrations X-Git-Tag: make_still_working~1264 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fce70f3556b1b8eab9655006fe2e6928948f3a99;p=helm.git A few integrations --- diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index 8a41a15dc..a4ba4cce1 100644 --- 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 a48f04d0f..a2b7c0186 100644 --- 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