2 \ 5h1 class="section"
\ 6Naif Set Theory
\ 5/h1
\ 6
4 In this Chapter we shall develop a naif theory of sets represented as
5 characteristic predicates over some universe
\ 5code
\ 6A
\ 5/code
\ 6, that is as objects of type
8 include "basics/types.ma".
9 include "basics/bool.ma".
11 (* For instance the empty set is defined by the always false function: *)
13 definition empty_set ≝ λA:Type[0].λa:A.
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
14 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
15 interpretation "empty set" 'empty_set = (empty_set ?).
17 (* Similarly, a singleton set contaning containing an element a, is defined
18 by by the characteristic function asserting equality with a *)
20 definition 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.
21 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
22 interpretation "singleton" 'singl x = (singleton ? x).
24 (* The membership relation between an element of type A and a set S:A →Prop is
25 simply the predicate resulting from the application of S to a.
26 The operations of union, intersection, complement and substraction
27 are easily defined in terms of the propositional connectives of dijunction,
28 conjunction and negation *)
30 definition 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.
31 interpretation "union" 'union a b = (union ? a b).
33 definition 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.
34 interpretation "intersection" 'intersects a b = (intersection ? a b).
36 definition complement ≝ λU:Type[0].λA:U → Prop.λw.
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 A w.
37 interpretation "complement" 'not a = (complement ? a).
39 definition 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.
40 interpretation "substraction" 'minus a b = (substraction ? a b).
42 (* Finally, we use implication to define the inclusion relation between
45 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
46 interpretation "subset" 'subseteq a b = (subset ? a b).
48 (* Two sets are equals if and only if they have the same elements, that is,
49 if the two characteristic functions are extensionally equivalent: *)
51 definition 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.
52 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
53 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
55 (* This notion of equality is different from the intensional equality of
56 functions; the fact it defines an equivalence relation must be explicitly
59 lemma eqP_sym: ∀U.∀A,B:U →Prop.
60 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.
61 #U #A #B #eqAB #a @
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @eqAB qed.
63 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
64 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.
65 #U #A #B #C #eqAB #eqBC #a @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 // qed.
67 (* For the same reason, we must also prove that all the operations behave well
68 with respect to eqP: *)
70 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
71 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.
72 #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.
74 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
75 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.
76 #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.
78 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
79 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.
80 #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.
82 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
83 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.
84 #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.
86 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
87 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.
88 #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.
90 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
91 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.
92 #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.
94 (* We can now prove several properties of the previous set-theoretic operations.
95 In particular, union is commutative and associative, and the empty set is an
98 lemma union_empty_r: ∀U.∀A:U→Prop.
99 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.
100 #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/]
103 lemma union_comm : ∀U.∀A,B:U →Prop.
104 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.
105 #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.
107 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
108 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).
109 #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/]
112 (* In the same way we prove commutativity and associativity for set
115 lemma cap_comm : ∀U.∀A,B:U →Prop.
116 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.
117 #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.
119 lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
120 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.
121 #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/ ]
124 (* We can also easily prove idempotency for union and intersection *)
126 lemma union_idemp: ∀U.∀A:U →Prop.
127 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.
128 #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.
130 lemma cap_idemp: ∀U.∀A:U →Prop.
131 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.
132 #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.
134 (* We conclude our examples with a couple of distributivity theorems, and a
135 characterization of substraction in terms of interesection and complementation. *)
137 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
138 (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).
139 #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/]
142 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
143 (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).
144 #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/]
147 lemma substract_def:∀U.∀A,B:U→Prop. A
\ 5a title="substraction" href="cic:/fakeuri.def(1)"
\ 6-
\ 5/a
\ 6B
\ 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.
148 #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/
151 (* In several situation it is important to assume to have a decidable equality
152 between elements of a set U, namely a boolean function eqb: U→U→bool such that
153 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y.
154 A set equipped with such an equality is called a DeqSet: *)
156 record DeqSet : Type[1] ≝ { carr :> Type[0];
157 eqb: carr → carr →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6;
158 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)
161 (* We use the notation == to denote the decidable equality, to distinguish it
162 from the propositional equality. In particular, a term of the form a==b is a
163 boolean, while a=b is a proposition. *)
165 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
166 interpretation "eqb" 'eqb a b = (eqb ? a b).
168 (* It is convenient to have a simple way to reflect a proof of the fact
169 that (eqb a b) is true into a proof of the proposition (a = b); to this aim,
170 we introduce two operators "\P" and "\b". *)
172 notation "\P H" non associative with precedence 90
173 for @{(proj1 … (eqb_true ???) $H)}.
175 notation "\b H" non associative with precedence 90
176 for @{(proj2 … (eqb_true ???) $H)}.
178 (* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
179 \b h: eqb a b = true. Let us see an example of their use: the following
180 statement asserts that we can reflect a proof that eqb a b is false into
181 a proof of the proposition a ≠ b. *)
183 lemma eqb_false: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀a,b:S.
184 (
\ 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.
186 (* We start the proof introducing the hypothesis, and then split the "if" and
191 (* The latter is easily reduced to prove the goal true=false under the assumption
193 [@(
\ 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
195 (* since by assumption H false is equal to (a==b), by rewriting we obtain the goal
196 true=(a==b) that is just the boolean version of H1 *)
198 <H @
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 @(\b H1)
200 (* In the "if" case, we proceed by cases over the boolean equality (a==b); if
201 (a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
202 true, then by reflection a=b, while by hypothesis a≠b *)
204 |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)
208 (* We also introduce two operators "\Pf" and "\bf" to reflect a proof
209 of (a==b)=false into a proof of a≠b, and vice-versa *)
211 notation "\Pf H" non associative with precedence 90
212 for @{(proj1 … (eqb_false ???) $H)}.
214 notation "\bf H" non associative with precedence 90
215 for @{(proj2 … (eqb_false ???) $H)}.
217 (* The following statement proves that propositional equality in a
218 DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
220 lemma 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.
221 #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
222 [%1 @(\P H) | %2 @(\Pf H)]
225 (* A simple example of a set with a decidable equality is bool. We first define
226 the boolean equality beqb, that is just the xand function, then prove that
227 beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by
228 instantiating the DeqSet record with the previous information *)
230 definition beqb ≝ λb1,b2.
231 match b1 with [ true ⇒ b2 | false ⇒
\ 5a href="cic:/matita/basics/bool/notb.def(1)"
\ 6notb
\ 5/a
\ 6 b2].
233 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
235 lemma 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).
236 #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/
239 definition 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.
241 (* At this point, we would expect to be able to prove things like the
242 following: for any boolean b, if b==false is true then b=false.
243 Unfortunately, this would not work, unless we declare b of type
244 DeqBool (change the type in the following statement and see what
247 example 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 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.
251 (* The point is that == expects in input a pair of objects whose type must be the
252 carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
253 system has no knowledge of it (it is an information that has been supplied by the
254 user, and stored somewhere in the library). More explicitly, the type inference
255 inference system, would face an unification problem consisting to unify bool
256 against the carrier of something (a metavaribale) and it has no way to synthetize
257 the answer. To solve this kind of situations, matita provides a mechanism to hint
258 the system the expected solution. A unification hint is a kind of rule, whose rhd
259 is the unification problem, containing some metavariables X1, ..., Xn, and whose
260 left hand side is the solution suggested to the system, in the form of equations
261 Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
262 is, if it is a unifier for the given problem.
263 To make an example, in the previous case, the unification problem is bool = carr X,
264 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
265 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
267 unification hint 0
\ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"
\ 6≔
\ 5/a
\ 6 ;
268 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
269 (* ---------------------------------------- *) ⊢
270 \ 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.
272 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;
273 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
274 (* ---------------------------------------- *) ⊢
275 \ 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.
277 (* After having provided the previous hints, we may rewrite example exhint
278 declaring b of type bool. *)
280 example 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 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.
284 (* The cartesian product of two DeqSets is still a DeqSet. To prove
285 this, we must as usual define the boolen equality function, and prove
286 it correctly reflects propositional equality. *)
288 definition eq_pairs ≝
289 λ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="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="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 p2).
291 lemma 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.
292 \ 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.
293 #A #B * #a1 #b1 * #a2 #b2 %
294 [#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) //
295 |#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)) //
299 definition DeqProd ≝ λA,B:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.
300 \ 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).
302 (* Having an unification problem of the kind T1×T2 = carr X, what kind
303 of hint can we give to the system? We expect T1 to be the carrier of a
304 DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
305 This is expressed by the following hint: *)
307 unification hint 0
\ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"
\ 6≔
\ 5/a
\ 6 C1,C2;
308 T1 ≟
\ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"
\ 6carr
\ 5/a
\ 6 C1,
309 T2 ≟
\ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"
\ 6carr
\ 5/a
\ 6 C2,
310 X ≟
\ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"
\ 6DeqProd
\ 5/a
\ 6 C1 C2
311 (* ---------------------------------------- *) ⊢
312 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.
314 unification hint 0
\ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"
\ 6≔
\ 5/a
\ 6 T1,T2,p1,p2;
315 X ≟
\ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"
\ 6DeqProd
\ 5/a
\ 6 T1 T2
316 (* ---------------------------------------- *) ⊢
317 \ 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.
319 example hint2: ∀b1,b2.
320 \ 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="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="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="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〉.