commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index d2dc7c84338e11e6490b4e9a6b25bb87e351f7c4..9a7e24e0875776b22cacc5b7ab7229b5fb9d5ee2 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -235,20 +235,46 @@ qed.
 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.
 
 (* 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. *)
+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). *)
 
-(* unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 ; 
+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.
+#b #H @(\P H) 
+qed.
+
+(* The point is that == expects in input a pair of objects object 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 ≔ b1,b2:bool; 
-    X ≟ mk_DeqSet bool beqb beqb_true
+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
 (* ---------------------------------------- *) ⊢ 
-    beqb b1 b2 ≡ eqb X b1 b2. *)
+    \ 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.
     
-example exhint: ∀b:bool. (b == false) = true → b = false. 
-#b #H @(\P H).
+(* After having provided the previous hints, we may rewrite example exhint delcaring
+b of type bool. *)
+ 
+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. 
+#b #H @(\P H)
 qed.
 
 (* pairs *)