X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=ff607176483a4ee9159c5264ef7a216393925bcd;hb=c6b408de46049021e42ebabd3ce382de1257c620;hp=e0d122934ef7e49d740beaf498c0ccef2e9f3d9d;hpb=e88e55208a612a21e25344df089a77536057bde1;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index e0d122934..ff6071764 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,14 +1,13 @@
 (* 
 h1 class="section"Naif Set Theory/h1
 *)
-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".
-
-(* For instance the empty set is defined by the always false function: *)
+(* 
+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. 
+For instance the empty set is defined by the always false function: *)
 
 definition empty_set ≝ λA:Type[0].λa:A.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
@@ -45,14 +44,17 @@ sets *)
 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
 interpretation "subset" 'subseteq a b = (subset ? a b).
 
-(* Two sets are equals if and only if they have the same elements, that is,
+(* 
+h2 class="section"Set Equality/h2
+Two sets are equals if and only if they have the same elements, that is,
 if the two characteristic functions are extensionally equivalent: *) 
 
 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a a title="iff" href="cic:/fakeuri.def(1)"↔/aspan class="error" title="Parse error: [term] expected after [sym↔] (in [term])"/span Q a.
 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
-(* This notion of equality is different from the intensional equality of
+(*
+This notion of equality is different from the intensional equality of
 functions; the fact it defines an equivalence relation must be explicitly 
 proved: *)
 
@@ -91,7 +93,9 @@ lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
   B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="substraction" href="cic:/fakeuri.def(1)"-/a C.
 #U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/iff_not.def(4)"iff_not/a/span/span/ qed.
 
-(* We can now prove several properties of the previous set-theoretic operations. 
+(* 
+h2 class="section"Simple properties of sets/h2
+We can now prove several properties of the previous set-theoretic operations. 
 In particular, union is commutative and associative, and the empty set is an 
 identity element: *)
 
@@ -148,7 +152,9 @@ lemma substract_def:∀U.∀A,B:U→Prop. Aa title="substraction" href="cic:/fa
 #U #A #B #w normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
-(* In several situation it is important to assume to have a decidable equality 
+(* 
+h2 class="section"Bool vs. Prop/h2
+In several situation it is important to assume to have a decidable equality 
 between elements of a set U, namely a boolean function eqb: U→U→bool such that
 for any pair of elements a and b in U, (eqb x y) is true if and only if x=y. 
 A set equipped with such an equality is called a DeqSet: *)
@@ -165,7 +171,9 @@ boolean, while a=b is a proposition. *)
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 interpretation "eqb" 'eqb a b = (eqb ? a b).
 
-(* It is convenient to have a simple way to reflect a proof of the fact 
+(* 
+h2 class="section"Small Scale Reflection/h2
+It is convenient to have a simple way to reflect a proof of the fact 
 that (eqb a b) is true into a proof of the proposition (a = b); to this aim, 
 we introduce two operators "\P" and "\b". *)
 
@@ -222,7 +230,9 @@ DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
   [%1 @(\P H) | %2 @(\Pf H)]
 qed.
 
-(* A simple example of a set with a decidable equality is bool. We first define 
+(* 
+h2 class="section"Unification Hints/h2
+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 *)