Sectionin

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

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index b56caaa662df48597fa486de75f507ab324b7d5a..32a3f23eaa596d83d75f801a7df4047678cea905 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -44,14 +44,16 @@ 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,
+(* \ 5h2 class="section"\ 6Set Quality\ 5/h2\ 6
+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 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym↔] (in [term])"\ 6\ 5/span\ 6 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: *)
 
@@ -147,7 +149,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: *)
@@ -164,7 +168,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". *)
 
@@ -221,7 +227,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 
+(* 
+\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
+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 *)