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 ≝
match E with
- [ 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 〉
- | 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 〉
- | 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 〉
- | 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 〉
+ [ pz ⇒ 〈\ 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 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+ | 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 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+ | 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 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
+ | 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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6
| po e1 e2 ⇒ (move ? x e1) \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 (move ? x e2)
| pc e1 e2 ⇒ (move ? x e1) \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 (move ? x e2)
- | pk e ⇒ (move ? x e)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ ].
+ | pk e ⇒ (move ? x e)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6⊛\ 5/a\ 6 ].
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.
\ 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).
// qed.
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.
- \ 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⊛.
+ \ 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="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\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6⊛\ 5/a\ 6.
// qed.
(*
-Example. Let us consider the item
+\ 5b\ 6Example\ 5/b\ 6. Let us consider the item
(•a + ϵ)((•b)*•a + •b)b
point stops in front of the final b, while the other one broadcast inside (b^*a + b)b,
so
- move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
+ move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
For b, we have two positions too. The innermost point stops in front of the final b too,
while the other point reaches the end of b* and must go back through b*a:
- move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a + ϵ)((•b)*•a + b)•b, false〉
+ move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a + ϵ)((•b)*•a + b)•b, false〉
*)
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).
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.
- \ 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.
+ \ 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="Pair construction" 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.
// qed.
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.
- 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.
+ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1 \ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2 → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
#A #l1 #l2 #a #b #H destruct //
qed.
prove by induction on the item. *)
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.
- \ 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|.
+ \ 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="forget" 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="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
#S #a #i elim i //
[#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 //
|#i1 #i2 #H1 #H2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 whd in ⊢ (??%%); //
theorem move_ok:
∀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.
- \ 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).
+ \ 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\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 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\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w).
#S #a #i elim i
[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/
|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/
|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/
- |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
+ |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\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) #H >H normalize
[>(\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/]
|% [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 |#H1 cases (\Pf H) #H2 @H2 destruct //]
]
notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
-let rec moves (S : DeqSet) w e on w : pre S ≝
+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 ≝
match w with
[ nil ⇒ e
- | cons x w' ⇒ w' ↦* (move S x (\fst e))].
+ | 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))].
-lemma moves_empty: ∀S:DeqSet.∀e:pre S.
- moves ? [ ] e = e.
+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.
+ \ 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 \ 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.
// qed.
-lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
- moves ? (a::w) e = moves ? w (move S a (\fst e)).
+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.
+ \ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w) 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)).
// qed.
lemma moves_left : ∀S,a,w,e.
- moves S (w@[a]) e = move S a (\fst (moves S w e)).
-#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+ \ 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="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" 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)).
+#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 //
qed.
-lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
- iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+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.
+ \ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w) \ 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\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6w) \ 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).
#S #a #w * #i #b cases b normalize
- [% /2/ * // #H destruct |% normalize /2/]
+ [% /\ 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/]
qed.
-lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
- |\fst (moves ? w e)| = |\fst e|.
+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.
+ \ 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="forget" 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\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
#S #w elim w //
qed.
-theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
- (\snd (moves ? w e) = true) ↔ \sem{e} w.
+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.
+ (\ 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\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w.
#S #w elim w
- [* #i #b >moves_empty cases b % /2/
- |#a #w1 #Hind #e >moves_cons
- @iff_trans [||@iff_sym @not_epsilon_sem]
- @iff_trans [||@move_ok] @Hind
+ [* #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/ #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/
+ |#a #w1 #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6
+ @\ 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]
+ @\ 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
]
qed.
(* It is now clear that we can build a DFA D_e for e by taking pre as states,
-and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
+and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
final if and only if b is true. The fact that states in D_e are finite is obvious:
in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
whose finite nature only holds after a suitable quotient.
Let us discuss a couple of examples.
+
+\ 5b\ 6Example\ 5/b\ 6.
Below is the DFA associated with the regular expression (ac+bc)*.
-\includegraphics[width=.8\textwidth]{acUbc.pdf}
-\caption{DFA for $(ac+bc)^*$\label{acUbc}}
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"\ 6
The graphical description of the automaton is the traditional one, with nodes for
states and labelled arcs for transitions. Unreachable states are not shown.
-Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
+Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
only if b is true, we may just label nodes with the item.
The automaton is not minimal: it is easy to see that the two states corresponding to
the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
only direct, but also extremely intuitive and locally verifiable.
Let us consider a more complex case.
+
+\ 5b\ 6Example\ 5/b\ 6.
Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
-\includegraphics[width=.8\textwidth]{automaton.pdf}
-\caption{DFA for $(a+\epsilon)(b^*a + b)b$\label{automaton}}
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"\ 6
Remarkably, this DFA is minimal, testifying the small number of states produced by our
-technique (the pair ofstates $6-8$ and $7-9$ differ for the fact that $6$ and $7$
-are final, while $8$ and $9$ are not).
-*)
+technique (the pair of states 6-8 and 7-9 differ for the fact that 6 and 7
+are final, while 8 and 9 are not).
+
+
+\ 5h2\ 6Move to pit\ 5/h2\ 6.
+
+We conclude this chapter with a few properties of the move opertions in relation
+with the pit state. *)
-(************************ pit state ***************************)
-definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
+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 title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6), \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
-let rec occur (S: DeqSet) (i: re S) on i ≝
+(* The following function compute the list of characters occurring in a given
+item i. *)
+
+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 ≝
match i with
- [ z ⇒ [ ]
- | e ⇒ [ ]
- | s y ⇒ [y]
- | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
- | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ [ z ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | e ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | s y ⇒ y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | 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)
+ | 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)
| k e ⇒ occur S e].
-lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
- move S a i = pit_pre S i.
+(* If a symbol a does not occur in i, then move(i,a) gets to the
+pit state. *)
+
+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="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) \ 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 →
+ \ 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.
#S #a #i elim i //
- [#x normalize cases (a==x) normalize // #H @False_ind /2/
- |#i1 #i2 #Hind1 #Hind2 #H >move_cat
- >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
- >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
- |#i1 #i2 #Hind1 #Hind2 #H >move_plus
- >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
- >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
- |#i #Hind #H >move_star >Hind //
+ [#x normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x) 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/
+ |#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6
+ >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 //]
+ >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 //] //
+ |#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6
+ >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 //]
+ >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 //] //
+ |#i #Hind #H >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6 >Hind //
]
qed.
-lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+(* We cannot escape form the pit state. *)
+
+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.
#S #a #i elim i //
- [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
- |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
- |#i #Hind >move_star >Hind //
+ [#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 >Hind1 >Hind2 //
+ |#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 >Hind1 >Hind2 //
+ |#i #Hind >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6 >Hind //
]
qed.
-lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+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.
#S #w #i elim w //
qed.
-lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
- moves S w e = pit_pre S (\fst e).
+(* If any character in w does not occur in i, then moves(i,w) gets
+to the pit state. *)
+
+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\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) →
+ \ 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).
#S #w elim w
- [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
- |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
- [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
- @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+ [#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/
+ |#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\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))))
+ [#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)
+ @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)
[#H2 >(\P H2) // |#H2 @H1 //]
- |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
+ |#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/
]
]
qed.
\ No newline at end of file
projects / helm.git / blobdiff