X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter7.ma;h=b9a35a8ad93214da1f607dec2f9c2d1f9623bb0d;hb=c65aeeb22bdc7bf289e5db108c358b199773c857;hp=da90566e88cb4e1754096fbcf189d51fe15dd5cc;hpb=55be7edb5a8249fa65746a47ea1b702881cbc979;p=helm.git
diff --git a/weblib/tutorial/chapter7.ma b/weblib/tutorial/chapter7.ma
index da90566e8..b9a35a8ad 100644
--- a/weblib/tutorial/chapter7.ma
+++ b/weblib/tutorial/chapter7.ma
@@ -1,4 +1,5 @@
-(* We shall apply all the previous machinery to the study of regular languages
+(*
Regular Expressions
+We shall apply all the previous machinery to the study of regular languages
and the constructions of the associated finite automata. *)
include "tutorial/chapter6.ma".
@@ -46,7 +47,8 @@ lemma rsem_star : âS.âr: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1
// qed.
-(* We now introduce pointed regular expressions, that are the main tool we shall
+(* Pointed Regular expressions
+We now introduce pointed regular expressions, that are the main tool we shall
use for the construction of the automaton.
A pointed regular expression is just a regular expression internally labelled
with some additional points. Intuitively, points mark the positions inside the
@@ -128,7 +130,8 @@ lemma erase_plus : âS.âi1,i2:pitem S.
lemma erase_star : âS.âi:pitem S.|i^*| = |i|^*.
// qed.
-(* Items and pres are very concrete datatypes: they can be effectively compared,
+(* Comparing items and pres
+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. *)
@@ -195,7 +198,8 @@ unification hint 0 â S,i1,i2;
(* ---------------------------------------- *) â¢
beqitem S i1 i2 â¡ eqb X i1 i2.
-(* The intuitive semantic of a point is to mark the position where
+(* Semantics of pointed regular expression
+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. *)
@@ -295,295 +299,3 @@ lemma minus_eps_pre: âS.âe:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
]
qed.
-definition lo â λS:DeqSet.λa,b:pre S.â©\fst a + \fst b,\snd a ⨠\snd bâª.
-notation "a â b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
-
-lemma lo_def: âS.âi1,i2:pitem S.âb1,b2. â©i1,b1âªââ©i2,b2âª=â©i1+i2,b1â¨b2âª.
-// qed.
-
-definition pre_concat_r â λS:DeqSet.λi:pitem S.λe:pre S.
- match e with [ mk_Prod i1 b â â©i · i1, bâª].
-
-notation "i â e" left associative with precedence 60 for @{'lhd $i $e}.
-interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
-
-lemma eq_to_ex_eq: âS.âA,B:word S â Prop.
- A = B â A =1 B.
-#S #A #B #H >H /2/ qed.
-
-lemma sem_pre_concat_r : âS,i.âe:pre S.
- \sem{i â e} =1 \sem{i} · \sem{|\fst e|} ⪠\sem{e}.
-#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
->sem_pre_true >sem_cat >sem_pre_true /2/
-qed.
-
-definition pre_concat_l â λS:DeqSet.λbcast:âS:DeqSet.pitem S â pre S.λe1:pre S.λi2:pitem S.
- match e1 with
- [ mk_Prod i1 b1 â match b1 with
- [ true â (i1 â (bcast ? i2))
- | false â â©i1 · i2,falseâª
- ]
- ].
-
-notation "a â¹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
-interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
-
-notation "â¢" non associative with precedence 60 for @{eclose ?}.
-
-let rec eclose (S: DeqSet) (i: pitem S) on i : pre S â
- match i with
- [ pz â â© `â
, false âª
- | pe â ⩠ϵ, true âª
- | ps x â â© `.x, falseâª
- | pp x â â© `.x, false âª
- | po i1 i2 â â¢i1 â â¢i2
- | pc i1 i2 â â¢i1 â¹ i2
- | pk i â â©(\fst (â¢i))^*,trueâª].
-
-notation "⢠x" non associative with precedence 60 for @{'eclose $x}.
-interpretation "eclose" 'eclose x = (eclose ? x).
-
-lemma eclose_plus: âS:DeqSet.âi1,i2:pitem S.
- â¢(i1 + i2) = â¢i1 â â¢i2.
-// qed.
-
-lemma eclose_dot: âS:DeqSet.âi1,i2:pitem S.
- â¢(i1 · i2) = â¢i1 â¹ i2.
-// qed.
-
-lemma eclose_star: âS:DeqSet.âi:pitem S.
- â¢i^* = â©(\fst(â¢i))^*,trueâª.
-// qed.
-
-definition lift â λS.λf:pitem S âpre S.λe:pre S.
- match e with
- [ mk_Prod i b â â©\fst (f i), \snd (f i) ⨠bâª].
-
-definition preclose â λS. lift S (eclose S).
-interpretation "preclose" 'eclose x = (preclose ? x).
-
-(* theorem 16: 2 *)
-lemma sem_oplus: âS:DeqSet.âe1,e2:pre S.
- \sem{e1 â e2} =1 \sem{e1} ⪠\sem{e2}.
-#S * #i1 #b1 * #i2 #b2 #w %
- [cases b1 cases b2 normalize /2/ * /3/ * /3/
- |cases b1 cases b2 normalize /2/ * /3/ * /3/
- ]
-qed.
-
-lemma odot_true :
- âS.âi1,i2:pitem S.
- â©i1,true⪠⹠i2 = i1 â (â¢i2).
-// qed.
-
-lemma odot_true_bis :
- âS.âi1,i2:pitem S.
- â©i1,true⪠⹠i2 = â©i1 · \fst (â¢i2), \snd (â¢i2)âª.
-#S #i1 #i2 normalize cases (â¢i2) // qed.
-
-lemma odot_false:
- âS.âi1,i2:pitem S.
- â©i1,false⪠⹠i2 = â©i1 · i2, falseâª.
-// qed.
-
-lemma LcatE : âS.âe1,e2:pitem S.
- \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ⪠\sem{e2}.
-// qed.
-
-lemma erase_bull : âS.âi:pitem S. |\fst (â¢i)| = |i|.
-#S #i elim i //
- [ #i1 #i2 #IH1 #IH2 >erase_dot eclose_dot
- cases (â¢i1) #i11 #b1 cases b1 // odot_true_bis //
- | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus ⦠i1) eclose_star >(erase_star ⦠i) odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
- |#H >odot_true >sem_pre_true @(eqP_trans ⦠(sem_pre_concat_r â¦))
- >erase_bull @eqP_trans [|@(eqP_union_l ⦠H)]
- @eqP_trans [|@eqP_union_l[|@union_comm ]]
- @eqP_trans [|@eqP_sym @union_assoc ] /3/
- ]
-qed.
-
-lemma minus_eps_pre_aux: âS.âe:pre S.âi:pitem S.âA.
- \sem{e} =1 \sem{i} ⪠A â \sem{\fst e} =1 \sem{i} ⪠(A - {[ ]}).
-#S #e #i #A #seme
-@eqP_trans [|@minus_eps_pre]
-@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
-@eqP_trans [||@distribute_substract]
-@eqP_substract_r //
-qed.
-
-(* theorem 16: 1 *)
-theorem sem_bull: âS:DeqSet. âi:pitem S. \sem{â¢i} =1 \sem{i} ⪠\sem{|i|}.
-#S #e elim e
- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l ⦠IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l ⦠IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
- ]
-qed.
-
-(* blank item *)
-let rec blank (S: DeqSet) (i: re S) on i :pitem S â
- match i with
- [ z â `â
- | e â ϵ
- | s y â `y
- | o e1 e2 â (blank S e1) + (blank S e2)
- | c e1 e2 â (blank S e1) · (blank S e2)
- | k e â (blank S e)^* ].
-
-lemma forget_blank: âS.âe:re S.|blank S e| = e.
-#S #e elim e normalize //
-qed.
-
-lemma sem_blank: âS.âe:re S.\sem{blank S e} =1 â
.
-#S #e elim e
- [1,2:@eq_to_ex_eq //
- |#s @eq_to_ex_eq //
- |#e1 #e2 #Hind1 #Hind2 >sem_cat
- @eqP_trans [||@(union_empty_r ⦠â
)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
- @eqP_trans [||@(cat_empty_l ⦠?)] @cat_ext_l @Hind1
- |#e1 #e2 #Hind1 #Hind2 >sem_plus
- @eqP_trans [||@(union_empty_r ⦠â
)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
- |#e #Hind >sem_star
- @eqP_trans [||@(cat_empty_l ⦠?)] @cat_ext_l @Hind
- ]
-qed.
-
-theorem re_embedding: âS.âe:re S.
- \sem{â¢(blank S e)} =1 \sem{e}.
-#S #e @eqP_trans [|@sem_bull] >forget_blank
-@eqP_trans [|@eqP_union_r [|@sem_blank]]
-@eqP_trans [|@union_comm] @union_empty_r.
-qed.
-
-(* lefted operations *)
-definition lifted_cat â λS:DeqSet.λe:pre S.
- lift S (pre_concat_l S eclose e).
-
-notation "e1 â e2" left associative with precedence 70 for @{'odot $e1 $e2}.
-
-interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
-
-lemma odot_true_b : âS.âi1,i2:pitem S.âb.
- â©i1,true⪠â â©i2,b⪠= â©i1 · (\fst (â¢i2)),\snd (â¢i2) ⨠bâª.
-#S #i1 #i2 #b normalize in ⢠(??%?); cases (â¢i2) //
-qed.
-
-lemma odot_false_b : âS.âi1,i2:pitem S.âb.
- â©i1,false⪠â â©i2,b⪠= â©i1 · i2 ,bâª.
-//
-qed.
-
-lemma erase_odot:âS.âe1,e2:pre S.
- |\fst (e1 â e2)| = |\fst e1| · (|\fst e2|).
-#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
-qed.
-
-definition lk â λS:DeqSet.λe:pre S.
- match e with
- [ mk_Prod i1 b1 â
- match b1 with
- [true â â©(\fst (eclose ? i1))^*, trueâª
- |false â â©i1^*,falseâª
- ]
- ].
-
-(* notation < "a \sup â" non associative with precedence 90 for @{'lk $a}.*)
-interpretation "lk" 'lk a = (lk ? a).
-notation "a^â" non associative with precedence 90 for @{'lk $a}.
-
-
-lemma ostar_true: âS.âi:pitem S.
- â©i,trueâª^â = â©(\fst (â¢i))^*, trueâª.
-// qed.
-
-lemma ostar_false: âS.âi:pitem S.
- â©i,falseâª^â = â©i^*, falseâª.
-// qed.
-
-lemma erase_ostar: âS.âe:pre S.
- |\fst (e^â)| = |\fst e|^*.
-#S * #i * // qed.
-
-lemma sem_odot_true: âS:DeqSet.âe1:pre S.âi.
- \sem{e1 â â©i,trueâª} =1 \sem{e1 â¹ i} ⪠{ [ ] }.
-#S #e1 #i
-cut (e1 â â©i,true⪠= â©\fst (e1 â¹ i), \snd(e1 â¹ i) ⨠trueâª) [//]
-#H >H cases (e1 â¹ i) #i1 #b1 cases b1
- [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l /2/
- |/2/
- ]
-qed.
-
-lemma eq_odot_false: âS:DeqSet.âe1:pre S.âi.
- e1 â â©i,false⪠= e1 â¹ i.
-#S #e1 #i
-cut (e1 â â©i,false⪠= â©\fst (e1 â¹ i), \snd(e1 â¹ i) ⨠falseâª) [//]
-cases (e1 â¹ i) #i1 #b1 cases b1 #H @H
-qed.
-
-lemma sem_odot:
- âS.âe1,e2: pre S. \sem{e1 â e2} =1 \sem{e1}· \sem{|\fst e2|} ⪠\sem{e2}.
-#S #e1 * #i2 *
- [>sem_pre_true
- @eqP_trans [|@sem_odot_true]
- @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
- |>sem_pre_false >eq_odot_false @odot_dot_aux //
- ]
-qed.
-
-(* theorem 16: 4 *)
-theorem sem_ostar: âS.âe:pre S.
- \sem{e^â} =1 \sem{e} · \sem{|\fst e|}^*.
-#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
- @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
- |>sem_pre_false >sem_pre_false >sem_star /2/
- ]
-qed.
\ No newline at end of file