X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist.ma;h=245a9fd3b4789818833887095b8db4cb1e04a1cf;hb=a5c551d0b7399f00e8eef3dfb06e2a0895eac3d4;hp=7d0c2ba13f2da25c065da05a332f3a7a8ba5bf49;hpb=601adf4ee553a77be1c55bc29159ed0e209500a1;p=helm.git

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 7d0c2ba13..245a9fd3b 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,8 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "basics/bool.ma".
-(* include "arithmetics/nat.ma". *)
+include "arithmetics/nat.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -31,12 +30,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 ≝
- λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝
+ λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ].
 
 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:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
+  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq //
 qed.
 
 (*
@@ -45,24 +44,24 @@ let rec id_list A (l: list A) on l :=
   [ nil => []
   | (cons hd tl) => hd :: id_list A tl ]. *)
 
-let rec append A (l1: list A) l2 on l1 ≝ 
+let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd :: append A tl l2 ].
+  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ].
 
-definition hd ≝ λA.λl: list A.λd:A.
+definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
-definition tail ≝  λA.λl: list A.
-  match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+definition tail ≝  λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  match l with [ nil ⇒  a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒  tl].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
 theorem associative_append: 
- ∀A.associative (list A) (append A).
+ ∀A.a href="cic:/matita/basics/relations/associative.def(1)"associative/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
 (* deleterio per auto 
@@ -71,41 +70,51 @@ ntheorem cons_append_commute:
     a :: (l1 @ l2) = (a :: l1) @ l2.
 //; nqed. *)
 
-theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/span class="autotactic"2span class="autotrace" trace trans_eq/span/span/ qed.
+theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))a title="append" href="cic:/fakeuri.def(1)"@/al1.span style="text-decoration: underline;"/spanspan class="autotactic"/span
+#A #a #l1 #l2 >a href="cic:/matita/basics/list/associative_append.def(4)"associative_append/a // qed.
 
-theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
-  l1@l2=[] → P (nil A) (nil A) → P l1 l2.
+theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/a] → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-theorem nil_to_nil:  ∀A.∀l1,l2:list A.
-  l1@l2 = [] → l1 = [] ∧ l2 = [].
-#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /span class="autotactic"2span class="autotrace" trace conj/span/span/
+theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
+#A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(4)"nil_append_elim/a A l1 l2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
 (* 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)].
+let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝
+ match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)].
   
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+lemma map_append : ∀A,B,f,l1,l2.
+  (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l1) a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f (l1a title="append" href="cic:/fakeuri.def(1)"@/al2).
+#A #B #f #l1 elim l1
+[ #l2 @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a
+| #h #t #IH #l2 normalize //
+] qed.
+
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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).
+  λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+  a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
 
-lemma filter_true : ∀A,l,a,p. p a = true → 
-  filter A p (a::l) = a :: filter A p l.
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1.
+
+lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-lemma filter_false : ∀A,l,a,p. p a = false → 
-  filter A p (a::l) = filter A p l.
+lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
 (*
@@ -115,28 +124,34 @@ match l1 with
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
   ]. *)
 
-(**************************** length ******************************
+(**************************** length *******************************)
 
-let rec length (A:Type[0]) (l:list A) on l ≝ 
+let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
   match l with 
-    [ nil ⇒ 0
-    | cons a tl ⇒ S (length A tl)].
+    [ nil ⇒ a title="natural number" href="cic:/fakeuri.def(1)"0/a
+    | cons a tl ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (length A tl)].
 
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
+lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A. 
+  a title="norm" href="cic:/fakeuri.def(1)"|/al1a title="append" href="cic:/fakeuri.def(1)"@/al2| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="norm" href="cic:/fakeuri.def(1)"|/al1|a title="natural plus" href="cic:/fakeuri.def(1)"+/aa title="norm" href="cic:/fakeuri.def(1)"|/al2|.
+#A #l1 elim l1 // normalize /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+let rec nth n (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (d:A)  ≝  
   match n with
-    [O ⇒ hd A l d
-    |S m ⇒ nth m A (tail A l) d].
+    [O ⇒ a href="cic:/matita/basics/list/hd.def(1)"hd/a A l d
+    |S m ⇒ nth m A (a href="cic:/matita/basics/list/tail.def(1)"tail/a A l) d].
 
-**************************** fold *******************************)
+(***************************** 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 ≝  
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a 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
@@ -149,37 +164,37 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
 theorem fold_true: 
-∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
-  \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
-    op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
-  \fold[op,nil]_{i ∈ l| p i} (f i).
+p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
-  \fold[op,nil]_{i ∈ l| p i} (f i) = 
-    \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)} (f i).
 #A #B #a #l #p #op #nil #f elim l //  
-#a #tl #Hind cases(true_or_false (p a)) #pa 
-  [ >filter_true // > fold_true // >fold_true //
-  | >filter_false // >fold_false // ]
+#a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa 
+  [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a //
+  | >a href="cic:/matita/basics/list/filter_false.def(3)"filter_false/a // >a href="cic:/matita/basics/list/fold_false.def(3)"fold_false/a // ]
 qed.
 
 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   {op :2> A → A → A; 
-   nill:∀a. op nil a = a; 
-   nilr:∀a. op a nil = a;
-   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+   nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; 
+   nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a;
+   assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c
   }.
 
-theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
-  op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
-    \fold[op,nil]_{i∈(I@J)} (f i).
+theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f.
+  op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
-  [>nill //|#a #tl #Hind <assoc //]
+  [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
 qed.
\ No newline at end of file