From 5e6f74d92ae5d2618a239565ef8ebfbb22d67923 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 29 Feb 2012 12:26:57 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter5.ma | 34 ++++++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma index d0bf2c5d6..f9a0b30be 100644 --- a/weblib/tutorial/chapter5.ma +++ b/weblib/tutorial/chapter5.ma @@ -7,7 +7,9 @@ a DeqSet, and prove some of their properties.*) include "basics/list.ma". include "tutorial/chapter4.ma". -(********* search *********) +(* The first function we define is an effective version of the membership relation, +between an element x and a list l. Its definition is a straightforward recursion on +l.*) let rec memb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l ≝ match l with @@ -18,6 +20,21 @@ let rec memb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}. interpretation "boolean membership" 'memb a l = (memb ? a l). +(* We can now prove several interesing properties for memb: +- memb_hd: x is a member of x::l +- memb_cons: if x is a member of l than x is a member of a::l +- memb_single: if x is a member of [a] then x=a +- memb_append: if x is a member of l1@l2 then either x is a member of l1 + or x is a member of l2 +- memb_append_l1: if x is a member of l1 then x is a member of l1@l2 +- memb_append_l2: if x is a member of l2 then x is a member of l1@l2 +- memb_exists: if x is a member of l, than l can decomposed as l1@(x::l2) +- not_memb_to_not_eq: if x is not a member of l and y is, then x≠y +- memb_map: if a is a member of l, then (f a) is a member of (map f l) +- memb_compose: if a is a member of l1 and b is a meber of l2 than + (op a b) is a member of (compose op l1 l2) +*) + lemma memb_hd: ∀S,a,l. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (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/basics/bool/bool.con(0,1,0)"true/a. #S #a #l normalize >(a href="cic:/matita/basics/logic/proj2.def(2)"proj2/a … (a href="cic:/matita/tutorial/chapter4/eqb_true.fix(0,0,4)"eqb_true/a S …) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a S a)) // qed. @@ -27,14 +44,13 @@ lemma memb_cons: ∀S,a,b,l. #S #a #b #l normalize cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize // qed. -lemma memb_single: ∀S,a,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a a title="cons" href="cic:/fakeuri.def(1)"[/ax] 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 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. +lemma memb_single: ∀S,a,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (xa title="cons" 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 a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x. #S #a #x normalize cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=x)) #H [#_ >(\P H) // |>H normalize #abs @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. lemma memb_append: ∀S,a,l1,l2. -a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S 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/basics/bool/bool.con(0,1,0)"true/a → - a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 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/chapter5/memb.fix(0,2,4)"memb/a S 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/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #a #l1 elim l1 normalize [#l2 #H %2 //] #b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a/span/span/ qed. @@ -53,8 +69,7 @@ lemma memb_append_l2: ∀S,a,l1,l2. #b #tl #Hind #l2 cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b) normalize /span class="autotactic"2span class="autotrace" trace /span/span/ qed. -lemma memb_exists: ∀S,a,l.a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l 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 title="exists" href="cic:/fakeuri.def(1)"∃/al1,l2.la title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/al1a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l2). +lemma memb_exists: ∀S,a,l.a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l 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 title="exists" href="cic:/fakeuri.def(1)"∃/al1,l2.la title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/al1a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l2). #S #a #l elim l [normalize #abs @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/] #b #tl #Hind #H cases (a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a … H) [#eqba @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S)) @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … tl) >(\P eqba) // @@ -88,7 +103,10 @@ lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2. ] qed. -(**************** unicity test *****************) +(* If we are interested in representing finite sets as lists, is is convenient +to avoid duplications of elements. The following uniqueb check this property. *) + +(*************** unicity test *****************) let rec uniqueb (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) l on l : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝ match l with @@ -209,4 +227,4 @@ let rec exists (A:Type[0]) (p:A → a href="cic:/matita/basics/bool/bool.ind(1, match l with [ nil ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a | cons h t ⇒ a href="cic:/matita/basics/bool/orb.def(1)"orb/a (p h) (exists A p t) -]. +]. \ No newline at end of file -- 2.39.2