2 \ 5h1
\ 6Moves
\ 5/h1
\ 6We now define the move operation, that corresponds to the advancement of the
3 state in response to the processing of an input character a. The intuition is
4 clear: we have to look at points inside $e$ preceding the given character a,
5 let the point traverse the character, and broadcast it. All other points must
8 We can give a particularly elegant definition in terms of the
9 lifted operators of the previous section:
12 include "tutorial/chapter8.ma".
14 let rec move (S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6) (x:S) (E:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S) on E :
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S ≝
16 [ pz ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"
\ 6pz
\ 5/a
\ 6 S,
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 〉
17 | pe ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6 \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"
\ 6ϵ
\ 5/a
\ 6,
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 〉
18 | ps y ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"
\ 6`
\ 5/a
\ 6y,
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 〉
19 | pp y ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"
\ 6`
\ 5/a
\ 6y, x
\ 5a title="eqb" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6= y 〉
20 | po e1 e2 ⇒ (move ? x e1)
\ 5a title="oplus" href="cic:/fakeuri.def(1)"
\ 6⊕
\ 5/a
\ 6 (move ? x e2)
21 | pc e1 e2 ⇒ (move ? x e1)
\ 5a title="lifted cat" href="cic:/fakeuri.def(1)"
\ 6⊙
\ 5/a
\ 6 (move ? x e2)
22 | pk e ⇒ (move ? x e)
\ 5a title="lk" href="cic:/fakeuri.def(1)"
\ 6^
\ 5/a
\ 6⊛ ].
24 lemma move_plus: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀x:S.∀i1,i2:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.
25 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S x (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 href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x i1)
\ 5a title="oplus" href="cic:/fakeuri.def(1)"
\ 6⊕
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x i2).
28 lemma move_cat: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀x:S.∀i1,i2:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.
29 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S x (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 href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x i1)
\ 5a title="lifted cat" href="cic:/fakeuri.def(1)"
\ 6⊙
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x i2).
32 lemma move_star: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀x:S.∀i:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.
33 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S x 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 href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x i)
\ 5a title="lk" href="cic:/fakeuri.def(1)"
\ 6^
\ 5/a
\ 6⊛.
37 \ 5b
\ 6Example
\ 5/b
\ 6. Let us consider the item
39 (•a + ϵ)((•b)*•a + •b)b
41 and the two moves w.r.t. the characters a and b.
42 For a, we have two possible positions (all other points gets erased); the innermost
43 point stops in front of the final b, while the other one broadcast inside (b^*a + b)b,
46 move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
48 For b, we have two positions too. The innermost point stops in front of the final b too,
49 while the other point reaches the end of b* and must go back through b*a:
51 move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a + ϵ)((•b)*•a + b)•b, false〉
55 definition pmove ≝ λS:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.λx:S.λe:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e).
57 lemma pmove_def : ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀x:S.∀i:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.∀b.
58 \ 5a href="cic:/matita/tutorial/chapter9/pmove.def(7)"
\ 6pmove
\ 5/a
\ 6 ? x
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6i,b〉
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? x i.
61 lemma eq_to_eq_hd: ∀A.∀l1,l2:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.∀a,b.
62 a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l1
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l2 → a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b.
63 #A #l1 #l2 #a #b #H destruct //
66 (* Obviously, a move does not change the carrier of the item, as one can easily
67 prove by induction on the item. *)
69 lemma same_kernel: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀a:S.∀i:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.
70 \ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? a i)|
\ 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|.
72 [#i1 #i2 #H1 #H2 >
\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"
\ 6move_cat
\ 5/a
\ 6 >
\ 5a href="cic:/matita/tutorial/chapter8/erase_odot.def(7)"
\ 6erase_odot
\ 5/a
\ 6 //
73 |#i1 #i2 #H1 #H2 >
\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"
\ 6move_plus
\ 5/a
\ 6 whd in ⊢ (??%%); //
77 (* Here is our first, major result, stating the correctness of the
78 move operation. The proof is a simple induction on i. *)
81 ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀a:S.∀i:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.∀w:
\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"
\ 6word
\ 5/a
\ 6 S.
82 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"
\ 6\sem
\ 5/a
\ 6{
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? a i} w
\ 5a title="iff" href="cic:/fakeuri.def(1)"
\ 6↔
\ 5/a
\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"
\ 6\sem
\ 5/a
\ 6{i} (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:w).
84 [normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"
\ 6conj
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
85 |normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"
\ 6conj
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
86 |normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"
\ 6conj
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
87 |normalize #x #w cases (
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (a
\ 5a title="eqb" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6=x)) #H >H normalize
88 [>(\P H) % [* // #bot @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 //| #H1 destruct /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/]
89 |% [@
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 |#H1 cases (\Pf H) #H2 @H2 destruct //]
91 |#i1 #i2 #HI1 #HI2 #w >
\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"
\ 6move_cat
\ 5/a
\ 6
92 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[|@
\ 5a href="cic:/matita/tutorial/chapter8/sem_odot.def(13)"
\ 6sem_odot
\ 5/a
\ 6] >
\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"
\ 6same_kernel
\ 5/a
\ 6 >
\ 5a href="cic:/matita/tutorial/chapter7/sem_cat_w.def(8)"
\ 6sem_cat_w
\ 5/a
\ 6
93 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[||@(
\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"
\ 6iff_or_l
\ 5/a
\ 6 … (HI2 w))] @
\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"
\ 6iff_or_r
\ 5/a
\ 6
94 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[||@
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @
\ 5a href="cic:/matita/tutorial/chapter6/deriv_middot.def(5)"
\ 6deriv_middot
\ 5/a
\ 6 //]
95 @
\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"
\ 6cat_ext_l
\ 5/a
\ 6 @HI1
96 |#i1 #i2 #HI1 #HI2 #w >(
\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"
\ 6sem_plus
\ 5/a
\ 6 S i1 i2) >
\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"
\ 6move_plus
\ 5/a
\ 6 >
\ 5a href="cic:/matita/tutorial/chapter7/sem_plus_w.def(8)"
\ 6sem_plus_w
\ 5/a
\ 6
97 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[|@
\ 5a href="cic:/matita/tutorial/chapter8/sem_oplus.def(9)"
\ 6sem_oplus
\ 5/a
\ 6]
98 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[|@
\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"
\ 6iff_or_l
\ 5/a
\ 6 [|@HI2]| @
\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"
\ 6iff_or_r
\ 5/a
\ 6 //]
99 |#i1 #HI1 #w >
\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"
\ 6move_star
\ 5/a
\ 6
100 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[|@
\ 5a href="cic:/matita/tutorial/chapter8/sem_ostar.def(13)"
\ 6sem_ostar
\ 5/a
\ 6] >
\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"
\ 6same_kernel
\ 5/a
\ 6 >
\ 5a href="cic:/matita/tutorial/chapter7/sem_star_w.def(8)"
\ 6sem_star_w
\ 5/a
\ 6
101 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6[||@
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @
\ 5a href="cic:/matita/tutorial/chapter6/deriv_middot.def(5)"
\ 6deriv_middot
\ 5/a
\ 6 //]
102 @
\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"
\ 6cat_ext_l
\ 5/a
\ 6 @HI1
106 (* The move operation is generalized to strings in the obvious way. *)
108 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
110 let rec moves (S :
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6) w e on w :
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S ≝
113 | cons x w' ⇒ w' ↦* (
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S x (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e))].
115 lemma moves_empty: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀e:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
116 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ?
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ] e
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 e.
119 lemma moves_cons: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀a:S.∀w.∀e:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
120 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:w) e
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w (
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e)).
123 lemma moves_left : ∀S,a,w,e.
124 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 S (w
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6(a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6])) e
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 S w e)).
125 #S #a #w elim w // #x #tl #Hind #e >
\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"
\ 6moves_cons
\ 5/a
\ 6 >
\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"
\ 6moves_cons
\ 5/a
\ 6 //
128 lemma not_epsilon_sem: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀a:S.∀w:
\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"
\ 6word
\ 5/a
\ 6 S. ∀e:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
129 \ 5a href="cic:/matita/basics/logic/iff.def(1)"
\ 6iff
\ 5/a
\ 6 ((a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:w)
\ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 e) ((a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:w)
\ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e).
130 #S #a #w * #i #b cases b normalize
131 [% /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ * // #H destruct |% normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/]
134 lemma same_kernel_moves: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀w.∀e:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
135 \ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e)|
\ 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
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e|.
139 theorem decidable_sem: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀w:
\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"
\ 6word
\ 5/a
\ 6 S. ∀e:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
140 (
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w 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="iff" href="cic:/fakeuri.def(1)"
\ 6↔
\ 5/a
\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"
\ 6\sem
\ 5/a
\ 6{e} w.
142 [* #i #b >
\ 5a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"
\ 6moves_empty
\ 5/a
\ 6 cases b % /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"
\ 6true_to_epsilon
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
\ 5span class="error" title="error location"
\ 6\ 5/span
\ 6 #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/
143 |#a #w1 #Hind #e >
\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"
\ 6moves_cons
\ 5/a
\ 6
144 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 [||@
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @
\ 5a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"
\ 6not_epsilon_sem
\ 5/a
\ 6]
145 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 [||@
\ 5a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"
\ 6move_ok
\ 5/a
\ 6] @Hind
149 (* It is now clear that we can build a DFA D_e for e by taking pre as states,
150 and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
151 final if and only if b is true. The fact that states in D_e are finite is obvious:
152 in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
153 e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
154 whose finite nature only holds after a suitable quotient.
156 Let us discuss a couple of examples.
158 \ 5b
\ 6Example
\ 5/b
\ 6.
159 Below is the DFA associated with the regular expression (ac+bc)*.
161 \ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"
\ 6
163 The graphical description of the automaton is the traditional one, with nodes for
164 states and labelled arcs for transitions. Unreachable states are not shown.
165 Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
166 only if b is true, we may just label nodes with the item.
167 The automaton is not minimal: it is easy to see that the two states corresponding to
168 the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
169 that they define the same language!). In fact, an important property of pres e is that
170 each state has a clear semantics, given in terms of the specification e and not of the
171 behaviour of the automaton. As a consequence, the construction of the automaton is not
172 only direct, but also extremely intuitive and locally verifiable.
174 Let us consider a more complex case.
176 \ 5b
\ 6Example
\ 5/b
\ 6.
177 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
179 \ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"
\ 6
181 Remarkably, this DFA is minimal, testifying the small number of states produced by our
182 technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7
183 are final, while 8 and 9 are not).
186 \ 5h2
\ 6Move to pit
\ 5/h2
\ 6.
188 We conclude this chapter with a few properties of the move opertions in relation
189 with the pit state. *)
191 definition pit_pre ≝ λS.λi.
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"
\ 6blank
\ 5/a
\ 6 S (
\ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6i|),
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6〉.
193 (* The following function compute the list of characters occurring in a given
196 let rec occur (S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6) (i:
\ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"
\ 6re
\ 5/a
\ 6 S) on i ≝
198 [ z ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
199 | e ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
200 | s y ⇒ y
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
201 | o e1 e2 ⇒
\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"
\ 6unique_append
\ 5/a
\ 6 ? (occur S e1) (occur S e2)
202 | c e1 e2 ⇒
\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"
\ 6unique_append
\ 5/a
\ 6 ? (occur S e1) (occur S e2)
205 (* If a symbol a does not occur in i, then move(i,a) gets to the
208 lemma not_occur_to_pit: ∀S,a.∀i:
\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"
\ 6pitem
\ 5/a
\ 6 S.
\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"
\ 6memb
\ 5/a
\ 6 S a (
\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"
\ 6occur
\ 5/a
\ 6 S (
\ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6i|))
\ 5a title="leibnitz's non-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 →
209 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S a i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"
\ 6pit_pre
\ 5/a
\ 6 S i.
211 [#x normalize cases (a
\ 5a title="eqb" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6=x) 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/
212 |#i1 #i2 #Hind1 #Hind2 #H >
\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"
\ 6move_cat
\ 5/a
\ 6
213 >Hind1 [2:@(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 @
\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"
\ 6sublist_unique_append_l1
\ 5/a
\ 6 //]
214 >Hind2 [2:@(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 @
\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"
\ 6sublist_unique_append_l2
\ 5/a
\ 6 //] //
215 |#i1 #i2 #Hind1 #Hind2 #H >
\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"
\ 6move_plus
\ 5/a
\ 6
216 >Hind1 [2:@(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 @
\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"
\ 6sublist_unique_append_l1
\ 5/a
\ 6 //]
217 >Hind2 [2:@(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 @
\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"
\ 6sublist_unique_append_l2
\ 5/a
\ 6 //] //
218 |#i #Hind #H >
\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"
\ 6move_star
\ 5/a
\ 6 >Hind //
222 (* We cannot escape form the pit state. *)
224 lemma move_pit: ∀S,a,i.
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"
\ 6pit_pre
\ 5/a
\ 6 S i))
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"
\ 6pit_pre
\ 5/a
\ 6 S i.
226 [#i1 #i2 #Hind1 #Hind2 >
\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"
\ 6move_cat
\ 5/a
\ 6 >Hind1 >Hind2 //
227 |#i1 #i2 #Hind1 #Hind2 >
\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"
\ 6move_plus
\ 5/a
\ 6 >Hind1 >Hind2 //
228 |#i #Hind >
\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"
\ 6move_star
\ 5/a
\ 6 >Hind //
232 lemma moves_pit: ∀S,w,i.
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 S w (
\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"
\ 6pit_pre
\ 5/a
\ 6 S i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"
\ 6pit_pre
\ 5/a
\ 6 S i.
236 (* If any character in w does not occur in i, then moves(i,w) gets
239 lemma to_pit: ∀S,w,e.
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"
\ 6sublist
\ 5/a
\ 6 S w (
\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"
\ 6occur
\ 5/a
\ 6 S (
\ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e|)) →
240 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 S w e
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"
\ 6pit_pre
\ 5/a
\ 6 S (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e).
242 [#e * #H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @H normalize #a #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/
243 |#a #tl #Hind #e #H cases (
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"
\ 6memb
\ 5/a
\ 6 S a (
\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"
\ 6occur
\ 5/a
\ 6 S (
\ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e|))))
244 [#Htrue >
\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"
\ 6moves_cons
\ 5/a
\ 6 whd in ⊢ (???%); <(
\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"
\ 6same_kernel
\ 5/a
\ 6 … a)
245 @Hind >
\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"
\ 6same_kernel
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 #b #memb cases (
\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"
\ 6orb_true_l
\ 5/a
\ 6 … memb)
246 [#H2 >(\P H2) // |#H2 @H1 //]
247 |#Hfalse >
\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"
\ 6moves_cons
\ 5/a
\ 6 >
\ 5a href="cic:/matita/tutorial/chapter9/not_occur_to_pit.def(8)"
\ 6not_occur_to_pit
\ 5/a
\ 6 // >Hfalse /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"
\ 6eqnot_to_noteq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/