X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=2ed7fcc868a9f1434e888f2f2400e365958ea130;hb=913512bbc9202f2109d53acd43dc8c0270b17184;hp=a1ffa3995f5f6c21251e8b38c34fe22c1c4b6373;hpb=471aadb252fa56a9d8fe484da01fdcff0d12814c;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a1ffa3995..2ed7fcc86 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.
 
 (*
@@ -65,12 +65,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,17 +79,24 @@ theorem nil_to_nil:  ∀A.∀l1,l2:list A.
 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
 qed.
 
-(* iterators *)
+(**************************** iterators ******************************)
 
 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+lemma map_append : ∀A,B,f,l1,l2.
+  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1
+[ #l2 @refl
+| #h #t #IH #l2 normalize //
+] qed.
   
 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  
 definition filter ≝ 
   λT.λp:T → bool.
-  foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
 
 (* compose f [a1;...;an] [b1;...;bm] = 
   [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
@@ -114,11 +115,45 @@ 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.
 
-let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
-match l1 with
-  [ nil ⇒ nil ?
-  | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
-  ].
+(**************************** 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 ******************************)
 
@@ -130,11 +165,19 @@ let rec length (A:Type[0]) (l:list A) on l ≝
 notation "|M|" non associative with precedence 60 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.
+
 (****************************** nth ********************************)
 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
   match n with
@@ -145,13 +188,110 @@ lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
 #A #a #i elim i normalize //
 qed.
 
+(****************************** nth_opt ********************************)
+let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
+match l with
+[ nil ⇒ None ?
+| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
+].
+
+(**************************** All *******************************)
+
+let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons h t ⇒ P h ∧ All A P t
+].
+
+lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
+#A #P #Q #H #l elim l normalize //
+#h #t #IH * /3/
+qed.
+
+lemma All_nth : ∀A,P,n,l.
+  All A P l →
+  ∀a.
+  nth_opt A n l = Some A a →
+  P a.
+#A #P #n elim n
+[ * [ #_ #a #E whd in E:(??%?); destruct
+    | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
+    ]
+| #m #IH *
+  [ #_ #a #E whd in E:(??%?); destruct
+  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
+  ]
+] qed.
+
+(**************************** Exists *******************************)
+
+let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ False
+| cons h t ⇒ (P h) ∨ (Exists A P t)
+].
+
+lemma Exists_append : ∀A,P,l1,l2.
+  Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
+#A #P #l1 elim l1
+[ normalize /2/
+| #h #t #IH #l2 *
+  [ #H /3/
+  | #H cases (IH l2 H) /3/
+  ]
+] qed.
+
+lemma Exists_append_l : ∀A,P,l1,l2.
+  Exists A P l1 → Exists A P (l1@l2).
+#A #P #l1 #l2 elim l1
+[ *
+| #h #t #IH *
+  [ #H %1 @H
+  | #H %2 @IH @H
+  ]
+] qed.
+
+lemma Exists_append_r : ∀A,P,l1,l2.
+  Exists A P l2 → Exists A P (l1@l2).
+#A #P #l1 #l2 elim l1
+[ #H @H
+| #h #t #IH #H %2 @IH @H
+] qed.
+
+lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
+#A #P #l1 #x #l2 elim l1
+[ normalize #H %2 @H
+| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
+qed.
+
+lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
+#A #P #l1 #x #l2 #H elim l1
+[ %1 @H
+| #h #t #IH %2 @IH
+] qed.
+
+lemma Exists_map : ∀A,B,P,Q,f,l.
+Exists A P l →
+(∀a.P a → Q (f a)) →
+Exists B Q (map A B f l).
+#A #B #P #Q #f #l elim l //
+#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
+
+lemma Exists_All : ∀A,P,Q,l.
+  Exists A P l →
+  All A Q l →
+  ∃x. P x ∧ Q x.
+#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
+qed.
+
 (**************************** fold *******************************)
 
 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
  match l with 
   [ nil ⇒ b 
-  | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
-      (fold A B op b p f l)].
+  | cons a l ⇒
+     if p a then op (f a) (fold A B op b p f l)
+     else fold A B op b p f l].
       
 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
   with precedence 80
@@ -228,3 +368,32 @@ lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 #A #n elim n -n /2/
 #n #IHn *; normalize /2/
 qed.
+
+(********************** find ******************************)
+let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
+match l with
+[ nil ⇒ None B
+| cons h t ⇒
+    match f h with
+    [ None ⇒ find A B f t
+    | Some b ⇒ Some B b
+    ]
+].
+
+(********************** position_of ******************************)
+let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
+match l with
+[ nil ⇒ None ?
+| cons h t ⇒
+   match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
+
+definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
+ λA,found,l. position_of_aux A found l 0.
+
+
+(********************** make_list ******************************)
+let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
+match n with
+[ O ⇒ [ ]
+| S m ⇒ a::(make_list A a m)
+].