weblib/tutorial/chapter7.ma

   1 (*
   2 \ 5h1\ 6Regular Expressions \ 5/h1\ 6
   3 We shall apply all the previous machinery to the study of regular languages
   4 and the constructions of the associated finite automata. *)
   5
   6 include "tutorial/chapter6.ma".
   7
   8 (* The type re of regular expressions over an alphabet $S$ is the smallest
   9 collection of objects generated by the following constructors: *)
  10
  11 inductive re (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
  12    z: re S                (* empty: ∅ *)
  13  | e: re S                (* epsilon: ϵ *)
  14  | s: S → re S            (* symbol: a *)
  15  | c: re S → re S → re S  (* concatenation: e1 · e2 *)
  16  | o: re S → re S → re S  (* plus: e1 + e2 *)
  17  | k: re S → re S.        (* kleene's star: e* *)
  18
  19 interpretation "re epsilon" 'epsilon = (e ?).
  20 interpretation "re or" 'plus a b = (o ? a b).
  21 interpretation "re cat" 'middot a b = (c ? a b).
  22 interpretation "re star" 'star a = (k ? a).
  23
  24 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
  25 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
  26 interpretation "atom" 'ps a = (s ? a).
  27
  28 notation "`∅" non associative with precedence 90 for @{ 'empty }.
  29 interpretation "empty" 'empty = (z ?).
  30
  31 (* The language sem{e} associated with the regular expression e is inductively
  32 defined by the following function: *)
  33
  34 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 ≝
  35 match r with
  36 [ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
  37 | 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}
  38 | 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 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) }
  39 | c r1 r2 ⇒ (in_l ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (in_l ? r2)
  40 | o r1 r2 ⇒ (in_l ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_l ? r2)
  41 | k r1 ⇒ (in_l ? r1) \ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*].
  42
  43 notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
  44 interpretation "in_l" 'in_l E = (in_l ? E).
  45 interpretation "in_l mem" 'mem w l = (in_l ? l w).
  46
  47 lemma rsem_star : ∀S.∀r: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S. \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
  48 // qed.
  49
  50
  51 (*
  52 \ 5h2\ 6Pointed Regular expressions \ 5/h2\ 6
  53 We now introduce pointed regular expressions, that are the main tool we shall
  54 use for the construction of the automaton.
  55 A pointed regular expression is just a regular expression internally labelled
  56 with some additional points. Intuitively, points mark the positions inside the
  57 regular expression which have been reached after reading some prefix of
  58 the input string, or better the positions where the processing of the remaining
  59 string has to be started. Each pointed expression for $e$ represents a state of
  60 the {\em deterministic} automaton associated with $e$; since we obviously have
  61 only a finite number of possible labellings, the number of states of the automaton
  62 is finite.
  63
  64 Pointed regular expressions provide the tool for an algebraic revisitation of
  65 McNaughton and Yamada's algorithm for position automata, making the proof of its
  66 correctness, that is far from trivial, particularly clear and simple. In particular,
  67 pointed expressions offer an appealing alternative to Brzozowski's derivatives,
  68 avoiding their weakest point, namely the fact of being forced to quotient derivatives
  69 w.r.t. a suitable notion of equivalence in order to get a finite number of states
  70 (that is not essential for recognizing strings, but is crucial for comparing regular
  71 expressions).
  72
  73 Our main data structure is the notion of pointed item, that is meant whose purpose
  74 is to encode a set of positions inside a regular expression.
  75 The idea of formalizing pointers inside a data type by means of a labelled version
  76 of the data type itself is probably one of the first, major lessons learned in the
  77 formalization of the metatheory of programming languages. For our purposes, it is
  78 enough to mark positions preceding individual characters, so we shall have two kinds
  79 of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
  80
  81 inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
  82    pz: pitem S                       (* empty *)
  83  | pe: pitem S                       (* epsilon *)
  84  | ps: S → pitem S                   (* symbol *)
  85  | pp: S → pitem S                   (* pointed sysmbol *)
  86  | pc: pitem S → pitem S → pitem S   (* concatenation *)
  87  | po: pitem S → pitem S → pitem S   (* plus *)
  88  | pk: pitem S → pitem S.            (* kleene's star *)
  89
  90 (* A pointed regular expression (pre) is just a pointed item with an additional
  91 boolean, that must be understood as the possibility to have a trailing point at
  92 the end of the expression. As we shall see, pointed regular expressions can be
  93 understood as states of a DFA, and the boolean indicates if
  94 the state is final or not. *)
  95
  96 definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
  97
  98 interpretation "pitem star" 'star a = (pk ? a).
  99 interpretation "pitem or" 'plus a b = (po ? a b).
 100 interpretation "pitem cat" 'middot a b = (pc ? a b).
 101 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
 102 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
 103 interpretation "pitem pp" 'pp a = (pp ? a).
 104 interpretation "pitem ps" 'ps a = (ps ? a).
 105 interpretation "pitem epsilon" 'epsilon = (pe ?).
 106 interpretation "pitem empty" 'empty = (pz ?).
 107
 108 (* The carrier $|i|$ of an item i is the regular expression obtained from i by
 109 removing all the points. Similarly, the carrier of a pointed regular expression
 110 is the carrier of its item. *)
 111
 112 let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on l: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S ≝
 113  match l with
 114   [ pz ⇒ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,1,1)"\ 6z\ 5/a\ 6 ? (* `∅ *)
 115   | pe ⇒ \ 5a title="re epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6
 116   | ps x ⇒ \ 5a title="atom" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6x
 117   | pp x ⇒ \ 5a title="atom" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6x
 118   | pc E1 E2 ⇒ (forget ? E1) \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (forget ? E2)
 119   | po E1 E2 ⇒ (forget ? E1) \ 5a title="re or" 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 (forget ? E2)
 120   | pk E ⇒ (forget ? E)\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* ].
 121
 122 (* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
 123 interpretation "forget" 'norm a = (forget ? a).
 124
 125 lemma erase_dot : ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 e2| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,4,1)"\ 6c\ 5/a\ 6 ? (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e1|) (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e2|).
 126 // qed.
 127
 128 lemma erase_plus : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 129   \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i1| \ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|.
 130 // qed.
 131
 132 lemma erase_star : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
 133 // qed.
 134
 135 (*
 136 \ 5h2\ 6Comparing items and pres\ 5/h2\ 6
 137 Items and pres are very concrete datatypes: they can be effectively compared,
 138 and enumerated. In particular, we can define a boolean equality beqitem and a proof
 139 beqitem_true that it refects propositional equality, enriching the set (pitem S)
 140 to a DeqSet. *)
 141
 142 let rec beqitem S (i1,i2: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on i1 ≝
 143   match i1 with
 144   [ pz ⇒ match i2 with [ pz ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
 145   | pe ⇒ match i2 with [ pe ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
 146   | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=y2 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
 147   | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=y2 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
 148   | po i11 i12 ⇒ match i2 with
 149     [ po i21 i22 ⇒ beqitem S i11 i21 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 beqitem S i12 i22
 150     | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"\ 6\ 5/span\ 6]
 151   | pc i11 i12 ⇒ match i2 with
 152     [ pc i21 i22 ⇒ beqitem S i11 i21 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 beqitem S i12 i22
 153     | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
 154   | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
 155   ].
 156
 157 lemma beqitem_true: ∀S,i1,i2. \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) (i1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i2).
 158 #S #i1 elim i1
 159   [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
 160   |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
 161   |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
 162     [>(\P H) // | @(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …))]
 163   |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
 164     [>(\P H) // | @(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …))]
 165   |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
 166    normalize #H destruct
 167     [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i11 i21)) #H1
 168       [>(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind1 i21) H1) >(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind2 i22)) // >H1 in H; #H @H
 169       |>H1 in H; normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 170       ]
 171     |>(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind1 i21) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) >(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind2 i22) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
 172     ]
 173   |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
 174    normalize #H destruct
 175     [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i11 i21)) #H1
 176       [>(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind1 i21) H1) >(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind2 i22)) // >H1 in H; #H @H
 177       |>H1 in H; normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 178       ]
 179     |>(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind1 i21) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) >(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind2 i22) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
 180     ]
 181   |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
 182    normalize #H destruct
 183     [>(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind i4) H) // |>(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind i4) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //]
 184   ]
 185 qed.
 186
 187 definition DeqItem ≝ λS.
 188   \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem_true.def(5)"\ 6beqitem_true\ 5/a\ 6 S).
 189
 190 (* We also add a couple of unification hints to allow the type inference system
 191 to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
 192 equality function of a DeqSet. *)
 193
 194 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 S;
 195     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem_true.def(5)"\ 6beqitem_true\ 5/a\ 6 S)
 196 (* ---------------------------------------- *) ⊢
 197     \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
 198
 199 unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 S,i1,i2;
 200     X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem_true.def(5)"\ 6beqitem_true\ 5/a\ 6 S)
 201 (* ---------------------------------------- *) ⊢
 202     \ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X i1 i2.
 203
 204 (*
 205 \ 5h2\ 6Semantics of pointed regular expressions\ 5/h2\ 6
 206 The intuitive semantic of a point is to mark the position where
 207 we should start reading the regular expression. The language associated
 208 to a pre is the union of the languages associated with its points. *)
 209
 210 let rec in_pl (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
 211 match r with
 212 [ pz ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 213 | pe ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 214 | ps _ ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 215 | pp x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) }
 216 | pc r1 r2 ⇒ (in_pl ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r2} \ 5a title="union" 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 (in_pl ? r2)
 217 | po r1 r2 ⇒ (in_pl ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_pl ? r2)
 218 | pk r1 ⇒ (in_pl ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r1}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*  ].
 219
 220 interpretation "in_pl" 'in_l E = (in_pl ? E).
 221 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
 222
 223 definition in_prl ≝ λS : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λp:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
 224   if (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p) then \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6} else \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p}.
 225
 226 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 227 interpretation "in_prl" 'in_l E = (in_prl ? E).
 228
 229 (* The following, trivial lemmas are only meant for rewriting purposes. *)
 230
 231 lemma sem_pre_true : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 232   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}.
 233 // qed.
 234
 235 lemma sem_pre_false : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 236   \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i}.
 237 // qed.
 238
 239 lemma sem_cat: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 240   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2}.
 241 // qed.
 242
 243 lemma sem_cat_w: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w.
 244   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2} w \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 ((\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|}) w \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2} w).
 245 // qed.
 246
 247 lemma sem_plus: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 248   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2}.
 249 // qed.
 250
 251 lemma sem_plus_w: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w.
 252   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2} w \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1} w \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2} w).
 253 // qed.
 254
 255 lemma sem_star : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
 256   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
 257 // qed.
 258
 259 lemma sem_star_w : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w.
 260   \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*} w \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 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 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} w1 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* w2).
 261 // qed.
 262
 263 (* Below are a few, simple, semantic properties of items. In particular:
 264 - not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
 265 - epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
 266 - minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
 267 - minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
 268 The first property is proved by a simple induction on $i$; the other
 269 results are easy corollaries. We need an auxiliary lemma first. *)
 270
 271 lemma append_eq_nil : ∀S.∀w1,w2:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. 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 \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 → w1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6.
 272 #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
 273
 274 lemma not_epsilon_lp : ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 (\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e).
 275 #S #e elim e normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 276   [#r1 #r2 * #n1 #n2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #H
 277    >(\ 5a href="cic:/matita/tutorial/chapter7/append_eq_nil.def(4)"\ 6append_eq_nil\ 5/a\ 6 …H…) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 278   |#r1 #r2 #n1 #n2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 279   |#r #n % * #w1 * #w2 * * #H >(\ 5a href="cic:/matita/tutorial/chapter7/append_eq_nil.def(4)"\ 6append_eq_nil\ 5/a\ 6 …H…) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 280   ]
 281 qed.
 282
 283 lemma epsilon_to_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e → \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 284 #S * #i #b cases b // normalize #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 285 qed.
 286
 287 lemma true_to_epsilon : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e.
 288 #S * #i #b #btrue normalize in btrue; >btrue %2 //
 289 qed.
 290
 291 lemma minus_eps_item: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i}\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]}.
 292 #S #i #w %
 293   [#H whd % // normalize @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter7/not_epsilon_lp.def(8)"\ 6not_epsilon_lp\ 5/a\ 6 …i)) //
 294   |* //
 295   ]
 296 qed.
 297
 298 lemma minus_eps_pre: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6\ 5span class="error" title="Parse error: [sym{] expected after [sym\sem ] (in [term])"\ 6\ 5/span\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e}\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]}.
 299 #S * #i *
 300   [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 normalize in ⊢ (??%?); #w %
 301     [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * // #H1 #H2 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 …H1 H2)]
 302   |>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 normalize in ⊢ (??%?); #w % [ /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * // ]
 303   ]
 304 qed.