From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 14 Oct 2011 10:44:57 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~2186
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=582f4274392187a0cc867ac5f4913ff758010dcd;p=helm.git

commit by user andrea
---

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
index bd5d17297..cafb85323 100644
--- a/weblib/tutorial/chapter3.ma
+++ b/weblib/tutorial/chapter3.ma
@@ -1,3 +1,5 @@
+
+include "tutorial/chapter2.ma".
 include "basics/bool.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
@@ -81,8 +83,10 @@ lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/f
   a href="cic:/matita/tutorial/chapter3/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/tutorial/chapter3/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 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.
+*)
 
 (*
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
@@ -91,21 +95,21 @@ 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/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l ≝ 
   match l with 
-    [ nil ⇒ 0
-    | cons a tl ⇒ S (length A tl)].
+    [ nil ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a
+    | cons a tl ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (length A tl)].
 
-let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
+let rec nth n (A:Type[0]) (l:a href="cic:/matita/tutorial/chapter3/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/tutorial/chapter3/hd.def(1)"hd/a A l d
+    |S m ⇒ nth m A (a href="cic:/matita/tutorial/chapter3/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→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 ≝  
+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/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l :B ≝  
  match l with 
   [ nil ⇒ b 
   | cons a l ⇒ a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p a) (op (f a) (fold A B op b p f l))
@@ -136,11 +140,11 @@ p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic
 theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
   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 title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/tutorial/chapter3/filter.def(2)"filter/a A p l)} (f i).
 #A #B #a #l #p #op #nil #f elim l //  
 #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 // ]
+  [ >a href="cic:/matita/tutorial/chapter3/filter_true.def(3)"filter_true/a // > a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"fold_true/a // >a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"fold_true/a //
+  | >a href="cic:/matita/tutorial/chapter3/filter_false.def(3)"filter_false/a // >a href="cic:/matita/tutorial/chapter3/fold_false.def(3)"fold_false/a // ]
 qed.
 
 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
@@ -150,9 +154,9 @@ record Aop (A:Type[0]) (nil:A) : Type[0] ≝
    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: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.
+theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/tutorial/chapter3/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 
-  [>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 //]
+  [>a href="cic:/matita/tutorial/chapter3/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/tutorial/chapter3/assoc.fix(0,2,2)"assoc/a //]
 qed.
\ No newline at end of file