From 83aea9a1662de32505512d6296921ebfffcfc53d Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 19 Oct 2011 10:34:46 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter3.ma | 65 +++++++++++++++++++++++++++---------- 1 file changed, 47 insertions(+), 18 deletions(-) diff --git a/weblib/tutorial/chapter3.ma b/weblib/tutorial/chapter3.ma index 9d1e81de0..ca7e89355 100644 --- a/weblib/tutorial/chapter3.ma +++ b/weblib/tutorial/chapter3.ma @@ -228,29 +228,46 @@ definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a a title="leibnitz's e (* 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). +lemma eq_maps: ∀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. - -(* -let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝ -match l1 with - [ nil ⇒ nil ? - | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g - ]. *) - -(**************************** fold *******************************) - -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 us make another remark about extensional equality. It is clear that, +if f is extensionally equal to g, then (map A B f) is extensionally equal to +(map A B g). Let us prove it. *) + +theorem eq_map : ∀A,B,f,g. a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a A B f g → a href="cic:/matita/tutorial/chapter3/ExtEq.def(1)"ExtEq/a ?? (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a span style="text-decoration: underline;"/spanA B f) (a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"map/a A B g). +#A #B #f #g #eqfg + +(* the relevant point is that we cannot proceed by rewriting f with g via +eqfg, here. Rewriting only works with Matita intensional equality, while here +we are dealing with a different predicate, defined by the user. The right way +to proceed is to unfold the definition of ExtEq, and work by induction on l, +as usual when we want to prove extensional equality between functions over +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 +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 +repeating proofs of generic properties over and over again. +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 ≝ 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)) (fold A B op b p f l)]. - -notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" + +(* It is also important to spend a few time to introduce some fancy notation +for these iterators. *) + + notation "\fold [ op , nil ]_{ ident i ∈ l | p} f" with precedence 80 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}. @@ -282,4 +299,16 @@ 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]) (ni \ No newline at end of file +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:A → B. + 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. \ No newline at end of file -- 2.39.2