X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter3.ma;h=20e545e37cff1a6fa90ef11852151c25bebdfa28;hb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;hp=ca7e89355b9e9bf5fcf98d772056a4c5b6a50dd3;hpb=83aea9a1662de32505512d6296921ebfffcfc53d;p=helm.git diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index ca7e89355..20e545e37 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -1,4 +1,3 @@ - include "tutorial/chapter2.ma". include "basics/bool.ma". @@ -10,11 +9,11 @@ inductive list (A:Type[0]) : Type[0] ≝ | cons: A -> list A -> list A. (* The type notation list A is the type of all lists with elements of type A: it is -defined by tow constructors: a polymorphic empty list (nil A) and a cons operation, +defined by two constructors: a polymorphic empty list (nil A) and a cons operation, adding a new head element of type A to a previous list. For instance, (list nat) and and (list bool) are lists of natural numbers and booleans, respectively. But we can -also form more complex data typea, like (list (list (nat → nat))), that is a list whose -elements are lists of functions from natural number to natural numbers. +also form more complex data types, like (list (list (nat → nat))), that is a list whose +elements are lists of functions from natural numbers to natural numbers. Typical elements in (list bool) are for instance, nil nat - the empty list of type nat @@ -100,9 +99,12 @@ theorem associative_append: #A #l1 #l2 #l3 (elim l1) normalize // qed. (* Problemi con la notazione *) +lemma a_append: ∀A.∀a.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a 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)"@/a l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a aa title="cons" href="cic:/fakeuri.def(1)":/a:l. +// qed. + theorem append_cons: ∀A.∀a:A.∀l,l1: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.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 (l a title="append" href="cic:/fakeuri.def(1)"@/a (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a a title="nil" href="cic:/fakeuri.def(1)"[/a])) a title="append" href="cic:/fakeuri.def(1)"@/a l1. -/2/ qed. +// qed. (* Other typical functions over lists are those computing the length of a list, and the function returning the nth element *) @@ -114,7 +116,7 @@ match l with 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 ⇒ a href="cic:/matita/tutorial/chapter3/hd.def(1)"hd/a A l d + [O ⇒ a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A l d |S m ⇒ nth m A (a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a A l) d]. example ex_length: a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a. @@ -142,7 +144,7 @@ definition is_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/list.ind( authorized to add P to your hypothesis: *) lemma neg_aux : ∀P:Prop. (P → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP) → a title="logical not" href="cic:/fakeuri.def(1)"¬/aP. -#P #PtonegP % /3/ qed. +#P #PtonegP % /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. theorem diff_cons_nil: ∀A:Type[0].∀l:a href="cic:/matita/tutorial/chapter3/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]. @@ -166,7 +168,7 @@ to solve the absurd case. *) lemma nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a span style="text-decoration: underline;"/spanA. 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 cases l1 normalize /2/ #a #tl #l2 #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ qed. +#A #l1 cases l1 normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ #a #tl #l2 #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ qed. (* Let us come to some important, higher order, polymorphic functionals acting over lists. A typical example is the map function, taking a function @@ -258,7 +260,7 @@ A really convenient tool is the following combination of fold and filter, that essentially allow you to iterate on every subset of a given enumerated (finite) type, represented as a list. *) - 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 ≝ + 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)" title="null"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))