From: matitaweb Date: Wed, 7 Mar 2012 11:37:19 +0000 (+0000) Subject: Sections X-Git-Tag: make_still_working~1881 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=15d44a1a9b0d9817434e014aeaa9615161b30e0c Sections --- diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index 3d7eb7a56..51b810bee 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -1,3 +1,6 @@ +(* +h1 class="section"Polymorphism and Higher Order/h1 +*) include "tutorial/chapter2.ma". include "basics/bool.ma". @@ -24,7 +27,10 @@ and so on. Note that both constructos nil and cons are expecting in input the type parameter: in this case, bool. +*) +(* +h2 class="section"Defining your own notation/h2 We now add a bit of notation, in order to make the syntax more readable. In particular, we would like to write [] instead of (nil A) and a::l instead of (cons A a l), leaving the system the burden to infer A, whenever possible. @@ -45,7 +51,9 @@ notation "hvbox(l1 break @ l2)" interpretation "nil" 'nil = (nil ?). interpretation "cons" 'cons hd tl = (cons ? hd tl). -(* Let us define a few basic functions over lists. Our first example is the +(* +h2 class="section"Basic operations on lists/h2 +Let us define a few basic functions over lists. Our first example is the append function, concatenating two lists l1 and l2. The natural way is to proceed by recursion on l1: if it is empty the result is simply l2, while if l1 = hd::tl then we recursively append tl and l2 , and then add hd as first element. Note that @@ -91,7 +99,6 @@ definition tail ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1, example ex_head: ∀A.∀a,d,l. a href="cic:/matita/tutorial/chapter3/head.def(1)"head/a A (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) d a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/spanspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/span a. #A #a #d #l normalize // qed. -(* Problemi con la notazione *) example ex_tail: a href="cic:/matita/tutorial/chapter3/tail.def(1)"tail/a ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/a ? a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a]. normalize // qed. @@ -133,7 +140,9 @@ and l2 just requires a trivial induction on the first list. *) a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? (l1a title="append" href="cic:/fakeuri.def(1)"@/al2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? l1) (a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"length/a ? l2). #A #l1 elim l1 normalize // qed. -(* Let us come to a more interesting question. How can we prove that the empty +(* +h2 class="section"Comparing Costructors/h2 +Let us come to a more interesting question. How can we prove that the empty list is different from any list with at least one element, that is from any list of the kind (a::l)? We start defining a simple predicate stating if a list is empty or not. The predicate is computed by inspection over the list *) @@ -172,7 +181,9 @@ lemma nil_to_nil: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind 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 /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 +(* +h2 class="section"Higher Order Functionals/h2 +Let us come to some important, higher order, polymorphic functionals acting over lists. A typical example is the map function, taking a function f:A → B, a list l = [a1; a2; ... ; an] and returning the list [f a1; f a2; ... ; f an]. *) @@ -218,7 +229,9 @@ of type A → list B → list B is the function mapping a and l to (f a)::l. definition map_again ≝ λA,B,f,l. a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a A (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a B) (λa,l.f aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="nil" href="cic:/fakeuri.def(1)"[/a] l. -(* Can we prove that map_again is "the same" as map? We should first of all +(* +h2 class="section"Extensional equality/h2 +Can we prove that map_again is "the same" as map? We should first of all clarify in which sense we expect the two functions to be equal. Equality in Matita has an intentional meaning: it is the smallest predicate induced by convertibility, i.e. syntactical equality up to normalization. From an @@ -251,9 +264,9 @@ inductive types; again the rest of the proof is trivial. *) #l (elim l) normalize // qed. -(**************************** BIGOPS *******************************) - -(* Building a library of basic functions, it is important to achieve a +(* +h2 class="section"Big Operators/h2 +Building a library of basic functions, it is important to achieve a good degree of abstraction and generality, in order to be able to reuse suitable instances of the same function in different context. This has not only the obvious benefit of factorizing code, but especially to avoid