matita/matita/lib/tutorial/chapter6.ma

   1 (*
   2 Formal Languages
   3
   4 In this chapter we shall apply our notion of DeqSet, and the list operations
   5 defined in Chapter 4 to formal languages. A formal language is an arbitrary set
   6 of words over a given alphabet, that we shall represent as a predicate over words.
   7 *)
   8 include "tutorial/chapter5.ma".
   9
  10 (* A word (or string) over an alphabet S is just a list of elements of S.*)
  11 definition word ≝ λS:DeqSet.list S.
  12
  13 (* For any alphabet there is only one word of length 0, the empty word, which is
  14 denoted by ϵ .*)
  15
  16 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
  17 interpretation "epsilon" 'epsilon = (nil ?).
  18
  19 (* The operation that consists in appending two words to form a new word, whose
  20 length is the sum of the lengths of the original words is called concatenation.
  21 String concatenation is just the append operation over lists, hence there is no
  22 point to define it. Similarly, many of its properties, such as the fact that
  23 concatenating a word with the empty word gives the original word, follow by
  24 general results over lists.
  25 *)
  26
  27 (*
  28 Operations over languages
  29
  30 Languages inherit all the basic operations for sets, namely union, intersection,
  31 complementation, substraction, and so on. In addition, we may define some new
  32 operations induced by string concatenation, and in particular the concatenation
  33 A · B of two languages A and B, the so called Kleene's star A* of A and the
  34 derivative of a language A w.r.t. a given character a. *)
  35
  36 definition cat : ∀S,l1,l2,w.Prop ≝
  37   λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
  38 (*
  39 notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
  40 *)
  41 interpretation "cat lang" 'middot a b = (cat ? a b).
  42
  43
  44 (* Given a language l, the Kleene's star of l, denoted by l*, is the set of
  45 finite-length strings that can be generated by concatenating arbitrary strings of
  46 l. In other words, w belongs to l* is and only if there exists a list of strings
  47 w1,w2,...wk all belonging to l, such that l = w1w2...wk.
  48 We need to define the latter operations. The following flatten function takes in
  49 input a list of words and concatenates them together. *)
  50
  51 (* FG: flatten in list.ma gets in the way:
  52 alias id "flatten" = "cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)".
  53 does not work, so we use flatten in lists for now
  54
  55 let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
  56 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
  57 *)
  58
  59 (* Given a list of words l and a language r, (conjunct l r) is true if and only if
  60 all words in l are in r, that is for every w in l, r w holds. *)
  61
  62 let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
  63 match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ].
  64
  65 (* We are ready to give the formal definition of the Kleene's star of l:
  66 a word w belongs to l* is and only if there exists a list of strings
  67 lw such that (conjunct lw l) and  l = flatten lw. *)
  68
  69
  70 definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
  71 notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
  72 interpretation "star lang" 'star l = (star ? l).
  73
  74 (* The derivative of a language A with respect to a character a is the set of
  75 all strings w such that aw is in A. *)
  76
  77 definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
  78
  79 (*
  80 Language equalities
  81
  82 Equality between languages is just the usual extensional equality between
  83 sets. The operation of concatenation behaves well with respect to this equality. *)
  84
  85 lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop.
  86   A =1 C  → A · B =1 C · B.
  87 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
  88 cases (H w1) /6/
  89 qed.
  90
  91 lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
  92   B =1 C → A · B =1 A · C.
  93 #S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
  94 cases (H w2) /6/
  95 qed.
  96
  97 (* Concatenating a language with the empty language results in the
  98 empty language. *)
  99 lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
 100 #S #A #w % [|*] * #w1 * #w2 * * #_ *
 101 qed.
 102
 103 (* Concatenating a language l with the singleton language containing the
 104 empty string, results in the language l; that is {ϵ} is a left and right
 105 unit with respect to concatenation. *)
 106
 107 lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
 108   A · {ϵ} =1  A.
 109 #S #A #w %
 110   [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
 111   |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
 112   ]
 113 qed.
 114
 115 lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
 116   {ϵ} · A =1  A.
 117 #S #A #w %
 118   [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
 119   |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
 120   ]
 121   qed.
 122
 123 (* Concatenation is distributive w.r.t. union. *)
 124
 125 lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
 126   (A ∪ B) · C =1  A · C ∪ B · C.
 127 #S #A #B #C #w %
 128   [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
 129 qed.
 130
 131 lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
 132   (A ∪ {ϵ}) · C =1  A · C ∪ C.
 133   #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
 134 qed.
 135
 136 (* The following is a major property of derivatives *)
 137
 138 lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ → deriv S (A·B) a =1 (deriv S A a) · B.
 139 #S #A #B #a #noteps #w normalize %
 140   [* #w1 cases w1
 141     [* #w2 * * #_ #Aeps @False_ind /2/
 142     |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
 143      #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % //
 144     ]
 145   |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1))
 146    @(ex_intro … w2) % // % normalize //
 147   ]
 148 qed.
 149
 150 (*
 151 Main Properties of Kleene's star
 152
 153 We conclude this section with some important properties of Kleene's
 154 star that will be used in the following chapters. *)
 155
 156 lemma espilon_in_star: ∀S.∀A:word S → Prop.
 157   A^* ϵ.
 158 #S #A @(ex_intro … [ ]) normalize /2/
 159 qed.
 160
 161 lemma cat_to_star:∀S.∀A:word S → Prop.
 162   ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
 163 #S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l))
 164 % destruct // normalize /2/
 165 qed.
 166
 167 lemma fix_star: ∀S.∀A:word S → Prop.
 168   A^* =1 A · A^* ∪ {ϵ}.
 169 #S #A #w %
 170   [* #l generalize in match w; -w cases l [normalize #w * /2/]
 171    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
 172    #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
 173    % destruct /2/ whd @(ex_intro … tl) /2/
 174   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
 175    * #w1 * #w2 * * #eqw <eqw @cat_to_star
 176   ]
 177 qed.
 178
 179 lemma star_fix_eps : ∀S.∀A:word S → Prop.
 180   A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.
 181 #S #A #w %
 182   [* #l elim l
 183     [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
 184     |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
 185        |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1
 186         @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
 187          [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
 188        ]
 189     ]
 190   |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
 191      | whd in ⊢ (%→?); #H <H //
 192      ]
 193   ]
 194 qed.
 195
 196 lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
 197   A^* ∪ {ϵ} =1 A^*.
 198 #S #A #w % /2/ * //
 199 qed.
 200