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 definition 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 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.
  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 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.
  30 interpretation "union" 'union a b = (union ? a b).
  31
  32 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.
  33 interpretation "intersection" 'intersects a b = (intersection ? a b).
  34
  35 definition 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 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.
  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 definition 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 (* Two sets are equals if and only if they have the same elements, that is,
  48 if the two characteristic functions are extensionally equivalent: *)
  49
  50 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.
  51 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
  52 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
  53
  54 (* This notion of equality is different from the intensional equality of
  55 functions; the fact it defines an equivalence relation must be explicitly
  56 proved: *)
  57
  58 lemma eqP_sym: ∀U.∀A,B:U →Prop.
  59   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.
  60 #U #A #B #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @eqAB qed.
  61
  62 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
  63   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.
  64 #U #A #B #C #eqAB #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 // qed.
  65
  66 (* For the same reason, we must also prove that all the operations behave well
  67 with respect to eqP: *)
  68
  69 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
  70   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.
  71 #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.
  72
  73 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
  74   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.
  75 #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.
  76
  77 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
  78   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.
  79 #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.
  80
  81 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
  82   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.
  83 #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.
  84
  85 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
  86   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.
  87 #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.
  88
  89 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
  90   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.
  91 #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.
  92
  93 (* We can now prove several properties of the previous set-theoretic operations.
  94 In particular, union is commutative and associative, and the empty set is an
  95 identity element: *)
  96
  97 lemma union_empty_r: ∀U.∀A:U→Prop.
  98   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.
  99 #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/]
 100 qed.
 101
 102 lemma union_comm : ∀U.∀A,B:U →Prop.
 103   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.
 104 #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.
 105
 106 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
 107   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).
 108 #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/]
 109 qed.
 110
 111 (* In the same way we prove commutativity and associativity for set
 112 interesection *)
 113
 114 lemma cap_comm : ∀U.∀A,B:U →Prop.
 115   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.
 116 #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.
 117
 118 lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
 119   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.
 120 #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/ ]
 121 qed.
 122
 123 (* We can also easily prove idempotency for union and intersection *)
 124
 125 lemma union_idemp: ∀U.∀A:U →Prop.
 126   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.
 127 #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.
 128
 129 lemma cap_idemp: ∀U.∀A:U →Prop.
 130   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.
 131 #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.
 132
 133 (* We conclude our examples with a couple of distributivity theorems, and a
 134 characterization of substraction in terms of interesection and complementation. *)
 135
 136 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
 137   (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).
 138 #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/]
 139 qed.
 140
 141 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
 142   (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).
 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 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.
 147 #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/
 148 qed.
 149
 150 (* In several situation it is important to assume to have a decidable equality
 151 between elements of a set U, namely a boolean function eqb: U→U→bool such that
 152 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y.
 153 A set equipped with such an equality is called a DeqSet: *)
 154
 155 record DeqSet : Type[1] ≝ { carr :> Type[0];
 156    eqb: carr → carr → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
 157    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)
 158 }.
 159
 160 (* We use the notation == to denote the decidable equality, to distinguish it
 161 from the propositional equality. In particular, a term of the form a==b is a
 162 boolean, while a=b is a proposition. *)
 163
 164 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 165 interpretation "eqb" 'eqb a b = (eqb ? a b).
 166
 167 (* It is convenient to have a simple way to reflect a proof of the fact
 168 that (eqb a b) is true into a proof of the proposition (a = b); to this aim,
 169 we introduce two operators "\P" and "\b". *)
 170
 171 notation "\P H" non associative with precedence 90
 172   for @{(proj1 … (eqb_true ???) $H)}.
 173
 174 notation "\b H" non associative with precedence 90
 175   for @{(proj2 … (eqb_true ???) $H)}.
 176
 177 (* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
 178 \b h: eqb a b = true. Let us see an example of their use: the following
 179 statement asserts that we can reflect a proof that eqb a b is false into
 180 a proof of the proposition a ≠ b. *)
 181
 182 lemma eqb_false: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S.
 183   (\ 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.
 184
 185 (* We start the proof introducing the hypothesis, and then split the "if" and
 186 "only if" cases *)
 187
 188 #S #a #b % #H
 189
 190 (* The latter is easily reduced to prove the goal true=false under the assumption
 191 H1: a = b *)
 192   [@(\ 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
 193
 194 (* since by assumption H false is equal to (a==b), by rewriting we obtain the goal
 195 true=(a==b) that is just the boolean version of H1 *)
 196
 197   <H @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @(\b H1)
 198
 199 (* In the "if" case, we proceed by cases over the boolean equality (a==b); if
 200 (a==b) is false, the goal is trivial; the other case is absurd, since if (a==b) is
 201 true, then by reflection a=b, while by hypothesis a≠b *)
 202
 203  |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   ]
 205 qed.
 206
 207 (* We also introduce two operators "\Pf" and "\bf" to reflect a proof
 208 of (a==b)=false into a proof of a≠b, and vice-versa *)
 209
 210 notation "\Pf H" non associative with precedence 90
 211   for @{(proj1 … (eqb_false ???) $H)}.
 212
 213 notation "\bf H" non associative with precedence 90
 214   for @{(proj2 … (eqb_false ???) $H)}.
 215
 216 (* The following statement proves that propositional equality in a
 217 DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
 218
 219  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.
 220 #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
 221   [%1 @(\P H) | %2 @(\Pf H)]
 222 qed.
 223
 224 (* A simple example of a set with a decidable equality is bool. We first define
 225 the boolean equality beqb, that is just the xand function, then prove that
 226 beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by
 227 instantiating the DeqSet record with the previous information *)
 228
 229 definition beqb ≝ λb1,b2.
 230   match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2].
 231
 232 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
 233
 234 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).
 235 #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/
 236 qed.
 237
 238 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.
 239
 240 (* At this point, we would expect to be able to prove things like the
 241 following: for any boolean b, if b==false is true then b=false.
 242 Unfortunately, this would not work, unless we declare b of type
 243 DeqBool (change the type in the following statement and see what
 244 happens). *)
 245
 246 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 #b #H @(\P H)
 248 qed.
 249
 250 (* The point is that == expects in input a pair of objects whose type must be the
 251 carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
 252 system has no knowledge of it (it is an information that has been supplied by the
 253 user, and stored somewhere in the library). More explicitly, the type inference
 254 inference system, would face an unification problem consisting to unify bool
 255 against the carrier of something (a metavaribale) and it has no way to synthetize
 256 the answer. To solve this kind of situations, matita provides a mechanism to hint
 257 the system the expected solution. A unification hint is a kind of rule, whose rhd
 258 is the unification problem, containing some metavariables X1, ..., Xn, and whose
 259 left hand side is the solution suggested to the system, in the form of equations
 260 Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
 261 is, if it is a unifier for the given problem.
 262 To make an example, in the previous case, the unification problem is bool = carr X,
 263 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
 264 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
 265
 266 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ;
 267     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
 268 (* ---------------------------------------- *) ⊢
 269     \ 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.
 270
 271 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;
 272     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
 273 (* ---------------------------------------- *) ⊢
 274     \ 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.
 275
 276 (* After having provided the previous hints, we may rewrite example exhint
 277 declaring b of type bool. *)
 278
 279 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.
 280 #b #H @(\P H)
 281 qed.
 282
 283 (* The cartesian product of two DeqSets is still a DeqSet. To prove
 284 this, we must as usual define the boolen equality function, and prove
 285 it correctly reflects propositional equality. *)
 286
 287 definition eq_pairs ≝
 288   λ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).
 289
 290 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.
 291   \ 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.
 292 #A #B * #a1 #b1 * #a2 #b2 %
 293   [#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) //
 294   |#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)) //
 295   ]
 296 qed.
 297
 298 definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
 299   \ 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).
 300
 301 (* Having an unification problem of the kind T1×T2 = carr X, what kind
 302 of hint can we give to the system? We expect T1 to be the carrier of a
 303 DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
 304 This is expressed by the following hint: *)
 305
 306 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 C1,C2;
 307     T1 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C1,
 308     T2 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C2,
 309     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 C1 C2
 310 (* ---------------------------------------- *) ⊢
 311     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.
 312
 313 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 T1,T2,p1,p2;
 314     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 T1 T2
 315 (* ---------------------------------------- *) ⊢
 316     \ 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.
 317
 318 example hint2: ∀b1,b2.
 319   \ 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〉.
 320 #b1 #b2 #H @(\P H).