From 381f6cd5749cf11e7cffb1bcd206c8318ddf8e51 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 19 Oct 2011 07:09:27 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 42 +++++++++++++++++++++++++++---------- 1 file changed, 31 insertions(+), 11 deletions(-) diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index 849b067e7..a75b4ce1e 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -5,7 +5,7 @@ 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] := +inductive list (A:Type[0]) : Type[0] ≝ | nil: list A | cons: A -> list A -> list A. @@ -77,9 +77,10 @@ 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. *) +(* similarly, we can define the two functions head and tail. Since we can only define +total functions, 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]. @@ -122,7 +123,10 @@ normalize // qed. example ex_nth: a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"nth/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) ? (a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"cons/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) (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 href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a. normalize // qed. -lemma length_add: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. +(* Proving that the length of l1@l2 is the sum of the lengths of l1 +and l2 just requires a trivial induction on the first list. *) + + lemma length_add: ∀A.∀l1,l2:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A. 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. @@ -164,18 +168,26 @@ 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 /2/ #a #tl #l2 #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/ qed. -(* iterators *) +(* 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]. *) 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 ≝ match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)]. - -let rec foldr (A,B:Type[0]) (f:A → B → B) (b: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 ⇒ f a (foldr A B f b l)]. - + +(* Another simple example is the filter function that given a list l: list A and +a boolean test p:A → bool returns the sublist of elements satisfying the test. *) + definition filter ≝ λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a T) (λx,l0.a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p x) (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) l0) a title="nil" href="cic:/fakeuri.def(1)"[/a]. +(* Here are a couple of simple lemmas on the behaviour of the filter function. +It is often convenient to state such lemmas, in order to be able to use rewriting +as an alternative to reduction in proofs: reduction is a bit difficult to control. +*) + lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 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 a title="cons" 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 // qed. @@ -184,6 +196,13 @@ 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. +(* The most typical list iterator is the fold function, that taken +a list l = [a1; a2; ... an], a base value b, and a function f: A → B → B +returns f a1 (f a2 (... (f an b)...)). *) + +let rec foldr (A,B:Type[0]) (f:A → B → B) (b: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 ⇒ f a (foldr A B f b l)]. + 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/tutorial/chapter3/map.fix(0,3,1)"map/a span style="text-decoration: underline;"/spanA B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B g l. #A #B #f #g #l #eqfg (elim l) normalize // qed. @@ -246,4 +265,5 @@ theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/tutorial/chapter3/list.ind 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/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 +qed. + -- 2.39.2