weblib/tutorial/chapter4.ma

   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. *)
   3
   4 include "basics/logic.ma".
   5
   6 (**** For instance the empty set is defined by the always function predicate *)
   7
   8 definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
   9 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
  10 interpretation "empty set" 'empty_set = (empty_set ?).
  11
  12 (* Similarly, a singleton set contaning containing an element a, is defined
  13 by by the characteristic function asserting equality with a *)
  14
  15 definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6a.
  16 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
  17 interpretation "singleton" 'singl x = (singleton ? x).
  18
  19 (* The membership relation between an element of type A and a set S:A →Prop is
  20 simply the predicate resulting from the application of S to a.
  21 The operations of union, intersection, complement and substraction
  22 are easily defined in terms of the propositional connectives of dijunction,
  23 conjunction and negation *)
  24
  25 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.
  26 interpretation "union" 'union a b = (union ? a b).
  27
  28 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.
  29 interpretation "intersection" 'intersects a b = (intersection ? a b).
  30
  31 definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
  32 interpretation "complement" 'not a = (complement ? a).
  33
  34 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.
  35 interpretation "substraction" 'minus a b = (substraction ? a b).
  36
  37 (* Finally, we use implication to define the inclusion relation between
  38 sets *)
  39
  40 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
  41 interpretation "subset" 'subseteq a b = (subset ? a b).
  42
  43 (* Two sets are equals if and only if they have the same elements, that is,
  44 if the two characteristic functions are extensionally equivalent: *)
  45
  46 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.
  47 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
  48 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
  49
  50 (* This notion of equality is different from the intensional equality of
  51 functions; the fact it defines an equivalence relation must be explicitly
  52 proved: *)
  53
  54 lemma eqP_sym: ∀U.∀A,B:U →Prop.
  55   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.
  56 #U #A #B #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @eqAB qed.
  57
  58 lemma eqP_trans: ∀U.∀A,B,C: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 C → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C.
  60 #U #A #B #C #eqAB #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 // qed.
  61
  62 (* For the same reason, we must also prove that all the operations behave well
  63 with respect to eqP: *)
  64
  65 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
  66   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.
  67 #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.
  68
  69 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
  70   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.
  71 #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.
  72
  73 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
  74   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.
  75 #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.
  76
  77 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
  78   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.
  79 #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.
  80
  81 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
  82   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.
  83 #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.
  84
  85 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
  86   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.
  87 #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.
  88
  89 (* We can now prove several properties of the previous set-theoretic
  90 operations. In particular, union is commutative and associative, and
  91 the empty set is an identity element: *)
  92
  93 lemma union_empty_r: ∀U.∀A:U→Prop.
  94   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.
  95 #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/]
  96 qed.
  97
  98 lemma union_comm : ∀U.∀A,B:U →Prop.
  99   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.
 100 #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.
 101
 102 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
 103   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).
 104 #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/]
 105 qed.
 106
 107 (* In the same way we prove commutativity and associativity for set
 108 interesection *)
 109
 110 lemma cap_comm : ∀U.∀A,B:U →Prop.
 111   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.
 112 #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.
 113
 114 lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
 115   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.
 116 #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/ ]
 117 qed.
 118
 119 (* We can also easily prove idempotency for union and intersection *)
 120
 121 lemma union_idemp: ∀U.∀A:U →Prop.
 122   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.
 123 #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.
 124
 125 lemma cap_idemp: ∀U.∀A:U →Prop.
 126   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.
 127 #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.
 128
 129 (* We conclude our examples with a couple of distributivity theorems,
 130 and a characterization of substraction in terms of interesection and
 131 complementation. *)
 132
 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/]
 136 qed.
 137
 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/]
 141 qed.
 142
 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/
 145 qed.
 146
 147 (****** DeqSet: a set with a decidbale equality ******)
 148
 149 record DeqSet : Type[1] ≝ { carr :> Type[0];
 150    eqb: carr → carr → bool;
 151    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
 152 }.
 153
 154 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 155 interpretation "eqb" 'eqb a b = (eqb ? a b).
 156
 157 notation "\P H" non associative with precedence 90
 158   for @{(proj1 … (eqb_true ???) $H)}.
 159
 160 notation "\b H" non associative with precedence 90
 161   for @{(proj2 … (eqb_true ???) $H)}.
 162
 163 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
 164   (eqb ? a b) = false ↔ a ≠ b.
 165 #S #a #b % #H
 166   [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
 167   |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
 168   ]
 169 qed.
 170
 171 notation "\Pf H" non associative with precedence 90
 172   for @{(proj1 … (eqb_false ???) $H)}.
 173
 174 notation "\bf H" non associative with precedence 90
 175   for @{(proj2 … (eqb_false ???) $H)}.
 176
 177 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
 178 #S #a #b cases (true_or_false (eqb ? a b)) #H
 179   [%1 @(\P H) | %2 @(\Pf H)]
 180 qed.
 181
 182 definition beqb ≝ λb1,b2.
 183   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
 184
 185 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
 186 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
 187 #b1 #b2 cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace conj\ 5/span\ 6\ 5/span\ 6/
 188 qed.
 189
 190 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
 191
 192 unification hint  0 ≔ ;
 193     X ≟ mk_DeqSet bool beqb beqb_true
 194 (* ---------------------------------------- *) ⊢
 195     bool ≡ carr X.
 196
 197 unification hint  0 ≔ b1,b2:bool;
 198     X ≟ mk_DeqSet bool beqb beqb_true
 199 (* ---------------------------------------- *) ⊢
 200     beqb b1 b2 ≡ eqb X b1 b2.
 201
 202 example exhint: ∀b:bool. (b == false) = true → b = false.
 203 #b #H @(\P H).
 204 qed.
 205
 206 (* pairs *)
 207 definition eq_pairs ≝
 208   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 209
 210 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
 211   eq_pairs A B p1 p2 = true ↔ p1 = p2.
 212 #A #B * #a1 #b1 * #a2 #b2 %
 213   [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
 214   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
 215   ]
 216 qed.
 217
 218 definition DeqProd ≝ λA,B:DeqSet.
 219   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
 220
 221 unification hint  0 ≔ C1,C2;
 222     T1 ≟ carr C1,
 223     T2 ≟ carr C2,
 224     X ≟ DeqProd C1 C2
 225 (* ---------------------------------------- *) ⊢
 226     T1×T2 ≡ carr X.
 227
 228 unification hint  0 ≔ T1,T2,p1,p2;
 229     X ≟ DeqProd T1 T2
 230 (* ---------------------------------------- *) ⊢
 231     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
 232
 233 example hint2: ∀b1,b2.
 234   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 235 #b1 #b2 #H @(\P H).