X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=a20a891089cb795ae88cdbe823a18d9a90096ebe;hb=b0d97cd7e2c50fb1fc2d50c86f3140e226b08a81;hp=40839b28fcf26fcf3abfe016fcb9b873a9ce19a1;hpb=596896aaf7158f90a96c3220e4a8f0a420f593d6;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 40839b28f..a20a89108 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -31,12 +31,12 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
 
 theorem nil_cons:
   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
-  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+  #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
 qed.
 
 (*
@@ -55,6 +55,11 @@ definition hd ≝ λA.λl: list A.λd:A.
 
 definition tail ≝  λA.λl: list A.
   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+  
+definition option_hd ≝ 
+  λA.λl:list A. match l with
+  [ nil ⇒ None ?
+  | cons a _ ⇒ Some ? a ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
@@ -65,12 +70,6 @@ theorem associative_append:
  ∀A.associative (list A) (append A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
-(* deleterio per auto 
-ntheorem cons_append_commute:
-  ∀A:Type.∀l1,l2:list A.∀a:A.
-    a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed. *)
-
 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
 #A #a #l #l1 >associative_append // qed.
 
@@ -85,6 +84,14 @@ theorem nil_to_nil:  ∀A.∀l1,l2:list A.
 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
 qed.
 
+lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
 (**************************** iterators ******************************)
 
 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
@@ -121,6 +128,46 @@ lemma filter_false : ∀A,l,a,p. p a = false →
 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:list S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (a::l2)
+  ]
+.
+
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a]. 
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2. 
+  rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 elim l1 normalize // 
+qed.
+
+lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+lemma reverse_append: ∀S,l1,l2. 
+  reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons // qed.
+
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append 
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l) 
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
+
 (**************************** length ******************************)
 
 let rec length (A:Type[0]) (l:list A) on l ≝ 
@@ -128,14 +175,148 @@ let rec length (A:Type[0]) (l:list A) on l ≝
     [ nil ⇒ 0
     | cons a tl ⇒ S (length A tl)].
 
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
+qed.
+
 lemma length_append: ∀A.∀l1,l2:list A. 
   |l1@l2| = |l1|+|l2|.
 #A #l1 elim l1 // normalize /2/
 qed.
 
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+lemma length_reverse: ∀A.∀l:list A. 
+  |reverse A l| = |l|.
+#A #l elim l // #a #l0 #IH >reverse_cons >length_append 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.
+  length ? l1 = length ? l2 →
+  (P [] []) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
+  P l1 l2.
+#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
+generalize in match Hl; generalize in match l2;
+elim l1
+[#l2 cases l2 // normalize #t2 #tl2 #H destruct
+|#t1 #tl1 #IH #l2 cases l2
+   [normalize #H destruct
+   |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
+]
+qed.
+
+lemma list_cases2 : 
+  ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
+  length ? l1 = length ? l2 →
+  (l1 = [] → l2 = [] → P) → 
+  (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
+[ #Pnil #Pcons @Pnil //
+| #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
+(*********************** properties of append ***********************)
+lemma append_l1_injective : 
+  ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
+#a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @eq_f /2/
+qed.
+  
+lemma append_l2_injective : 
+  ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
+#a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) normalize //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /2/
+qed.
+
+lemma append_l1_injective_r :
+  ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
+>reverse_append >reverse_append #Heq1
+lapply (append_l2_injective … Heq1) [ // ] #Heq2
+lapply (eq_f … (reverse ?) … Heq2) //
+qed.
+  
+lemma append_l2_injective_r : 
+  ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
+>reverse_append >reverse_append #Heq1
+lapply (append_l1_injective … Heq1) [ // ] #Heq2
+lapply (eq_f … (reverse ?) … Heq2) //
+qed.
+
+lemma length_rev_append: ∀A.∀l,acc:list A. 
+  |rev_append ? l acc| = |l|+|acc|.
+#A #l elim l // #a #tl #Hind normalize 
+#acc >Hind normalize // 
+qed.
+
+(****************************** mem ********************************)
+let rec mem A (a:A) (l:list A) on l ≝
+  match l with
+  [ nil ⇒ False
+  | cons hd tl ⇒ a=hd ∨ mem A a tl
+  ]. 
+
+(***************************** split *******************************)
+let rec split_rev A (l:list A) acc n on n ≝ 
+  match n with 
+  [O ⇒ 〈acc,l〉
+  |S m ⇒ match l with 
+    [nil ⇒ 〈acc,[]〉
+    |cons a tl ⇒ split_rev A tl (a::acc) m
+    ]
+  ].
+  
+definition split ≝ λA,l,n.
+  let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
+
+lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
+  |\fst (split_rev A l acc n)| = n+|acc|.
+#A #n elim n // #m #Hind *
+  [normalize #acc #Hfalse @False_ind /2/
+  |#a #tl #acc #Hlen normalize >Hind 
+    [normalize // |@le_S_S_to_le //]
+  ]
+qed.
+
+lemma split_len: ∀A,n,l. n ≤ |l| →
+  |\fst (split A l n)| = n.
+#A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
+normalize >length_reverse  >(split_rev_len … [ ] Hlen) normalize //
+qed.
+  
+lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| → 
+  reverse ? acc@ l = 
+    reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
+ #A #n elim n //
+ #m #Hind * 
+   [#acc whd in ⊢ ((??%)→?); #False_ind /2/ 
+   |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append 
+    @(Hind tl) @le_S_S_to_le @Hlen
+   ]
+qed.
+ 
+lemma split_eq: ∀A,n,l. n ≤ |l| → 
+  l = (\fst (split A l n))@(\snd (split A l n)).
+#A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
+>(split_rev_eq … Hlen) normalize 
+>(eq_pair_fst_snd ?? (split_rev A l [] n)) %
+qed.
+
+lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| → 
+  ∃l1,l2. l = l1@l2 ∧ |l1| = n.
+#A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
+@(ex_intro … (\snd (split A l n))) % /2/
+qed.
+  
 (****************************** nth ********************************)
 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
   match n with
@@ -323,7 +504,7 @@ lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
 qed.
 
 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
-#A #n elim n -n /2/
+#A #n elim n -n // 
 #n #IHn *; normalize /2/
 qed.