]> matita.cs.unibo.it Git - helm.git/blob - weblib/tutorial/chapter5.ma
Sys.Break no longer caught during indexing
[helm.git] / weblib / tutorial / chapter5.ma
1 (* 
2 \ 5h1 class="section"\ 6Effective searching\ 5/h1\ 6
3 The fact of being able to decide, via a computable boolean function, the 
4 equality between elements of a given set is an essential prerequisite for 
5 effectively searching an element of that set inside a data structure. In this 
6 section we shall define several boolean functions acting on lists of elements in 
7 a DeqSet, and prove some of their properties.*)
8
9 include "basics/list.ma". 
10 include "tutorial/chapter4.ma".
11
12 (* The first function we define is an effective version of the membership relation,
13 between an element x and a list l. Its definition is a straightforward recursion on
14 l.*)
15
16 let rec memb (S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (x:S) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6 S) on l  ≝
17   match l with
18   [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
19   | cons a tl ⇒ (x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= a) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 memb S x tl
20   ]\ 5span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"\ 6\ 5/span\ 6\ 5span class="error" title="No choices for ID nil"\ 6\ 5/span\ 6.
21
22 notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
23 interpretation "boolean membership" 'memb a l = (memb ? a l).
24
25 (* We can now prove several interesing properties for memb:
26 - memb_hd: x is a member of x::l
27 - memb_cons: if x is a member of l than x is a member of a::l
28 - memb_single: if x is a member of [a] then x=a
29 - memb_append: if x is a member of l1@l2 then either x is a member of l1
30   or x is a member of l2
31 - memb_append_l1: if x is a member of l1 then x is a member of l1@l2
32 - memb_append_l2: if x is a member of l2 then x is a member of l1@l2
33 - memb_exists: if x is a member of l, than l can decomposed as l1@(x::l2)
34 - not_memb_to_not_eq: if x is not a member of l and y is, then x≠y
35 - memb_map: if a is a member of l, then (f a) is a member of (map f l)
36 - memb_compose: if a is a member of l1 and b is a meber of l2 than
37   (op a b) is a member of (compose op l1 l2)
38 *)
39
40 lemma memb_hd: ∀S,a,l. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
41 #S #a #l normalize >(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter4/eqb_true.fix(0,0,4)"\ 6eqb_true\ 5/a\ 6 S …) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 S a)) //
42 qed.
43
44 lemma memb_cons: ∀S,a,b,l. 
45   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5/span\ 6 S a (b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
46 #S #a #b #l normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize // 
47 qed.
48
49 lemma memb_single: ∀S,a,x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
50 #S #a #x normalize cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x)) #H
51   [#_ >(\P H) // |>H normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
52 qed.
53
54 lemma memb_append: ∀S,a,l1,l2. 
55 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5span class="error" title="Parse error: [term level 46] expected after [sym@] (in [term])"\ 6\ 5/span\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
56 #S #a #l1\ 5span class="error" title="Parse error: illegal begin of statement"\ 6\ 5/span\ 6\ 5span class="error" title="Parse error: illegal begin of statement"\ 6\ 5/span\ 6 elim l1 normalize [#l2 #H %2 //] 
57 #b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6
58 qed. 
59
60 lemma memb_append_l1: ∀S,a,l1,l2. 
61  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
62 #S #a #l1 elim l1 normalize
63   [normalize #le #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
64   |#b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6
65   ]
66 qed. 
67
68 lemma memb_append_l2: ∀S,a,l1,l2. 
69  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
70 #S #a #l1 elim l1 normalize //
71 #b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6
72 qed. 
73
74 lemma memb_exists: ∀S,a,l.\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5/span\ 6 → \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6l1,l2.l\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l2).
75 #S #a #l elim l [normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
76 #b #tl #Hind #H cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H)
77   [#eqba @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … tl) >(\P eqba) //
78   |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
79    @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … l2) >eqtl //
80   ]
81 qed.
82
83 lemma not_memb_to_not_eq: ∀S,a,b,l. 
84  \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S b l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
85 #S #a #b #l cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) // 
86 #eqab >(\P eqab) #H >H #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
87 qed. 
88  
89 lemma memb_map: ∀S1,S2,f,a,l. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S1 a l\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
90   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S2 (f a) (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 … f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
91 #S1 #S2 #f #a #l elim l normalize [//]
92 #x #tl #memba cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x))
93   [#eqx >eqx >(\P eqx) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … (f x))) normalize //
94   |#eqx >eqx cases (f a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=f x) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
95   ]
96 qed.
97
98 lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.   
99   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S1 a1 l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S2 a2 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
100   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S3 (op a1 a2) (\ 5a href="cic:/matita/basics/list/compose.def(2)"\ 6compose\ 5/a\ 6 S1 S2 S3 op l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
101 #S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
102 #x #tl #Hind #l2 #memba1 #memba2 cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … memba1)
103   [#eqa1 >(\P eqa1) @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter5/memb_map.def(5)"\ 6memb_map\ 5/a\ 6 // 
104   |#membtl @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 @Hind //
105   ]
106 qed.
107
108 (* 
109 \ 5h2 class="section"\ 6Unicity\ 5/h2\ 6
110 If we are interested in representing finite sets as lists, is is convenient
111 to avoid duplications of elements. The following uniqueb check this property. 
112 *)
113
114 let rec uniqueb (S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) l on l : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
115   match l with 
116   [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
117   | cons a tl ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a tl) \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 uniqueb S tl
118   ].
119
120 (* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
121
122 let rec unique_append (S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
123   match l1 with
124   [ nil ⇒ l2
125   | cons a tl ⇒ 
126      let r ≝ unique_append S tl l2 in
127      if \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a r then r else a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:r
128   ].
129
130 lemma memb_unique_append: ∀S,a,l1,l2. 
131   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
132 #S #a #l1 elim l1 normalize [#l2 #H %2 //] 
133 #b #tl #Hind #l2 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) #Hab >Hab normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
134 cases (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S b (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)) normalize 
135   [@Hind | >Hab normalize @Hind]   
136 qed. 
137
138 lemma unique_append_elim: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀P: S → Prop.∀l1,l2. 
139   (∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"\ 6\ 5/span\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x) → (∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x) →
140     ∀x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P x. 
141 #S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (\ 5a href="cic:/matita/tutorial/chapter5/memb_unique_append.def(6)"\ 6memb_unique_append\ 5/a\ 6\ 5span class="error" title="No choices for ID memb_unique_append"\ 6\ 5/span\ 6 … membx) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6
142 qed.
143
144 lemma unique_append_unique: ∀S,l1,l2. \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
145   \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
146 #S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
147 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2))) 
148 #H >H normalize [@Hind //] >H normalize @Hind //
149 qed.
150
151 (*
152 \ 5h2 class="section"\ 6Sublists\ 5/h2\ 6
153 *)
154 definition sublist ≝ 
155   λS,l1,l2.∀a. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
156
157 lemma sublist_length: ∀S,l1,l2. 
158  \ 5a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"\ 6uniqueb\ 5/a\ 6 S l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 l2 → \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1| \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l2|.
159 #S #l1 elim l1 // 
160 #a #tl #Hind #l2 #unique #sub
161 cut (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6l3,l4.l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l4)) [@\ 5a href="cic:/matita/tutorial/chapter5/memb_exists.def(5)"\ 6memb_exists\ 5/a\ 6 @sub //]
162 * #l3 * #l4 #eql2 >eql2 >\ 5a href="cic:/matita/basics/list/length_append.def(2)"\ 6length_append\ 5/a\ 6 normalize 
163 applyS \ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 <\ 5a href="cic:/matita/basics/list/length_append.def(2)"\ 6length_append\ 5/a\ 6 @Hind [@(\ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6 … unique)]
164 >eql2 in sub; #sub #x #membx 
165 cases (\ 5a href="cic:/matita/tutorial/chapter5/memb_append.def(5)"\ 6memb_append\ 5/a\ 6 … (sub x (\ 5a href="cic:/matita/basics/bool/orb_true_r2.def(3)"\ 6orb_true_r2\ 5/a\ 6 … membx)))
166   [#membxl3 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l1.def(5)"\ 6memb_append_l1\ 5/a\ 6 //
167   |#membxal4 cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … membxal4)
168     [#eqxa @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 lapply (\ 5a href="cic:/matita/basics/bool/andb_true_l.def(4)"\ 6andb_true_l\ 5/a\ 6 … unique)
169      <(\P eqxa) >membx normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ |#membxl4 @\ 5a href="cic:/matita/tutorial/chapter5/memb_append_l2.def(5)"\ 6memb_append_l2\ 5/a\ 6 //
170     ]
171   ]
172 qed.
173
174 lemma sublist_unique_append_l1: 
175   ∀S,l1,l2. \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2).
176 #S #l1 elim l1 normalize [#l2 #S #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
177 #x #tl #Hind #l2 #a 
178 normalize cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x)) #eqax >eqax 
179 [<(\P eqax) cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)))
180   [#H >H normalize // | #H >H normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … a)) //]
181 |cases (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)) normalize 
182   [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ |>eqax normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
183 ]
184 qed.
185
186 lemma sublist_unique_append_l2: 
187   ∀S,l1,l2. \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l2 (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2).
188 #S #l1 elim l1 [normalize //] #x #tl #Hind normalize 
189 #l2 #a cases (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)) normalize
190 [@Hind | cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x) normalize // @Hind]
191 qed.
192
193 lemma decidable_sublist:∀S,l1,l2. 
194   (\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 l2) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S l1 l2).
195 #S #l1 #l2 elim l1 
196   [%1 #a normalize in ⊢ (%→?); #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
197   |#a #tl * #subtl 
198     [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2)) #memba
199       [%1 whd #x #membx cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … membx)
200         [#eqax >(\P eqax) // |@subtl]
201       |%2 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6 … \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 memba)) #H1 @H1 @\ 5a href="cic:/matita/tutorial/chapter5/memb_hd.def(5)"\ 6memb_hd\ 5/a\ 6
202       ]
203     |%2 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … subtl) #H1 #x #H2 @H1 @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
204     ] 
205   ]
206 qed.
207
208 (*\ 5h2 class="section"\ 6Filtering\ 5/h2\ 6*)
209
210 lemma memb_filter_true: ∀S,f,a,l. 
211   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 S f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
212 #S #f #a #l elim l [normalize #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
213 #b #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #H
214 normalize >H normalize [2:@Hind]
215 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) #eqab
216   [#_ >(\P eqab) // | >eqab normalize @Hind]
217 qed. 
218   
219 lemma memb_filter_memb: ∀S,f,a,l. 
220   \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 S f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
221 #S #f #a #l elim l [normalize //]
222 #b #tl #Hind normalize (cases (f b)) normalize 
223 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize // @Hind
224 qed.
225   
226 lemma memb_filter: ∀S,f,l,x. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
227 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6).
228 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6memb_filter_memb\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_true.def(5)"\ 6memb_filter_true\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
229
230 lemma memb_filter_l: ∀S,f,x,l. (f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
231 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S x (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? f l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
232 #S #f #x #l #fx elim l normalize //
233 #b #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (x\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) #eqxb
234   [<(\P eqxb) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … x)) >fx normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … x)) normalize //
235   |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
236   ]
237 qed. 
238
239 (*
240 \ 5h2 class="section"\ 6Exists\ 5/h2\ 6
241 *)
242
243 let rec exists (A:Type[0]) (p:A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
244 match l with
245 [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
246 | cons h t ⇒ \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 (p h) (exists A p t)
247 ].