commit by user andrea

diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma
index 208db9e3fb27dd4d09c1030d62ec3cae5e3a5c1d..da90566e88cb4e1754096fbcf189d51fe15dd5cc 100644 (file)
--- a/weblib/tutorial/chapter7.ma
+++ b/weblib/tutorial/chapter7.ma
@@ -26,14 +26,14 @@ interpretation "atom" 'ps a = (s ? a).
 notation "`∅" non associative with precedence 90 for @{ 'empty }.
 interpretation "empty" 'empty = (z ?).
 
-(* The language $sem{e}$ associated with the regular expression e is inductively 
+(* The language sem{e} associated with the regular expression e is inductively 
 defined by the following function: *)
 
-let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝ 
+let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"\ 6\ 5/span\ 6 S → Prop ≝ 
 match r with
-[ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+[ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"\ 6\ 5/span\ 6
 | e ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}
-| s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x]}
+| s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5span class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"\ 6\ 5/span\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym[] (in [term])"\ 6\ 5/span\ 6x]}
 | c r1 r2 ⇒ (in_l ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (in_l ? r2)
 | o r1 r2 ⇒ (in_l ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_l ? r2)
 | k r1 ⇒ (in_l ? r1) \ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*].
@@ -128,10 +128,11 @@ lemma erase_plus : ∀S.∀i1,i2:pitem S.
 lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. 
 // qed.
 
-(* Items and pres are a very concrete datatype: they can be effectively compared, 
-and enumerated. In particular, we can define a boolean equality beqitem and 
-\vebeqitem_true+ enriching the set \verb+(pitem S)+
-to a \verb+DeqSet+. boolean equality *)
+(* Items and pres are very concrete datatypes: they can be effectively compared, 
+and enumerated. In particular, we can define a boolean equality beqitem and a proof
+beqitem_true that it refects propositional equality, enriching the set (pitem S)
+to a DeqSet. *)
+
 let rec beqitem S (i1,i2: pitem S) on i1 ≝ 
   match i1 with
   [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
@@ -179,7 +180,11 @@ qed.
 
 definition DeqItem ≝ λS.
   mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
-  
+
+(* We also add a couple of unification hints to allow the type inference system 
+to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the 
+equality function of a DeqSet. *)
+
 unification hint  0 ≔ S; 
     X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
 (* ---------------------------------------- *) ⊢ 
@@ -190,7 +195,9 @@ unification hint  0 ≔ S,i1,i2;
 (* ---------------------------------------- *) ⊢ 
     beqitem S i1 i2 ≡ eqb X i1 i2.
 
-(* semantics *)
+(* The intuitive semantic of a point is to mark the position where
+we should start reading the regular expression. The language associated
+to a pre is the union of the languages associated with its points. *)
 
 let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝ 
 match r with
@@ -211,6 +218,8 @@ definition in_prl ≝ λS : DeqSet.λp:pre S.
 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 interpretation "in_prl" 'in_l E = (in_prl ? E).
 
+(* The following, trivial lemmas are only meant for rewriting purposes. *)
+
 lemma sem_pre_true : ∀S.∀i:pitem S. 
   \sem{〈i,true〉} = \sem{i} ∪ {ϵ}. 
 // qed.
@@ -243,6 +252,14 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w.
   \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
 // qed.
 
+(* Below are a few, simple, semantic properties of items. In particular:
+- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
+- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+The first property is proved by a simple induction on $i$; the other
+results are easy corollaries. We need an auxiliary lemma first. *)
+
 lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
 #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
 
@@ -255,7 +272,6 @@ lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
   ]
 qed.
 
-(* lemma 12 *)
 lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
 #S * #i #b cases b // normalize #H @False_ind /2/ 
 qed.