From: matitaweb Date: Tue, 28 Feb 2012 13:11:17 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1932 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38e1e666b4f053b5e2e0add2c5e45a1914e27978;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index d2dc7c843..9a7e24e08 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -235,20 +235,46 @@ qed. definition DeqBool ≝ a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"beqb_true/a. (* 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 a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"≔/a ; +example exhint: ∀b:a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"DeqBool/a. (ba title="eqb" href="cic:/fakeuri.def(1)"=/a=a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → ba title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#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 a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"≔/a ; X ≟ a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"beqb_true/a (* ---------------------------------------- *) ⊢ a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≡ a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"carr/a X. -unification hint 0 ≔ b1,b2:bool; - X ≟ mk_DeqSet bool beqb beqb_true +unification hint 0 a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"≔/a b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a; + X ≟ a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"beqb_true/a (* ---------------------------------------- *) ⊢ - beqb b1 b2 ≡ eqb X b1 b2. *) + a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a b1 b2 ≡ a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"eqb/a 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:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. (b a title="eqb" href="cic:/fakeuri.def(1)"=/a= a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#b #H @(\P H) qed. (* pairs *)