From: matitaweb Date: Tue, 28 Feb 2012 13:17:46 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1931 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b12c549230b2232b31e443942c20be615455b0ad commit by user andrea --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 9a7e24e08..2c98ad147 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -1,5 +1,6 @@ -(* In this Chapter we shall develop a naif theory of sets represented as characteristic -predicates over some universe codeA/code, that is as objects of type A→Prop. *) +(* In this Chapter we shall develop a naif theory of sets represented as +characteristic predicates over some universe codeA/code, that is as objects of type +A→Prop. *) include "basics/types.ma". include "basics/bool.ma". @@ -244,18 +245,18 @@ example exhint: ∀b:a href="cic:/matita/tutorial/chapter4/DeqBool.def(5)"DeqB #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. +(* 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)). *) @@ -270,8 +271,8 @@ unification hint 0 a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"≔/a (* ---------------------------------------- *) ⊢ 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. -(* After having provided the previous hints, we may rewrite example exhint delcaring -b of type bool. *) +(* After having provided the previous hints, we may rewrite example exhint +declaring 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)