Made a copy of basics/list.ma as a base for chapter 3.

diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma
new file mode 100644 (file)
index 0000000..14f7aaa
--- /dev/null
+++ b/weblib/tutorial/chapter3.ma
@@ -0,0 +1,186 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+include "basics/bool.ma".
+(* include "arithmetics/nat.ma". *)
+
+inductive list (A:Type[0]) : Type[0] :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+ λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
+
+theorem nil_cons:
+  ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+  #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
+qed.
+
+(*
+let rec id_list A (l: list A) on l :=
+  match l with
+  [ nil => []
+  | (cons hd tl) => hd :: id_list A tl ]. *)
+
+let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
+
+definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒  tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+#A #l (elim l) normalize // qed.
+
+theorem associative_append: 
+ ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 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\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a])\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
+/2/ qed.
+
+theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
+  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+#A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(3)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /2/
+qed.
+
+(* iterators *)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
+ match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (map A B f tl)].
+  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 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 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+  \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p x) (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
+
+lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → 
+  \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 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
+  ]. *)
+
+(**************************** length ******************************
+
+let rec length (A:Type[0]) (l:list A) on l ≝ 
+  match l with 
+    [ nil ⇒ 0
+    | cons a tl ⇒ S (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)  ≝  
+  match n with
+    [O ⇒ hd A l d
+    |S m ⇒ nth m A (tail A l) d].
+
+**************************** fold *******************************)
+
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
+ match l with 
+  [ nil ⇒ b 
+  | cons a l ⇒ \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p a) (op (f a) (fold A B op b p f l))
+      (fold A B op b p f l)].
+      
+notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
+
+notation "\fold [ op , nil ]_{ident i ∈ l } f"
+  with precedence 80
+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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
+  \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+    op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[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 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+  \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[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.
+  \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+    \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)} (f i).
+#A #B #a #l #p #op #nil #f elim l //  
+#a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa 
+  [ >\ 5a href="cic:/matita/basics/list/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 // > \ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 //
+  | >\ 5a href="cic:/matita/basics/list/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
+qed.
+
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+  {op :2> A → A → A; 
+   nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a; 
+   nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
+   assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
+  }.
+
+theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
+  op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+    \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
+#A #B #I #J #nil #op #f (elim I) normalize 
+  [>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
+qed.
+