-definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
-
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
-
-ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
- match a with [ mk_pair e1 b1 ⇒
- match b1 with
- [ false ⇒ 〈e1 · \fst b, \snd b〉
- | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
-
-notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
-interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
-
-ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
- match a with [ mk_pair e1 b1 ⇒
- match b1 with
- [ false ⇒ 〈e1^*, false〉
- | true ⇒ 〈(\fst (bcast ? e1))^*, true〉]].
-
-notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
-interpretation "lk" 'lk op a = (lk ? op a).
-notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
-
-notation > "•" non associative with precedence 60 for @{eclose ?}.
-nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
- match E with
- [ pz ⇒ 〈 ∅, false 〉
- | pe ⇒ 〈 ϵ, true 〉
- | ps x ⇒ 〈 `.x, false 〉
- | pp x ⇒ 〈 `.x, false 〉
- | po E1 E2 ⇒ •E1 ⊕ •E2
- | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
- | pk E ⇒ 〈(\fst (•E))^*,true〉].
-notation < "• x" non associative with precedence 60 for @{'eclose $x}.
-interpretation "eclose" 'eclose x = (eclose ? x).
-notation > "• x" non associative with precedence 60 for @{'eclose $x}.
-
-ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
-interpretation "reclose" 'eclose x = (reclose ? x).
-
-ndefinition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
-notation > "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-notation "A =\sub 1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
-
-naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q.
-
-nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
-#S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
-nqed.
-
-nlemma cupA : ∀S.∀a,b,c:word S → Prop.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; napply extP; #w; nnormalize; @; *; /3/; *; /3/; nqed.
-
-nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
-#S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.
-
-(* theorem 16: 2 *)
-nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2.
-#S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
-nwhd in ⊢ (??(??%)?);
-nchange in ⊢(??%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
-nchange in ⊢(??(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
-nrewrite > (epsilon_or S …); nrewrite > (cupA S (𝐋\p e1) …);
-nrewrite > (cupC ? (ϵ b1) …); nrewrite < (cupA S (𝐋\p e2) …);
-nrewrite > (cupC ? ? (ϵ b1) …); nrewrite < (cupA …); //;
-nqed.
-
-nlemma odotEt :
- ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
-#S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
-
-nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed.
-
-nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r).
-#S p q r; napply extP; #w; nnormalize; @;
-##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
-##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
-nqed.
-
-nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p.
-#S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed.
-
-nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 |e1 · e2| = 𝐋 |e1| · 𝐋 |e2|.
-#S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
-nqed.
-
-nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 |e1 + e2| = 𝐋 |e1| ∪ 𝐋 |e2|.
-#S e1 e2; napply extP; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed.
-
-nlemma erase_star : ∀S.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed.
-
-ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w.
-interpretation "substract" 'minus a b = (substract ? a b).
-
-nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
-#S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed.
-
-nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a.
-#S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed.
-
-nlemma subK : ∀S.∀a:word S → Prop. a - a = {}.
-#S a; napply extP; #w; nnormalize; @; *; /2/; nqed.
-
-nlemma subW : ∀S.∀a,b:word S → Prop.∀w.(a - b) w → a w.
-#S a b w; nnormalize; *; //; nqed.
-
-nlemma erase_bull : ∀S.∀a:pitem S. |\fst (•a)| = |a|.
-#S a; nelim a; // by {};
-##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| · |e2|);
- nrewrite < IH1; nrewrite < IH2;
- nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉));
- ncases (•e1); #e3 b; ncases b; nnormalize;
- ##[ ncases (•e2); //; ##| nrewrite > IH2; //]
-##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| + |e2|);
- nrewrite < IH2; nrewrite < IH1;
- nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2));
- ncases (•e1); ncases (•e2); //;
-##| #e IH; nchange in ⊢ (???%) with (|e|^* ); nrewrite < IH;
- nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##]
-nqed.
-
-nlemma eta_lp : ∀S.∀p:pre S.𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
-#S p; ncases p; //; nqed.
-
-nlemma epsilon_dot: ∀S.∀p:word S → Prop. {[]} · p = p.
-#S e; napply extP; #w; nnormalize; @; ##[##2: #Hw; @[]; @w; /3/; ##]
-*; #w1; *; #w2; *; *; #defw defw1 Hw2; nrewrite < defw; nrewrite < defw1;
-napply Hw2; nqed.
-
-(* theorem 16: 1 → 3 *)
-nlemma odot_dot_aux : ∀S.∀e1,e2: pre S.
- 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 |\fst e2| →
- 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2.
-#S e1 e2 th1; ncases e1; #e1' b1'; ncases b1';
-##[ nwhd in ⊢ (??(??%)?); nletin e2' ≝ (\fst e2); nletin b2' ≝ (\snd e2);
- nletin e2'' ≝ (\fst (•(\fst e2))); nletin b2'' ≝ (\snd (•(\fst e2)));
- nchange in ⊢ (??%?) with (?∪?);
- nchange in ⊢ (??(??%?)?) with (?∪?);
- nchange in match (𝐋\p 〈?,?〉) with (?∪?);
- nrewrite > (epsilon_or …); nrewrite > (cupC ? (ϵ ?)…);
- nrewrite > (cupA …);nrewrite < (cupA ?? (ϵ?)…);
- nrewrite > (?: 𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 |e2'|); ##[##2:
- nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 |e2'|);
- ngeneralize in match th1;
- nrewrite > (eta_lp…); #th1; nrewrite > th1; //;##]
- nrewrite > (eta_lp ? e2);
- nchange in match (𝐋\p 〈\fst e2,?〉) with (𝐋\p e2'∪ ϵ b2');
- nrewrite > (cup_dotD …); nrewrite > (epsilon_dot…);
- nrewrite > (cupC ? (𝐋\p e2')…); nrewrite > (cupA…);nrewrite > (cupA…);
- nrewrite < (erase_bull S e2') in ⊢ (???(??%?)); //;
-##| ncases e2; #e2' b2'; nchange in match (〈e1',false〉⊙?) with 〈?,?〉;
- nchange in match (𝐋\p ?) with (?∪?);
- nchange in match (𝐋\p (e1'·?)) with (?∪?);
- nchange in match (𝐋\p 〈e1',?〉) with (?∪?);
- nrewrite > (cup0…);
- nrewrite > (cupA…); //;##]
-nqed.
-
-nlemma sub_dot_star :
- ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*.
-#S X b; napply extP; #w; @;
-##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //]
- *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj;
- @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //;
- @; //; napply (subW … sube);
-##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
- #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *;
- ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2;
- @; ncases b in H1; #H1;
- ##[##2: nrewrite > (sub0…); @w'; @(w1@w2);
- nrewrite > (associative_append ? w' w1 w2);
- nrewrite > defwl'; @; ##[@;//] @(wl'); @; //;
- ##| ncases w' in Pw';
- ##[ #ne; @w1; @w2; nrewrite > defwl'; @; //; @; //;
- ##| #x xs Px; @(x::xs); @(w1@w2);
- nrewrite > (defwl'); @; ##[@; //; @; //; @; nnormalize; #; ndestruct]
- @wl'; @; //; ##] ##]
- ##| #wlnil; nchange in match (flatten ? (w'::wl')) with (w' @ flatten ? wl');
- nrewrite < (wlnil); nrewrite > (append_nil…); ncases b;
- ##[ ncases w' in Pw'; /2/; #x xs Pxs; @; @(x::xs); @([]);
- nrewrite > (append_nil…); @; ##[ @; //;@; //; nnormalize; @; #; ndestruct]
- @[]; @; //;
- ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //]
- @; //; @; //; @; *;##]##]##]
-nqed.
-
-(* theorem 16: 1 *)
-alias symbol "pc" (instance 13) = "cat lang".
-alias symbol "in_pl" (instance 23) = "in_pl".
-alias symbol "in_pl" (instance 5) = "in_pl".
-alias symbol "eclose" (instance 21) = "eclose".
-ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|.
-#S e; nelim e; //;
- ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror;
- ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *;
- ##| #e1 e2 IH1 IH2;
- nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
- nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
- nrewrite > (IH1 …); nrewrite > (cup_dotD …);
- nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
- nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
- nrewrite < (erase_dot …); nrewrite < (cupA …); //;
- ##| #e1 e2 IH1 IH2;
- nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …);
- nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …);
- nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…);
- nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …);
- nrewrite < (erase_plus …); //.
- ##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH;
- nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
- nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]});
- nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* );
- nrewrite > (erase_bull…e);
- nrewrite > (erase_star …);
- nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[##2:
- nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH;
- ##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH;
- nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//;
- ##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##]
- nrewrite > (cup_dotD…); nrewrite > (cupA…);
- nrewrite > (?: ((?·?)∪{[]} = 𝐋 |e^*|)); //;
- nchange in match (𝐋 |e^*|) with ((𝐋 |e|)^* ); napply sub_dot_star;##]
- nqed.
-
-(* theorem 16: 3 *)
-nlemma odot_dot:
- ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2.
-#S e1 e2; napply odot_dot_aux; napply (bull_cup S (\fst e2)); nqed.
-
-nlemma dot_star_epsilon : ∀S.∀e:re S.𝐋 e · 𝐋 e^* ∪ {[]} = 𝐋 e^*.
-#S e; napply extP; #w; nnormalize; @;
-##[ *; ##[##2: #H; nrewrite < H; @[]; /3/] *; #w1; *; #w2;
- *; *; #defw Hw1; *; #wl; *; #defw2 Hwl; @(w1 :: wl);
- nrewrite < defw; nrewrite < defw2; @; //; @;//;
-##| *; #wl; *; #defw Hwl; ncases wl in defw Hwl; ##[#defw; #; @2; nrewrite < defw; //]
- #x xs defw; *; #Hx Hxs; @; @x; @(flatten ? xs); nrewrite < defw;
- @; /2/; @xs; /2/;##]
- nqed.
-
-nlemma nil_star : ∀S.∀e:re S. [ ] ∈ e^*.
-#S e; @[]; /2/; nqed.
-
-nlemma cupID : ∀S.∀l:word S → Prop.l ∪ l = l.
-#S l; napply extP; #w; @; ##[*]//; #; @; //; nqed.
-
-nlemma cup_star_nil : ∀S.∀l:word S → Prop. l^* ∪ {[]} = l^*.
-#S a; napply extP; #w; @; ##[*; //; #H; nrewrite < H; @[]; @; //] #;@; //;nqed.
-
-nlemma rcanc_sing : ∀S.∀A,C:word S → Prop.∀b:word S .
- ¬ (A b) → A ∪ { (b) } = C → A = C - { (b) }.
-#S A C b nbA defC; nrewrite < defC; napply extP; #w; @;
-##[ #Aw; /3/| *; *; //; #H nH; ncases nH; #abs; nlapply (abs H); *]
-nqed.
-
-(* theorem 16: 4 *)
-nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 |\fst e|)^*.
-#S p; ncases p; #e b; ncases b;
-##[ nchange in match (〈e,true〉^⊛) with 〈?,?〉;
- nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e));
- nchange in ⊢ (??%?) with (?∪?);
- nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* );
- nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b' )); ##[##2:
- nlapply (bull_cup ? e); #bc;
- nchange in match (𝐋\p (•e)) in bc with (?∪?);
- nchange in match b' in bc with b';
- ncases b' in bc; ##[##2: nrewrite > (cup0…); nrewrite > (sub0…); //]
- nrewrite > (cup_sub…); ##[napply rcanc_sing] //;##]
- nrewrite > (cup_dotD…); nrewrite > (cupA…);nrewrite > (erase_bull…);
- nrewrite > (sub_dot_star…);
- nchange in match (𝐋\p 〈?,?〉) with (?∪?);
- nrewrite > (cup_dotD…); nrewrite > (epsilon_dot…); //;
-##| nwhd in match (〈e,false〉^⊛); nchange in match (𝐋\p 〈?,?〉) with (?∪?);
- nrewrite > (cup0…);
- nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* );
- nrewrite < (cup0 ? (𝐋\p e)); //;##]
-nqed.
-
-nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝
- match e with
- [ z ⇒ pz ?
- | e ⇒ pe ?
- | s x ⇒ ps ? x
- | c e1 e2 ⇒ pc ? (pre_of_re ? e1) (pre_of_re ? e2)
- | o e1 e2 ⇒ po ? (pre_of_re ? e1) (pre_of_re ? e2)
- | k e1 ⇒ pk ? (pre_of_re ? e1)].
-
-nlemma notFalse : ¬False. @; //; nqed.
-
-nlemma dot0 : ∀S.∀A:word S → Prop. {} · A = {}.
-#S A; nnormalize; napply extP; #w; @; ##[##2: *]
-*; #w1; *; #w2; *; *; //; nqed.
-
-nlemma Lp_pre_of_re : ∀S.∀e:re S. 𝐋\p (pre_of_re ? e) = {}.
-#S e; nelim e; ##[##1,2,3: //]
-##[ #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1 e2))) with (?∪?);
- nrewrite > H1; nrewrite > H2; nrewrite > (dot0…); nrewrite > (cupID…);//
-##| #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1+e2))) with (?∪?);
- nrewrite > H1; nrewrite > H2; nrewrite > (cupID…); //
-##| #e1 H1; nchange in match (𝐋\p (pre_of_re S (e1^* ))) with (𝐋\p (pre_of_re ??) · ?);
- nrewrite > H1; napply dot0; ##]
-nqed.
-
-nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 |pre_of_re S e| = 𝐋 e.
-#S A; nelim A; //;
-##[ #e1 e2 H1 H2; nchange in match (𝐋 (e1 · e2)) with (𝐋 e1·?);
- nrewrite < H1; nrewrite < H2; //
-##| #e1 e2 H1 H2; nchange in match (𝐋 (e1 + e2)) with (𝐋 e1 ∪ ?);
- nrewrite < H1; nrewrite < H2; //
-##| #e1 H1; nchange in match (𝐋 (e1^* )) with ((𝐋 e1)^* );
- nrewrite < H1; //]
-nqed.
-
-(* corollary 17 *)
-nlemma L_Lp_bull : ∀S.∀e:re S.𝐋 e = 𝐋\p (•pre_of_re ? e).
-#S e; nrewrite > (bull_cup…); nrewrite > (Lp_pre_of_re…);
-nrewrite > (cupC…); nrewrite > (cup0…); nrewrite > (erase_pre_of_reK…); //;
-nqed.
-
-nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w.
-#S f g H; nrewrite > H; //; nqed.
+(*
+\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
+A simple example of a set with a decidable equality is bool. We first define
+the boolean equality beqb, that is just the xand function, then prove that
+beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by
+instantiating the DeqSet record with the previous information *)
+
+\ 5img class="anchor" src="icons/tick.png" id="beqb"\ 6definition beqb ≝ λb1,b2.
+ match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2].
+
+notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
+
+\ 5img class="anchor" src="icons/tick.png" id="beqb_true"\ 6lemma 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).
+#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/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="DeqBool"\ 6definition 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.
+
+(* At this point, we would expect to be able to prove things like the
+following: for any boolean b, if b==false is true then b=false.
+Unfortunately, this would not work, unless we declare b of type
+DeqBool (change the type in the following statement and see what
+happens). *)
+
+\ 5img class="anchor" src="icons/tick.png" id="exhint"\ 6example 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 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.
+#b #H @(\P H)
+qed.
+
+(* The point is that == expects in input a pair of objects whose type must be the
+carrier of a DeqSet; bool is indeed the carrier of DeqBool, but the type inference
+system has no knowledge of it (it is an information that has been supplied by the
+user, and stored somewhere in the library). More explicitly, the type inference
+inference system, would face an unification problem consisting to unify bool
+against the carrier of something (a metavaribale) and it has no way to synthetize
+the answer. To solve this kind of situations, matita provides a mechanism to hint
+the system the expected solution. A unification hint is a kind of rule, whose rhd
+is the unification problem, containing some metavariables X1, ..., Xn, and whose
+left hand side is the solution suggested to the system, in the form of equations
+Xi=Mi. The hint is accepted by the system if and only the solution is correct, that
+is, if it is a unifier for the given problem.
+To make an example, in the previous case, the unification problem is bool = carr X,
+and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
+bool is convertible with (carr (mk_DeqSet bool beb true)). *)
+
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ;
+ 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
+(* ---------------------------------------- *) ⊢
+ \ 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.
+
+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;
+ 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
+(* ---------------------------------------- *) ⊢
+ \ 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.
+
+(* After having provided the previous hints, we may rewrite example exhint
+declaring b of type bool. *)