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

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 55e734d56..ff6071764 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,11 +1,13 @@
-(* 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. *)
-
+(* 
+h1 class="section"Naif Set Theory/h1
+*)
 include "basics/types.ma".
 include "basics/bool.ma".
-
-(**** For instance the empty set is defined by the always function predicate *)
+(* 
+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}.
@@ -14,7 +16,7 @@ interpretation "empty set" 'empty_set = (empty_set ?).
 (* Similarly, a singleton set contaning containing an element a, is defined
 by by the characteristic function asserting equality with a *)
 
-definition singleton ≝ λA.λx,a:A.xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa.
+definition singleton ≝ λA.λx,a:A.xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/spana.
 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
 interpretation "singleton" 'singl x = (singleton ? x).
 
@@ -27,7 +29,7 @@ conjunction and negation *)
 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a a title="logical or" href="cic:/fakeuri.def(1)"∨/a Q a.
 interpretation "union" 'union a b = (union ? a b).
 
-definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a a title="logical and" href="cic:/fakeuri.def(1)"∧/a Q a.
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a a title="logical and" href="cic:/fakeuri.def(1)"∧/aspan class="error" title="Parse error: [term] expected after [sym∧] (in [term])"/span Q a.
 interpretation "intersection" 'intersects a b = (intersection ? a b).
 
 definition complement ≝ λU:Type[0].λA:U → Prop.λw.a title="logical not" href="cic:/fakeuri.def(1)"¬/a A w.
@@ -42,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)"↔/a Q a.
+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: *)
 
@@ -65,7 +70,7 @@ lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
 with respect to eqP: *)
 
 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
-  A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="union" href="cic:/fakeuri.def(1)"∪/a B.
+  A a title="extensional equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: NUMBER '1' or [term] expected after [sym=] (in [term])"/span1 C  → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="union" href="cic:/fakeuri.def(1)"∪/a B.
 #U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_or_r.def(2)"iff_or_r/a @eqAB qed.
   
 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
@@ -77,7 +82,7 @@ lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
 #U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_and_r.def(2)"iff_and_r/a @eqAB qed.
   
 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
-  B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C.
+  B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="intersection" href="cic:/fakeuri.def(1)"∩/aspan class="error" title="Parse error: [term] expected after [sym∩] (in [term])"/span B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" 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 @eqBC qed.
 
 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
@@ -88,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: *)
 
@@ -103,7 +110,7 @@ lemma union_comm : ∀U.∀A,B:U →Prop.
 
 lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
   A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="union" href="cic:/fakeuri.def(1)"∪/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="union" href="cic:/fakeuri.def(1)"∪/a C).
-#S #A #B #C #w % [* [* /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] | * [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/]
+#S #A #B #C #w % [* [* /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ ] | * [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/]
 qed.   
 
 (* In the same way we prove commutativity and associativity for set 
@@ -145,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: *)
@@ -162,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". *)
 
@@ -219,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 *)