From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Feb 2012 12:26:57 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1925
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5e6f74d92ae5d2618a239565ef8ebfbb22d67923

commit by user andrea
---

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