weblib/cicm2012/part2.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 "∅" non associative with precedence 90 for @{'empty_set}.
  14 interpretation "empty set" 'empty_set = (empty_set ?).
  15
  16 (* Similarly, a singleton set containing an element a, is defined
  17 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\ 6a.
  20 (* notation "{x}" non associative with precedence 90 for @{'singl $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 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="difference"\ 6definition difference := λ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 "difference" 'minus a b = (difference ? 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 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 (* the fact it defines an equivalence relation must be explicitly proved: *)
  57
  58 \ 5img class="anchor" src="icons/tick.png" id="eqP_sym"\ 6lemma eqP_sym: ∀U.∀A,B:U →Prop.
  59   A =1 B → B =1 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_trans"\ 6lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
  63   A =1 B → B =1 C → A =1 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_union_r"\ 6lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
  70   A =1 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B =1 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_union_l"\ 6lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
  74   B =1 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B =1 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_intersect_r"\ 6lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
  78   A =1 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B =1 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_intersect_l"\ 6lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
  82   B =1 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B =1 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_substract_r"\ 6lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
  86   A =1 C  → A \ 5a title="difference" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B =1 C \ 5a title="difference" 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 \ 5img class="anchor" src="icons/tick.png" id="eqP_substract_l"\ 6lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
  90   B =1 C  → A \ 5a title="difference" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B =1 A \ 5a title="difference" 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 (*
  94 \ 5h2 class="section"\ 6Simple properties of sets\ 5/h2\ 6
  95 We can now prove several properties of the previous set-theoretic operations.
  96 In particular, union is commutative and associative, and the empty set is an
  97 identity element: *)
  98
  99 \ 5img class="anchor" src="icons/tick.png" id="union_empty_r"\ 6lemma union_empty_r: ∀U.∀A:U→Prop.
 100   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 =1 A.
 101 #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/]
 102 qed.
 103
 104 \ 5img class="anchor" src="icons/tick.png" id="union_comm"\ 6lemma union_comm : ∀U.∀A,B:U →Prop.
 105   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B =1 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A.
 106 #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
 108 \ 5img class="anchor" src="icons/tick.png" id="union_assoc"\ 6lemma union_assoc: ∀U.∀A,B,C:U → Prop.
 109   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 =1 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).
 110 #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/]
 111 qed.
 112
 113 (* In the same way we prove commutativity and associativity for set
 114 interesection *)
 115
 116 \ 5img class="anchor" src="icons/tick.png" id="cap_comm"\ 6lemma cap_comm : ∀U.∀A,B:U →Prop.
 117   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B =1 B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 A.
 118 #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
 120 \ 5img class="anchor" src="icons/tick.png" id="cap_assoc"\ 6lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
 121   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) =1 (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.
 122 #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/ ]
 123 qed.
 124
 125 (* We can also easily prove idempotency for union and intersection *)
 126
 127 \ 5img class="anchor" src="icons/tick.png" id="union_idemp"\ 6lemma union_idemp: ∀U.∀A:U →Prop.
 128   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A =1 A.
 129 #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
 131 \ 5img class="anchor" src="icons/tick.png" id="cap_idemp"\ 6lemma cap_idemp: ∀U.∀A:U →Prop.
 132   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 A =1 A.
 133 #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
 135 (* We conclude our examples with a couple of distributivity theorems, and a
 136 characterization of substraction in terms of interesection and complementation. *)
 137
 138 \ 5img class="anchor" src="icons/tick.png" id="distribute_intersect"\ 6lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
 139   (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 =1 (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).
 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/]
 141 qed.
 142
 143 \ 5img class="anchor" src="icons/tick.png" id="distribute_substract"\ 6lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
 144   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="difference" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C =1 (A \ 5a title="difference" 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="difference" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C).
 145 #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/]
 146 qed.
 147
 148 \ 5img class="anchor" src="icons/tick.png" id="substract_def"\ 6lemma substract_def:∀U.∀A,B:U→Prop. A\ 5a title="difference" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6B =1 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.
 149 #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/
 150 qed.
 151
 152 (*
 153 \ 5h2 class="section"\ 6Bool vs. Prop\ 5/h2\ 6
 154 In several situation it is important to assume to have a decidable equality
 155 between elements of a set U, namely a boolean function eqb: U→U→bool such that
 156 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y.
 157 A set equipped with such an equality is called a DeqSet: *)
 158
 159 \ 5img class="anchor" src="icons/tick.png" id="DeqSet"\ 6record DeqSet : Type[1] ≝ { carr :> Type[0];
 160    eqb: carr → carr → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
 161    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)
 162 }.
 163
 164 (* We use the notation == to denote the decidable equality, to distinguish it
 165 from the propositional equality. In particular, a term of the form a==b is a
 166 boolean, while a=b is a proposition. *)
 167
 168 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 169 interpretation "eqb" 'eqb a b = (eqb ? a b).
 170
 171 (*
 172 \ 5h2 class="section"\ 6Small Scale Reflection\ 5/h2\ 6
 173 It is convenient to have a simple way to reflect a proof of the fact
 174 that (eqb a b) is true into a proof of the proposition (a = b); to this aim,
 175 we introduce two operators "\P" and "\b". *)
 176
 177 notation "\P H" non associative with precedence 90
 178   for @{(proj1 … (eqb_true ???) $H)}.
 179
 180 notation "\b H" non associative with precedence 90
 181   for @{(proj2 … (eqb_true ???) $H)}.
 182
 183 (* If H:eqb a b = true, then \P H: a = b, and conversely if h:a = b, then
 184 \b h: eqb a b = true. Let us see an example of their use: the following
 185 statement asserts that we can reflect a proof that eqb a b is false into
 186 a proof of the proposition a ≠ b. *)
 187
 188 lemma eqb_false: ∀S:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a,b:S.
 189   (\ 5a href="cic:/matita/cicm2012/part2/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.
 190 #S #a #b %
 191 (* same tactic on two goals *)
 192 #H
 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
 194    <H @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @(\b H1)
 195   |cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/cicm2012/part2/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)
 196   ]
 197 qed.
 198
 199 (* We also introduce two operators "\Pf" and "\bf" to reflect a proof
 200 of (a==b)=false into a proof of a≠b, and vice-versa *)
 201
 202 notation "\Pf H" non associative with precedence 90
 203   for @{(proj1 … (eqb_false ???) $H)}.
 204
 205 notation "\bf H" non associative with precedence 90
 206   for @{(proj2 … (eqb_false ???) $H)}.
 207
 208 (* The following statement proves that propositional equality in a
 209 DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
 210
 211  lemma dec_eq: ∀S:\ 5a href="cic:/matita/cicm2012/part2/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.
 212 #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/cicm2012/part2/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 ? a b)) #H
 213   [%1 @(\P H) | %2 @(\Pf H)]
 214 qed.
 215
 216 (*
 217 \ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
 218 A simple example of a set with a decidable equality is bool. We first define
 219 the boolean equality beqb, then prove that beqb b1 b2 is true if and only if
 220 b1=b2, and finally build the type DeqBool by instantiating the DeqSet record
 221 with the previous information *)
 222
 223 definition beqb ≝ λb1,b2.
 224   match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2].
 225
 226 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
 227 lemma beqb_true: ∀b1,b2. \ 5a href="cic:/matita/cicm2012/part2/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 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b2.
 228 #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/
 229 qed.
 230
 231 definition DeqBool ≝ \ 5a href="cic:/matita/cicm2012/part2/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/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
 232
 233 (* At this point, we would expect to be able to prove things like the
 234 following: for any boolean b, if b==false is true then b=false.
 235 Unfortunately, this would not work, unless we declare b of type
 236 DeqBool (change the type in the following statement and see what
 237 happens). *)
 238
 239 example exhint: ∀b:\ 5a href="cic:/matita/cicm2012/part2/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.
 240 #b #H @(\P H)
 241 qed.
 242
 243 (* The point is that == expects in input a pair of objects whose type must be the
 244 carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
 245 system has no knowledge of it (it is an information that has been supplied by the
 246 user, and stored somewhere in the library). More explicitly, the type inference
 247 inference system, would face an unification problem consisting to unify bool
 248 against the carrier of something (a metavaribale) and it has no way to synthetize
 249 the answer. To solve this kind of situations, matita provides a mechanism to hint
 250 the system the expected solution. A unification hint is a kind of rule, whose rhd
 251 is the unification problem, containing some metavariables X1, ..., Xn, and whose
 252 left hand side is the solution suggested to the system, in the form of equations
 253 Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
 254 is, if it is a unifier for the given problem.
 255 To make an example, in the previous case, the unification problem is bool = carr X,
 256 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
 257 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
 258
 259 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ;
 260     X ≟ \ 5a href="cic:/matita/cicm2012/part2/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/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6
 261 (* ---------------------------------------- *) ⊢
 262     \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≡ \ 5a href="cic:/matita/cicm2012/part2/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
 263
 264 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;
 265     X ≟ \ 5a href="cic:/matita/cicm2012/part2/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/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/cicm2012/part2/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6
 266 (* ---------------------------------------- *) ⊢
 267     \ 5a href="cic:/matita/cicm2012/part2/beqb.def(2)"\ 6beqb\ 5/a\ 6 b1 b2 ≡ \ 5a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X b1 b2.
 268
 269 (* After having provided the previous hints, we may rewrite example exhint
 270 declaring b of type bool. *)
 271
 272 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.
 273 #b #H @(\P H)
 274 qed.
 275
 276 (* The cartesian product of two DeqSets is still a DeqSet. To prove
 277 this, we must as usual define the boolen equality function, and prove
 278 it correctly reflects propositional equality. *)
 279
 280 definition eq_pairs ≝
 281   λA,B:\ 5a href="cic:/matita/cicm2012/part2/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).
 282
 283 lemma eq_pairs_true: ∀A,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀p1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.
 284   \ 5a href="cic:/matita/cicm2012/part2/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.
 285 #A #B * #a1 #b1 * #a2 #b2 %
 286   [#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) //
 287   |#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)) //
 288   ]
 289 qed.
 290
 291 definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/cicm2012/part2/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
 292   \ 5a href="cic:/matita/cicm2012/part2/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/cicm2012/part2/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B) (\ 5a href="cic:/matita/cicm2012/part2/eq_pairs_true.def(6)"\ 6eq_pairs_true\ 5/a\ 6 A B).
 293
 294 (* Having a unification problem of the kind T1×T2 = carr X, what kind
 295 of hint can we give to the system? We expect T1 to be the carrier of a
 296 DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
 297 This is expressed by the following hint: *)
 298
 299 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 C1,C2;
 300     T1 ≟ \ 5a href="cic:/matita/cicm2012/part2/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C1,
 301     T2 ≟ \ 5a href="cic:/matita/cicm2012/part2/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C2,
 302     X ≟ \ 5a href="cic:/matita/cicm2012/part2/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 C1 C2
 303 (* ---------------------------------------- *) ⊢
 304     T1\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6T2 ≡ \ 5a href="cic:/matita/cicm2012/part2/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
 305
 306 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 T1,T2,p1,p2;
 307     X ≟ \ 5a href="cic:/matita/cicm2012/part2/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 T1 T2
 308 (* ---------------------------------------- *) ⊢
 309     \ 5a href="cic:/matita/cicm2012/part2/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 T1 T2 p1 p2 ≡ \ 5a href="cic:/matita/cicm2012/part2/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X p1 p2.
 310
 311 example hint2: ∀b1,b2.
 312   〈b1,\ 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 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 → 〈b1,\ 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 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.
 313 #b1 #b2 #H @(\P H)
 314 qed.