more sections

[helm.git] / weblib / tutorial / chapter4.ma

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index e0d122934ef7e49d740beaf498c0ccef2e9f3d9d..20762a99a25975239a42be90d10572eb063c24a1 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,14 +1,13 @@
 (* 
 \ 5h1 class="section"\ 6Naif Set Theory\ 5/h1\ 6
 *)
-In this Chapter we shall develop a naif theory of sets represented as 
-characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, 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 \ 5code\ 6A\ 5/code\ 6, 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.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
@@ -148,7 +147,9 @@ lemma substract_def:∀U.∀A,B:U→Prop. A\ 5a title="substraction" href="cic:/fa
 #U #A #B #w 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.
 
-(* In several situation it is important to assume to have a decidable equality 
+(* 
+\ 5h2 class="section"\ 6Bool vs. Prop\ 5/h2\ 6
+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 +166,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 
+(* 
+\ 5h2 class="section"\ 6Small Scale Reflection\ 5/h2\ 6
+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". *)
 
@@ -238,7 +241,9 @@ 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
+(* 
+\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 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