-include "tutorial/chapter5.ma".
-
-(* In this chapter we shall apply our notion of DeqSet, and the list operations
+(*
+\ 5h1 class="section"\ 6Formal Languages\ 5/h1\ 6
+In this chapter we shall apply our notion of DeqSet, and the list operations
defined in Chapter 4 to formal languages. A formal language is an arbitrary set
of words over a given alphabet, that we shall represent as a predicate over words.
-A word (or string) over an alphabet S is just a list of elements of S. *)
+*)
+include "tutorial/chapter5.ma".
-definition word ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S.
+(* A word (or string) over an alphabet S is just a list of elements of S.*)
+definition word ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5/span\ 6 S.
(* For any alphabet there is only one word of length 0, the \ 5i\ 6empty word\ 5/i\ 6, which is
denoted by ϵ .*)
point to define it. Similarly, many of its properties, such as the fact that
concatenating a word with the empty word gives the original word, follow by
general results over lists.
+*)
+(*
+\ 5h2 class="section"\ 6Operations over languages\ 5/h2\ 6
Languages inherit all the basic operations for sets, namely union, intersection,
complementation, substraction, and so on. In addition, we may define some new
operations induced by string concatenation, and in particular the concatenation
derivative of a language A w.r.t. a given character a. *)
definition cat : ∀S,l1,l2,w.Prop ≝
- λS.λl1,l2.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6w1,w2.w1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 w2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l1 w1 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 w2.
+ λS.λl1,l2.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6\ 5span class="error" title="Parse error: [sym_] or [ident] expected after [sym∃] (in [term])"\ 6\ 5/span\ 6w1,w2.w1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 w2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l1 w1 \ 5a title="logical and" 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 l2 w2.
notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
interpretation "cat lang" 'middot a b = (cat ? a b).
-(* Given a list of words, the flatten operation concatenates them all. *)
+
+(* Given a language l, the Kleene's star of l, denoted by l*, is the set of
+finite-length strings that can be generated by concatenating arbitrary strings of
+l. In other words, w belongs to l* is and only if there exists a list of strings
+w1,w2,...wk all belonging to l, such that l = w1w2...wk.
+We need to define the latter operations. The following flatten function takes in
+input a list of words and concatenates them together. *)
let rec flatten (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) on l : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S ≝
match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] | cons w tl ⇒ w \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 flatten ? tl ].
(* Given a list of words l and a language r, (conjunct l r) is true if and only if
all words in l are in r, that is for every w in l, r w holds. *)
-let rec conjunct (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) (r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop) on l: Prop ≝
+let rec conjunct (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6 (\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S)) (r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop) on l: Prop ≝
match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons w tl ⇒ r w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 conjunct ? tl r ].
-(* Given a language l, the kleene's star of l, denoted by l*, is the set of
-finite-length strings that can be generated by concatenating arbitrary strings of
-l. In other words, w belongs to l* is and only if there exists a list of strings
-lw all belonging to l, such that l = flatten lw. *)
+(* We are ready to give the formal definition of the Kleene's star of l:
+a word w belongs to l* is and only if there exists a list of strings
+lw such that (conjunct lw l) and l = flatten lw. *)
definition star ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw.\ 5a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l.
notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
interpretation "star lang" 'star l = (star ? l).
-(* Equality between languages is just the usual extensional equality between
+(* The derivative of a language A with respect to a character a is the set of
+all strings w such that aw is in A. *)
+
+definition deriv ≝ λS.λA:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.λa,w. A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
+
+(*
+\ 5h2 class="section"\ 6Language equalities\ 5/h2\ 6
+Equality between languages is just the usual extensional equality between
sets. The operation of concatenation behaves well with respect to this equality. *)
lemma cat_ext_l: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w1) /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+cases (H w1) /\ 5span class="autotactic"\ 66\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
lemma cat_ext_r: ∀S.∀A,B,C:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S →Prop.
#S #A #C @\ 5a href="cic:/matita/tutorial/chapter4/eqP_trans.def(3)"\ 6eqP_trans\ 5/a\ 6 [|@\ 5a href="cic:/matita/tutorial/chapter6/distr_cat_r.def(5)"\ 6distr_cat_r\ 5/a\ 6 |@\ 5a href="cic:/matita/tutorial/chapter4/eqP_union_l.def(3)"\ 6eqP_union_l\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter6/epsilon_cat_l.def(5)"\ 6epsilon_cat_l\ 5/a\ 6]
qed.
-(* The derivative of a language A with respect to a character a is the set of
-all strings w such that aw is in A. *)
-
-definition deriv ≝ λS.λA:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.λa,w. A (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
+(* The following is a major property of derivatives *)
lemma deriv_middot: ∀S,A,B,a. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S (A\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6B) a \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 (\ 5a href="cic:/matita/tutorial/chapter6/deriv.def(4)"\ 6deriv\ 5/a\ 6 S A a) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 B.
#S #A #B #a #noteps #w normalize %
]
qed.
-(* We conclude this section with some important properties of Kleene's
-star that will be usde in the following chapters. *)
+(*
+\ 5h2 class="section"\ 6Main Properties of Kleene's star\ 5/h2\ 6
+We conclude this section with some important properties of Kleene's
+star that will be used in the following chapters. *)
lemma espilon_in_star: ∀S.∀A:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
A\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6.
projects / helm.git / blobdiff