From f4fdd895e9c85986998dea3556dc596a3e548c51 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 17 Oct 2011 10:51:01 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 92 +++++++++++++++++++++++++++++-------- 1 file changed, 73 insertions(+), 19 deletions(-) diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index d7b6d4f1e..4ce43679d 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -2,10 +2,34 @@ include "tutorial/chapter2.ma". include "basics/bool.ma". +(* Matita supports polymorphic data types. The most typical case are polymorphic +lists, parametric in the type of their elements: *) + inductive list (A:Type[0]) : Type[0] := | nil: list A | 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, +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. + +Typical elements in (list bool) are for instance, + nil nat - the empty list of type nat + cons nat true (nil nat) - the list containing true + cons nat false (cons nat (true (nil nat))) - the list containing false and true +and so on. + +Note that both constructos nil and cons are expecting in input the type parameter - +in this case, bool. + +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. +*) + notation "hvbox(hd break :: tl)" right associative with precedence 47 for @{'cons $hd $tl}. @@ -21,48 +45,78 @@ notation "hvbox(l1 break @ l2)" interpretation "nil" 'nil = (nil ?). interpretation "cons" 'cons hd tl = (cons ? hd tl). -definition not_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/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: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]. - #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/tutorial/chapter3/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq // -qed. +(* 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 the append +function itself is polymorphic, and the first argument it takes in input is the type +A of the elements of two lists l1 and l2. +Moreover, since the append function takes in input several parameters, we must also +specify in the its defintion on which one of them we are recurring: in this case l1. +If not othewise specified, recursion is supposed to act on the first argument of the +function.*) let rec append A (l1: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) l2 on l1 ≝ match l1 with [ nil ⇒ l2 | cons hd tl ⇒ hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ]. -definition hd ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.λd:A. +interpretation "append" 'append l1 l2 = (append ? l1 l2). + +(* As usual, the function is executable. For instance, (append A nil l) reduces to +l, as shown by the following example: *) + +example nil_append: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a 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 l. +#A #l normalize // qed. + +(* Proving that l @ [] = l is just a bit more complex. The situation is exactly the +same as for the addition operation of the previous chapter: since append is defined +by recutsion over the first argument, the computation of l @ [] is stuck, and we must +proceed by induction on l *) + +lemma append_nil: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/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. + +(* similarly, we can define the two functions head and tail. We should decide what to do in +case the input list is empty. For tl, it is natural to return the empty list; for hd, we take +in input a default element d of type A to return in this case. *) + +definition head ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.λd:A. match l with [ nil ⇒ d | cons a _ ⇒ a]. definition tail ≝ λA.λl: a href="cic:/matita/tutorial/chapter3/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). +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)"=/a a. +#A #a #d #l normalize // qed. -theorem append_nil: ∀A.∀l:a href="cic:/matita/tutorial/chapter3/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. +(* 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. theorem associative_append: - ∀A.a href="cic:/matita/basics/relations/associative.def(1)"associative/a (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) (a href="cic:/matita/tutorial/chapter3/append.fix(0,1,1)"append/a A). +∀A.∀l1,l2,l3: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="append" href="cic:/fakeuri.def(1)"@/a l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l1 a title="append" href="cic:/fakeuri.def(1)"@/a (l2 a title="append" href="cic:/fakeuri.def(1)"@/a l3). #A #l1 #l2 #l3 (elim l1) normalize // qed. -(* qualcosa di strano qui 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 title="cons" href="cic:/fakeuri.def(1)"[/aa]) a title="append" href="cic:/fakeuri.def(1)"@/a l1. -/2/ qed. *) +(* Problemi con la notazione *) +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. -theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/tutorial/chapter3/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 title="nil" href="cic:/fakeuri.def(1)"[/a] a title="nil" href="cic:/fakeuri.def(1)"[/a] → P l1 l2. -#A #l1 #l2 #P (cases l1) normalize // -#a #l3 #heq destruct -qed. theorem 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 #l2 #isnil @(a href="cic:/matita/tutorial/chapter3/nil_append_elim.def(3)"nil_append_elim/a A l1 l2) /2/ qed. +definition not_nil: ∀A:Type[0].a href="cic:/matita/tutorial/chapter3/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: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]. +#A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/tutorial/chapter3/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq // +qed. + (* iterators *) let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a B ≝ -- 2.39.2