1 (* In this Chapter we shall develop a naif theory of sets represented as characteristic
2 predicates over some universe
\ 5code
\ 6A
\ 5/code
\ 6, that is as objects of type A→Prop. *)
4 include "basics/types.ma".
5 include "basics/bool.ma".
7 (**** For instance the empty set is defined by the always function predicate *)
9 definition empty_set ≝ λA:Type[0].λa:A.
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
10 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
11 interpretation "empty set" 'empty_set = (empty_set ?).
13 (* Similarly, a singleton set contaning containing an element a, is defined
14 by by the characteristic function asserting equality with a *)
16 definition singleton ≝ λA.λx,a:A.x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6a.
17 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
18 interpretation "singleton" 'singl x = (singleton ? x).
20 (* The membership relation between an element of type A and a set S:A →Prop is
21 simply the predicate resulting from the application of S to a.
22 The operations of union, intersection, complement and substraction
23 are easily defined in terms of the propositional connectives of dijunction,
24 conjunction and negation *)
26 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.
27 interpretation "union" 'union a b = (union ? a b).
29 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 Q a.
30 interpretation "intersection" 'intersects a b = (intersection ? a b).
32 definition complement ≝ λU:Type[0].λA:U → Prop.λw.
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 A w.
33 interpretation "complement" 'not a = (complement ? a).
35 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.
36 interpretation "substraction" 'minus a b = (substraction ? a b).
38 (* Finally, we use implication to define the inclusion relation between
41 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
42 interpretation "subset" 'subseteq a b = (subset ? a b).
44 (* Two sets are equals if and only if they have the same elements, that is,
45 if the two characteristic functions are extensionally equivalent: *)
47 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 Q a.
48 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
49 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
51 (* This notion of equality is different from the intensional equality of
52 functions; the fact it defines an equivalence relation must be explicitly
55 lemma eqP_sym: ∀U.∀A,B:U →Prop.
56 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.
57 #U #A #B #eqAB #a @
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @eqAB qed.
59 lemma eqP_trans: ∀U.∀A,B,C: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 C → A
\ 5a title="extensional equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 61 C.
61 #U #A #B #C #eqAB #eqBC #a @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 // qed.
63 (* For the same reason, we must also prove that all the operations behave well
64 with respect to eqP: *)
66 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
67 A
\ 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 C
\ 5a title="union" href="cic:/fakeuri.def(1)"
\ 6∪
\ 5/a
\ 6 B.
68 #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.
70 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
71 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.
72 #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.
74 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
75 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.
76 #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.
78 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
79 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 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.
80 #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.
82 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
83 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.
84 #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.
86 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
87 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.
88 #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.
90 (* We can now prove several properties of the previous set-theoretic operations.
91 In particular, union is commutative and associative, and the empty set is an
94 lemma union_empty_r: ∀U.∀A:U→Prop.
95 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.
96 #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/]
99 lemma union_comm : ∀U.∀A,B:U →Prop.
100 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.
101 #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.
103 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
104 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).
105 #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,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/]
108 (* In the same way we prove commutativity and associativity for set
111 lemma cap_comm : ∀U.∀A,B:U →Prop.
112 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.
113 #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.
115 lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
116 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.
117 #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/ ]
120 (* We can also easily prove idempotency for union and intersection *)
122 lemma union_idemp: ∀U.∀A:U →Prop.
123 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.
124 #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.
126 lemma cap_idemp: ∀U.∀A:U →Prop.
127 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.
128 #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.
130 (* We conclude our examples with a couple of distributivity theorems, and a
131 characterization of substraction in terms of interesection and complementation. *)
133 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
134 (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).
135 #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/]
138 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
139 (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).
140 #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/]
143 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.
144 #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/
147 (* In several situation it is important to assume to have a decidable equality
148 between elements of a set U, namely a boolean function eqb: U→U→bool such that
149 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y.
150 A set equipped with such an equality is called a DeqSet: *)
152 record DeqSet : Type[1] ≝ { carr :> Type[0];
153 eqb: carr → carr →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6;
154 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)
157 (* We use the notation == to denote the decidable equality, to distinguish it
158 from the propositional equality. In particular, a term of the form a==b is a
159 boolean, while a=b is a proposition. *)
161 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
162 interpretation "eqb" 'eqb a b = (eqb ? a b).
164 (* It is convenient to have a simple way to reflect a proof of the fact
165 that (eqb a b) is true into a proof of the proposition (a = b); to this aim,
166 we introduce two operators "\P" and "\b". *)
168 notation "\P H" non associative with precedence 90
169 for @{(proj1 … (eqb_true ???) $H)}.
171 notation "\b H" non associative with precedence 90
172 for @{(proj2 … (eqb_true ???) $H)}.
174 (* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
175 \b h: eqb a b = true. Let us see an example of their use: the following
176 statement asserts that we can reflect a proof that eqb a b is false into
177 a proof of the proposition a ≠ b. *)
179 lemma eqb_false: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀a,b:S.
180 (
\ 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.
182 (* We start the proof introducing the hypothesis, and then split the "if" and
187 (* The latter is easily reduced to prove the goal true=false under the assumption
189 [@(
\ 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
191 (* since by assumption H false is equal to (a==b), by rewriting we obtain the goal
192 true=(a==b) that is just the boolean version of H1 *)
194 <H @
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 @(\b H1)
196 (* In the "if" case, we proceed by cases over the boolean equality (a==b); if
197 (a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
198 true, then by reflection a=b, while by hypothesis a≠b *)
200 |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)
204 (* We also introduce two operators "\Pf" and "\bf" to reflect a proof
205 of (a==b)=false into a proof of a≠b, and vice-versa *)
207 notation "\Pf H" non associative with precedence 90
208 for @{(proj1 … (eqb_false ???) $H)}.
210 notation "\bf H" non associative with precedence 90
211 for @{(proj2 … (eqb_false ???) $H)}.
213 (* The following statement proves that propositional equality in a
214 DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
216 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.
217 #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
218 [%1 @(\P H) | %2 @(\Pf H)]
221 (* A simple example of a set with a decidable equality is bool. We first define
222 the boolean equality beqb, that is just the xand function, then prove that
223 beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by
224 instantiating the DeqSet record with the previous information *)
226 definition beqb ≝ λb1,b2.
227 match b1 with [ true ⇒ b2 | false ⇒
\ 5a href="cic:/matita/basics/bool/notb.def(1)"
\ 6notb
\ 5/a
\ 6 b2].
229 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
231 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).
232 #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/
235 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.
237 (* At this point, we would expect to be able to prove things like the
238 following: for any boolean b, if b==false is true then b=false.
239 Unfortunately, this would not work, unless we declare b of type
240 DeqBool (change the type in the following statement and see what
243 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.
247 (* The point is that == expects in input a pair of objects object whose type
248 must be the carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the
249 type inference system has no knowledge of it (it is an information that has been
250 supplied by the user, and stored somewhere in the library). More explicitly, the
251 type inference inference system, would face an unification problem consisting to
252 unify bool against the carrier of something (a metavaribale) and it has no way to
253 synthetize the answer. To solve this kind of situations, matita provides a
254 mechanism to hint the system the expected solution. A unification hint is a kind of
255 rule, whose rhd is the unification problem, containing some metavariables X1, ...,
256 Xn, and whose left hand side is the solution suggested to the system, in the form
257 of equations Xi=Mi. The hint is accepted by the system if and only the solution is
258 correct, that is, if it is a unifier for the given problem.
259 To make an example, in the previous case, the unification problem is bool = carr X,
260 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
261 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
263 unification hint 0
\ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"
\ 6≔
\ 5/a
\ 6 ;
264 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
265 (* ---------------------------------------- *) ⊢
266 \ 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.
268 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;
269 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
270 (* ---------------------------------------- *) ⊢
271 \ 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.
273 (* After having provided the previous hints, we may rewrite example exhint delcaring
276 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.
281 definition eq_pairs ≝
282 λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
284 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
285 eq_pairs A B p1 p2 = true ↔ p1 = p2.
286 #A #B * #a1 #b1 * #a2 #b2 %
287 [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
288 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
292 definition DeqProd ≝ λA,B:DeqSet.
293 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
295 unification hint 0 ≔ C1,C2;
299 (* ---------------------------------------- *) ⊢
302 unification hint 0 ≔ T1,T2,p1,p2;
304 (* ---------------------------------------- *) ⊢
305 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
307 example hint2: ∀b1,b2.
308 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.