]> matita.cs.unibo.it Git - helm.git/blob - weblib/tutorial/chapter4.ma
update in basic_2 and ground_2
[helm.git] / weblib / tutorial / chapter4.ma
1 (* 
2 \ 5h1 class="section"\ 6Naif Set Theory\ 5/h1\ 6
3 *)
4 include "basics/types.ma".
5 include "basics/bool.ma".
6 (* 
7 In this Chapter we shall develop a naif theory of sets represented as 
8 characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type 
9 A→Prop. 
10 For instance the empty set is defined by the always false function: *)
11
12 \ 5img class="anchor" src="icons/tick.png" id="empty_set"\ 6definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
13 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
14 interpretation "empty set" 'empty_set = (empty_set ?).
15
16 (* Similarly, a singleton set contaning containing an element a, is defined
17 by by the characteristic function asserting equality with a *)
18
19 \ 5img class="anchor" src="icons/tick.png" id="singleton"\ 6definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6a.
20 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
21 interpretation "singleton" 'singl x = (singleton ? x).
22
23 (* The membership relation between an element of type A and a set S:A →Prop is
24 simply the predicate resulting from the application of S to a.
25 The operations of union, intersection, complement and substraction 
26 are easily defined in terms of the propositional connectives of dijunction,
27 conjunction and negation *)
28
29 \ 5img class="anchor" src="icons/tick.png" id="union"\ 6definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 Q a.
30 interpretation "union" 'union a b = (union ? a b).
31
32 \ 5img class="anchor" src="icons/tick.png" id="intersection"\ 6definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∧] (in [term])"\ 6\ 5/span\ 6 Q a.
33 interpretation "intersection" 'intersects a b = (intersection ? a b).
34
35 \ 5img class="anchor" src="icons/tick.png" id="complement"\ 6definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
36 interpretation "complement" 'not a = (complement ? a).
37
38 \ 5img class="anchor" src="icons/tick.png" id="substraction"\ 6definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 B w.
39 interpretation "substraction" 'minus a b = (substraction ? a b).
40
41 (* Finally, we use implication to define the inclusion relation between
42 sets *)
43
44 \ 5img class="anchor" src="icons/tick.png" id="subset"\ 6definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
45 interpretation "subset" 'subseteq a b = (subset ? a b).
46
47 (* 
48 \ 5h2 class="section"\ 6Set Equality\ 5/h2\ 6
49 Two sets are equals if and only if they have the same elements, that is,
50 if the two characteristic functions are extensionally equivalent: *) 
51
52 \ 5img class="anchor" src="icons/tick.png" id="eqP"\ 6definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym↔] (in [term])"\ 6\ 5/span\ 6 Q a.
53 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
54 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
55
56 (*
57 This notion of equality is different from the intensional equality of
58 functions; the fact it defines an equivalence relation must be explicitly 
59 proved: *)
60
61 \ 5img class="anchor" src="icons/tick.png" id="eqP_sym"\ 6lemma eqP_sym: ∀U.∀A,B:U →Prop. 
62   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
63 #U #A #B #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @eqAB qed.
64  
65 \ 5img class="anchor" src="icons/tick.png" id="eqP_trans"\ 6lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
66   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C.
67 #U #A #B #C #eqAB #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 // qed.
68
69 (* For the same reason, we must also prove that all the operations behave well
70 with respect to eqP: *)
71
72 \ 5img class="anchor" src="icons/tick.png" id="eqP_union_r"\ 6lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
73   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: NUMBER '1' or [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 61 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B.
74 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6 @eqAB qed.
75   
76 \ 5img class="anchor" src="icons/tick.png" id="eqP_union_l"\ 6lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
77   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C.
78 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"\ 6iff_or_l\ 5/a\ 6 @eqBC qed.
79   
80 \ 5img class="anchor" src="icons/tick.png" id="eqP_intersect_r"\ 6lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
81   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B.
82 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
83   
84 \ 5img class="anchor" src="icons/tick.png" id="eqP_intersect_l"\ 6lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
85   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∩] (in [term])"\ 6\ 5/span\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C.
86 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 @eqBC qed.
87
88 \ 5img class="anchor" src="icons/tick.png" id="eqP_substract_r"\ 6lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
89   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B.
90 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
91   
92 \ 5img class="anchor" src="icons/tick.png" id="eqP_substract_l"\ 6lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
93   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C  → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C.
94 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/iff_not.def(4)"\ 6iff_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
95
96 (* 
97 \ 5h2 class="section"\ 6Simple properties of sets\ 5/h2\ 6
98 We can now prove several properties of the previous set-theoretic operations. 
99 In particular, union is commutative and associative, and the empty set is an 
100 identity element: *)
101
102 \ 5img class="anchor" src="icons/tick.png" id="union_empty_r"\ 6lemma union_empty_r: ∀U.∀A:U→Prop. 
103   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
104 #U #A #w % [* // 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 \ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
105 qed.
106
107 \ 5img class="anchor" src="icons/tick.png" id="union_comm"\ 6lemma union_comm : ∀U.∀A,B:U →Prop. 
108   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
109 #U #A #B #a % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
110
111 \ 5img class="anchor" src="icons/tick.png" id="union_assoc"\ 6lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
112   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C).
113 #S #A #B #C #w % [* [* /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ] | * [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
114 qed.   
115
116 (* In the same way we prove commutativity and associativity for set 
117 interesection *)
118
119 \ 5img class="anchor" src="icons/tick.png" id="cap_comm"\ 6lemma cap_comm : ∀U.∀A,B:U →Prop. 
120   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
121 #U #A #B #a % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
122
123 \ 5img class="anchor" src="icons/tick.png" id="cap_assoc"\ 6lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
124   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C) \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C.
125 #U #A #B #C #w % [ * #Aw * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5span class="autotrace"\ 6\ 5/span\ 6\ 5/span\ 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\ 5/span\ 6\ 5/span\ 6/ ]
126 qed.
127
128 (* We can also easily prove idempotency for union and intersection *)
129
130 \ 5img class="anchor" src="icons/tick.png" id="union_idemp"\ 6lemma union_idemp: ∀U.∀A:U →Prop. 
131   A  \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
132 #U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] qed. 
133
134 \ 5img class="anchor" src="icons/tick.png" id="cap_idemp"\ 6lemma cap_idemp: ∀U.∀A:U →Prop. 
135   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
136 #U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] qed. 
137
138 (* We conclude our examples with a couple of distributivity theorems, and a 
139 characterization of substraction in terms of interesection and complementation. *)
140
141 \ 5img class="anchor" src="icons/tick.png" id="distribute_intersect"\ 6lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
142   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C).
143 #U #A #B #C #w % [* * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
144 qed.
145   
146 \ 5img class="anchor" src="icons/tick.png" id="distribute_substract"\ 6lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
147   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B) \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C).
148 #U #A #B #C #w % [* * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
149 qed.
150
151 \ 5img class="anchor" src="icons/tick.png" id="substract_def"\ 6lemma substract_def:∀U.∀A,B:U→Prop. A\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6\ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="complement" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
152 #U #A #B #w normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
153 qed.
154
155 (* 
156 \ 5h2 class="section"\ 6Bool vs. Prop\ 5/h2\ 6
157 In several situation it is important to assume to have a decidable equality 
158 between elements of a set U, namely a boolean function eqb: U→U→bool such that
159 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y. 
160 A set equipped with such an equality is called a DeqSet: *)
161
162 \ 5img class="anchor" src="icons/tick.png" id="DeqSet"\ 6record DeqSet : Type[1] ≝ { carr :> Type[0];
163    eqb: carr → carr → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
164    eqb_true: ∀x,y. (eqb x y \ 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="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y)
165 }.
166
167 (* We use the notation == to denote the decidable equality, to distinguish it
168 from the propositional equality. In particular, a term of the form a==b is a 
169 boolean, while a=b is a proposition. *)
170
171 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
172 interpretation "eqb" 'eqb a b = (eqb ? a b).
173
174 (* 
175 \ 5h2 class="section"\ 6Small Scale Reflection\ 5/h2\ 6
176 It is convenient to have a simple way to reflect a proof of the fact 
177 that (eqb a b) is true into a proof of the proposition (a = b); to this aim, 
178 we introduce two operators "\P" and "\b". *)
179
180 notation "\P H" non associative with precedence 90 
181   for @{(proj1 … (eqb_true ???) $H)}. 
182
183 notation "\b H" non associative with precedence 90 
184   for @{(proj2 … (eqb_true ???) $H)}. 
185   
186 (* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
187 \b h: eqb a b = true. Let us see an example of their use: the following 
188 statement asserts that we can reflect a proof that eqb a b is false into
189 a proof of the proposition a ≠ b. *)
190
191 \ 5img class="anchor" src="icons/tick.png" id="eqb_false"\ 6lemma eqb_false: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S. 
192   (\ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 ? a 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 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 b.
193
194 (* We start the proof introducing the hypothesis, and then split the "if" and
195 "only if" cases *)
196  
197 #S #a #b % #H 
198
199 (* The latter is easily reduced to prove the goal true=false under the assumption
200 H1: a = b *)
201   [@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … \ 5a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"\ 6not_eq_true_false\ 5/a\ 6) #H1 
202   
203 (* since by assumption H false is equal to (a==b), by rewriting we obtain the goal 
204 true=(a==b) that is just the boolean version of H1 *) 
205
206   <H @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @(\b H1)
207
208 (* In the "if" case, we proceed by cases over the boolean equality (a==b); if 
209 (a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
210 true, then by reflection a=b, while by hypothesis a≠b *)
211   
212  |cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 ? a b)) // #H1 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … (\P H1) H)
213   ]
214 qed.
215  
216 (* We also introduce two operators "\Pf" and "\bf" to reflect a proof
217 of (a==b)=false into a proof of a≠b, and vice-versa *) 
218
219 notation "\Pf H" non associative with precedence 90 
220   for @{(proj1 … (eqb_false ???) $H)}. 
221
222 notation "\bf H" non associative with precedence 90 
223   for @{(proj2 … (eqb_false ???) $H)}. 
224
225 (* The following statement proves that propositional equality in a 
226 DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
227
228  \ 5img class="anchor" src="icons/tick.png" id="dec_eq"\ 6lemma dec_eq: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S. a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 a \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 b.
229 #S #a #b cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 ? a b)) #H
230   [%1 @(\P H) | %2 @(\Pf H)]
231 qed.
232
233 (* 
234 \ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
235 A simple example of a set with a decidable equality is bool. We first define 
236 the boolean equality beqb, that is just the xand function, then prove that 
237 beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by 
238 instantiating the DeqSet record with the previous information *)
239
240 \ 5img class="anchor" src="icons/tick.png" id="beqb"\ 6definition beqb ≝ λb1,b2.
241   match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2].
242
243 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
244
245 \ 5img class="anchor" src="icons/tick.png" id="beqb_true"\ 6lemma beqb_true: ∀b1,b2. \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 \ 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) (b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2).
246 #b1 #b2 cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
247 qed. 
248
249 \ 5img class="anchor" src="icons/tick.png" id="DeqBool"\ 6definition DeqBool ≝ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
250
251 (* At this point, we would expect to be able to prove things like the
252 following: for any boolean b, if b==false is true then b=false. 
253 Unfortunately, this would not work, unless we declare b of type 
254 DeqBool (change the type in the following statement and see what 
255 happens). *)
256
257 \ 5img class="anchor" src="icons/tick.png" id="exhint"\ 6example exhint: ∀b:\ 5a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"\ 6DeqBool\ 5/a\ 6. (b\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" 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 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 → 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.
258 #b #H @(\P H) 
259 qed.
260
261 (* The point is that == expects in input a pair of objects whose type must be the 
262 carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference 
263 system has no knowledge of it (it is an information that has been supplied by the 
264 user, and stored somewhere in the library). More explicitly, the type inference 
265 inference system, would face an unification problem consisting to unify bool 
266 against the carrier of something (a metavaribale) and it has no way to synthetize 
267 the answer. To solve this kind of situations, matita provides a mechanism to hint 
268 the system the expected solution. A unification hint is a kind of rule, whose rhd 
269 is the unification problem, containing some metavariables X1, ..., Xn, and whose 
270 left hand side is the solution suggested to the system, in the form of equations 
271 Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
272 is, if it is a unifier for the given problem.
273 To make an example, in the previous case, the unification problem is bool = carr X,
274 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since 
275 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
276
277 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6\ 5/a\ 6 ; 
278     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6
279 (* ---------------------------------------- *) ⊢ 
280     \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
281     
282 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6\ 5/a\ 6 b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6
283     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6
284 (* ---------------------------------------- *) ⊢ 
285     \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X b1 b2.
286     
287 (* After having provided the previous hints, we may rewrite example exhint 
288 declaring b of type bool. *)
289  
290 \ 5img class="anchor" src="icons/tick.png" id="exhint1"\ 6example exhint1: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. (b \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" 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 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 → 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
291 #b #H @(\P H)
292 qed.
293
294 (* The cartesian product of two DeqSets is still a DeqSet. To prove
295 this, we must as usual define the boolen equality function, and prove
296 it correctly reflects propositional equality. *)
297
298 \ 5img class="anchor" src="icons/tick.png" id="eq_pairs"\ 6definition eq_pairs ≝
299   λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λp1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p1 \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p2) \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p1 \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p2).
300
301 \ 5img class="anchor" src="icons/tick.png" id="eq_pairs_true"\ 6lemma eq_pairs_true: ∀A,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀p1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.
302   \ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B p1 p2 \ 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="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 p1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p2.
303 #A #B * #a1 #b1 * #a2 #b2 %
304   [#H cases (\ 5a href="cic:/matita/basics/bool/andb_true.def(5)"\ 6andb_true\ 5/a\ 6 …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
305   |#H destruct normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … a2)) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … b2)) //
306   ]
307 qed.
308
309 \ 5img class="anchor" src="icons/tick.png" id="DeqProd"\ 6definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
310   \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs_true.def(6)"\ 6eq_pairs_true\ 5/a\ 6 A B).
311
312 (* Having an unification problem of the kind T1×T2 = carr X, what kind 
313 of hint can we give to the system? We expect T1 to be the carrier of a
314 DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
315 This is expressed by the following hint: *)
316
317 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6\ 5/a\ 6 C1,C2; 
318     T1 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C1,
319     T2 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C2,
320     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 C1 C2
321 (* ---------------------------------------- *) ⊢ 
322     T1\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6T2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
323
324 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6\ 5/a\ 6 T1,T2,p1,p2; 
325     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 T1 T2
326 (* ---------------------------------------- *) ⊢ 
327     \ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 T1 T2 p1 p2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X p1 p2.
328
329 \ 5img class="anchor" src="icons/tick.png" id="hint2"\ 6example hint2: ∀b1,b2. 
330   \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2\ 5a title="Pair construction" 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 → \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6.
331 #b1 #b2 #H @(\P H).