From 0163748c68bda563aa92d244b917b394b2446c7d Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 19 Oct 2011 08:07:45 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 62 +++++++++++++++++++++++-------------- 1 file changed, 39 insertions(+), 23 deletions(-) diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index a75b4ce1e..9d1e81de0 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -176,15 +176,26 @@ f:A → B, a list l = [a1; a2; ... ; an] and returning the list 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)]. -(* 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. *) +(* Another major example is the fold function, that taken a list +l = [a1; a2; ... ;an], a base value b: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)]. + +(* As an example of application of foldr, let us use it to define a filter function +that given a list l: list A and a boolean test p:A → bool returns the sublist of elements +satisfying the test. In this case, the result type B of foldr should be (list A), the base +value is [], and f: A → list A →list A is the function that taken x and l returns x::l, if +x satisfies the test, and l otherwise. We use an if_then_else function included from +bbol.ma to this purpose. *) 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 +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. *) @@ -196,14 +207,32 @@ 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)...)). *) +(* As another example, let us redefine the map function using foldr. The +result type B is (list B), the base value b is [], and the fold function +of type A → list B → list B is the function mapping a and l to (f a)::l. +*) -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)]. +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. -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. +(* 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 +intentional point of view, map and map_again are not functions, but programs, +and they are clearly different. What we would like to say is that the two +programs behave in the same way: this is a different, extensional equality +that can be defined in the following way. *) + +definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g a. + +(* Proving that map and map_again are extentionally equal in the +previous sense can be proved by a trivial structural induction on the list *) + +lemma eq_map: ∀A,B,f. a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a ?? (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B f) (a href="cic:/matita/tutorial/chapter3/map_again.def(2)"map_again/a A B f). +#A #B #f #n (elim n) normalize // qed. + + + 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. (* @@ -253,17 +282,4 @@ theorem fold_filter: | >a href="cic:/matita/tutorial/chapter3/filter_false.def(3)"filter_false/a // >a href="cic:/matita/tutorial/chapter3/fold_false.def(3)"fold_false/a // ] qed. -record Aop (A:Type[0]) (nil:A) : Type[0] ≝ - {op :2> A → A → A; - nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; - nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; - assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c - }. - -theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"Aop/a B nil.∀f. - op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a - 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. - +record Aop (A:Type[0]) (ni \ No newline at end of file -- 2.39.2