-(* The fact of being able to decide, via a computable boolean function, the
+(*
+\ 5h1 class="section"\ 6Effective searching\ 5/h1\ 6
+The fact of being able to decide, via a computable boolean function, the
equality between elements of a given set is an essential prerequisite for
effectively searching an element of that set inside a data structure. In this
section we shall define several boolean functions acting on lists of elements in
a DeqSet, and prove some of their properties.*)
-include "basics/list.ma".
+include "basics/list.ma".
include "tutorial/chapter4.ma".
(* 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:\ 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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="memb"\ 6let 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 ≝
match l with
[ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
- | cons a tl ⇒ (x \ 5a title="eqb" 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= a) \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 memb S x tl
- ].
+ | cons a tl ⇒ (x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 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
+ ]\ 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.
notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
interpretation "boolean membership" 'memb a l = (memb ? a l).
(op a b) is a member of (compose op l1 l2)
*)
-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.
+\ 5img class="anchor" src="icons/tick.png" id="memb_hd"\ 6lemma 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 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.
#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)) //
qed.
-lemma memb_cons: ∀S,a,b,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 → \ 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.
-#S #a #b #l normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize //
+\ 5img class="anchor" src="icons/tick.png" id="memb_cons"\ 6lemma memb_cons: ∀S,a,b,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 → \ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 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.
+#S #a #b #l normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b) normalize //
qed.
-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.
-#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
+\ 5img class="anchor" src="icons/tick.png" id="memb_single"\ 6lemma 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="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" 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.
+#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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) #H
[#_ >(\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/]
qed.
-lemma memb_append: ∀S,a,l1,l2.
+\ 5img class="anchor" src="icons/tick.png" id="memb_append"\ 6lemma memb_append: ∀S,a,l1,l2.
\ 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.
-#S #a #l1 elim l1 normalize [#l2 #H %2 //]
-#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/
+#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 //]
+#b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b) 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/
qed.
-lemma memb_append_l1: ∀S,a,l1,l2.
+\ 5img class="anchor" src="icons/tick.png" id="memb_append_l1"\ 6lemma memb_append_l1: ∀S,a,l1,l2.
\ 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.
#S #a #l1 elim l1 normalize
[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/
- |#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/
+ |#b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
]
qed.
-lemma memb_append_l2: ∀S,a,l1,l2.
+\ 5img class="anchor" src="icons/tick.png" id="memb_append_l2"\ 6lemma memb_append_l2: ∀S,a,l1,l2.
\ 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.
#S #a #l1 elim l1 normalize //
-#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/
+#b #tl #Hind #l2 cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
qed.
-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).
+\ 5img class="anchor" src="icons/tick.png" id="memb_exists"\ 6lemma 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\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6l\ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2).
#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/]
#b #tl #Hind #H cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H)
[#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) //
|#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
- @(\ 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 //
+ @(\ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)) @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … l2) >eqtl //
]
qed.
-lemma not_memb_to_not_eq: ∀S,a,b,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,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.
-#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)) //
+\ 5img class="anchor" src="icons/tick.png" id="not_memb_to_not_eq"\ 6lemma not_memb_to_not_eq: ∀S,a,b,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,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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b \ 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.
+#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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b)) //
#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/
qed.
-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 →
+\ 5img class="anchor" src="icons/tick.png" id="memb_map"\ 6lemma 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 →
\ 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.
#S1 #S2 #f #a #l elim l normalize [//]
-#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))
+#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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x))
[#eqx >eqx >(\P eqx) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … (f x))) normalize //
- |#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/
+ |#eqx >eqx cases (f a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6f x) normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
]
qed.
-lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
+\ 5img class="anchor" src="icons/tick.png" id="memb_compose"\ 6lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
\ 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 →
\ 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.
#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
]
qed.
-(* 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 *****************)
+(*
+\ 5h2 class="section"\ 6Unicity\ 5/h2\ 6
+If we are interested in representing finite sets as lists, is is convenient
+to avoid duplications of elements. The following uniqueb check this property.
+*)
-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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="uniqueb"\ 6let 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 ≝
match l with
[ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
| 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
(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
-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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="unique_append"\ 6let 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 ≝
match l1 with
[ nil ⇒ l2
| cons a tl ⇒
let r ≝ unique_append S tl l2 in
- 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
+ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6r
].
-axiom unique_append_elim: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀P: S → Prop.∀l1,l2.
-(∀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) →
-∀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.
+\ 5img class="anchor" src="icons/tick.png" id="memb_unique_append"\ 6lemma memb_unique_append: ∀S,a,l1,l2.
+ \ 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.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //]
+#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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b)) #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/
+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
+ [@Hind | >Hab normalize @Hind]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="unique_append_elim"\ 6lemma unique_append_elim: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀P: S → Prop.∀l1,l2.
+ (∀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) →
+ ∀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.
+#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/
+qed.
-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 →
+\ 5img class="anchor" src="icons/tick.png" id="unique_append_unique"\ 6lemma 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 →
\ 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.
#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
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)))
#H >H normalize [@Hind //] >H normalize @Hind //
qed.
-(******************* sublist *******************)
-definition sublist ≝
+(*
+\ 5h2 class="section"\ 6Sublists\ 5/h2\ 6
+*)
+\ 5img class="anchor" src="icons/tick.png" id="sublist"\ 6definition sublist ≝
λ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.
-lemma sublist_length: ∀S,l1,l2.
- \ 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|.
+\ 5img class="anchor" src="icons/tick.png" id="sublist_length"\ 6lemma sublist_length: ∀S,l1,l2.
+ \ 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="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 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\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
#S #l1 elim l1 //
#a #tl #Hind #l2 #unique #sub
-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 //]
+cut (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l3,l4\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6l2\ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l4)) [@\ 5a href="cic:/matita/tutorial/chapter5/memb_exists.def(5)"\ 6memb_exists\ 5/a\ 6 @sub //]
* #l3 * #l4 #eql2 >eql2 >\ 5a href="cic:/matita/basics/list/length_append.def(2)"\ 6length_append\ 5/a\ 6 normalize
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)]
>eql2 in sub; #sub #x #membx
]
qed.
-lemma sublist_unique_append_l1:
+\ 5img class="anchor" src="icons/tick.png" id="sublist_unique_append_l1"\ 6lemma sublist_unique_append_l1:
∀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).
#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/]
#x #tl #Hind #l2 #a
-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
+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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) #eqax >eqax
[<(\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)))
[#H >H normalize // | #H >H normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … 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
]
qed.
-lemma sublist_unique_append_l2:
+\ 5img class="anchor" src="icons/tick.png" id="sublist_unique_append_l2"\ 6lemma sublist_unique_append_l2:
∀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).
#S #l1 elim l1 [normalize //] #x #tl #Hind normalize
#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
-[@Hind | cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x) normalize // @Hind]
+[@Hind | cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x) normalize // @Hind]
qed.
-lemma decidable_sublist:∀S,l1,l2.
+\ 5img class="anchor" src="icons/tick.png" id="decidable_sublist"\ 6lemma decidable_sublist:∀S,l1,l2.
(\ 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).
#S #l1 #l2 elim l1
[%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/
]
qed.
-(********************* filtering *****************)
+(*\ 5h2 class="section"\ 6Filtering\ 5/h2\ 6*)
-lemma filter_true: ∀S,f,a,l.
+\ 5img class="anchor" src="icons/tick.png" id="memb_filter_true"\ 6lemma memb_filter_true: ∀S,f,a,l.
\ 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.
#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/]
#b #tl #Hind cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (f b)) #H
normalize >H normalize [2:@Hind]
-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
+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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b)) #eqab
[#_ >(\P eqab) // | >eqab normalize @Hind]
qed.
-lemma memb_filter_memb: ∀S,f,a,l.
+\ 5img class="anchor" src="icons/tick.png" id="memb_filter_memb"\ 6lemma memb_filter_memb: ∀S,f,a,l.
\ 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.
#S #f #a #l elim l [normalize //]
#b #tl #Hind normalize (cases (f b)) normalize
-cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b) normalize // @Hind
+cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b) normalize // @Hind
qed.
-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 →
+\ 5img class="anchor" src="icons/tick.png" id="memb_filter"\ 6lemma 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 →
\ 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).
-/\ 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/filter_true.def(5)"\ 6filter_true\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+/\ 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.
-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 →
+\ 5img class="anchor" src="icons/tick.png" id="memb_filter_l"\ 6lemma 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 →
\ 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.
#S #f #x #l #fx elim l normalize //
-#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
+#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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b)) #eqxb
[<(\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 //
|>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
]
qed.
-(********************* exists *****************)
+(*
+\ 5h2 class="section"\ 6Exists\ 5/h2\ 6
+*)
-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 ≝
+\ 5img class="anchor" src="icons/tick.png" id="exists"\ 6let 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 ≝
match l with
[ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
| cons h t ⇒ \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 (p h) (exists A p t)