From: matitaweb Date: Thu, 1 Mar 2012 16:38:03 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1923 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01feaa4859598983ee07f43760811ff73eea001b;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma index cadc0065c..21e6e75aa 100644 --- a/weblib/tutorial/chapter6.ma +++ b/weblib/tutorial/chapter6.ma @@ -1,129 +1,173 @@ include "tutorial/chapter5.ma". -definition word ≝ λS:DeqSet.list S. +(* 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. *) + +definition word ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S. + +(* For any alphabet there is only one word of length 0, the iempty word/i, which is +denoted by ϵ .*) notation "ϵ" non associative with precedence 90 for @{ 'epsilon }. interpretation "epsilon" 'epsilon = (nil ?). -(* concatenation *) +(* The operation that consists in appending two words to form a new word, whose +length is the sum of the lengths of the original words is called concatenation. +String concatenation is just the append operation over lists, hence there is no +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. + +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 +A · B of two languages A and B, the so called Kleene's star A* of A and the +derivative of a language A w.r.t. a given character a. *) + definition cat : ∀S,l1,l2,w.Prop ≝ - λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2. + λS.λl1,l2.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/aw1,w2.w1 a title="append" href="cic:/fakeuri.def(1)"@/a w2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 w1 a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 w2. + notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}. interpretation "cat lang" 'middot a b = (cat ? a b). -let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ -match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. +(* Given a list of words, the flatten operation concatenates them all. *) -let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝ -match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. +let rec flatten (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) on l : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S ≝ +match l with [ nil ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a ] | cons w tl ⇒ w a title="append" href="cic:/fakeuri.def(1)"@/a flatten ? tl ]. -(* kleene's star *) -definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. +(* 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 : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (l : a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a (a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S)) (r : a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S → Prop) on l: Prop ≝ +match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons w tl ⇒ r w a title="logical and" href="cic:/fakeuri.def(1)"∧/a 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. *) + +definition star ≝ λS.λl.λw:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/alw.a href="cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)"flatten/a ? lw a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter6/conjunct.fix(0,1,4)"conjunct/a ? lw l. notation "a ^ *" non associative with precedence 90 for @{ 'star $a}. interpretation "star lang" 'star l = (star ? l). -lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop. - A =1 C → A · B =1 C · B. +(* 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:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. + A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="cat lang" href="cic:/fakeuri.def(1)"·/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="cat lang" href="cic:/fakeuri.def(1)"·/a B. #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2 -cases (H w1) /6/ +cases (H w1) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. -lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop. - B =1 C → A · B =1 A · C. +lemma cat_ext_r: ∀S.∀A,B,C:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. + B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="cat lang" href="cic:/fakeuri.def(1)"·/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="cat lang" href="cic:/fakeuri.def(1)"·/a C. #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2 -cases (H w2) /6/ +cases (H w2) /span class="autotactic"6span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. -lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅. +(* Concatenating a language with the empty language results in the +empty language. *) +lemma cat_empty_l: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S→Prop. a title="empty set" href="cic:/fakeuri.def(1)"∅/a a title="cat lang" href="cic:/fakeuri.def(1)"·/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="empty set" href="cic:/fakeuri.def(1)"∅/a. #S #A #w % [|*] * #w1 * #w2 * * #_ * qed. -lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop. - (A ∪ B) · C =1 A · C ∪ B · C. +(* Concatenating a language l with the singleton language containing the +empty string, results in the language l; that is {ϵ} is a left and right +unit with respect to concatenation. *) + +lemma epsilon_cat_r: ∀S.∀A:a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S →Prop. + A a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="singleton" href="cic:/fakeuri.def(1)"{/aa title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A. +#S #A #w % + [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2