From: matitaweb Date: Tue, 6 Mar 2012 13:56:12 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1900 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e093d15aa59216997eeb3b55008dae069dbc6db6;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index fb11216e5..c9a65f57b 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -107,42 +107,42 @@ qed. 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 : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) w e on w : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ match w with [ nil ⇒ e - | cons x w' ⇒ w' ↦* (move S x (\fst e))]. + | cons x w' ⇒ w' ↦* (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e))]. -lemma moves_empty: ∀S:DeqSet.∀e:pre S. - moves ? [ ] e = e. +lemma moves_empty: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? a title="nil" href="cic:/fakeuri.def(1)"[/a ] e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:w) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a 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 // + a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S (wa title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa]) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e)). +#S #a #w elim w // #x #tl #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a // 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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a href="cic:/matita/basics/logic/iff.def(1)"iff/a ((aa title="cons" href="cic:/fakeuri.def(1)":/a:w) a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e) ((aa title="cons" href="cic:/fakeuri.def(1)":/a:w) a title="in_pl mem" href="cic:/fakeuri.def(1)"∈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e). #S #a #w * #i #b cases b normalize - [% /2/ * // #H destruct |% normalize /2/] + [% /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ * // #H destruct |% normalize /span class="autotactic"2span class="autotrace" trace /span/span/] qed. -lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S. - |\fst (moves ? w e)| = |\fst e|. +lemma same_kernel_moves: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e)| a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e|. #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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. + (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e} 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 >a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"moves_empty/a cases b % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"true_to_epsilon/a/span/span/span class="error" title="error location"/span #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#a #w1 #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a + @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a [||@a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"not_epsilon_sem/a] + @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a [||@a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"move_ok/a] @Hind ] qed. @@ -158,7 +158,7 @@ Let us discuss a couple of examples. bExample/b. Below is the DFA associated with the regular expression (ac+bc)*. -img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/ +img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)" The graphical description of the automaton is the traditional one, with nodes for states and labelled arcs for transitions. Unreachable states are not shown. @@ -176,14 +176,13 @@ Let us consider a more complex case. bExample/b. Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton. -img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"/ +img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b" 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 +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). -*) -(* + h2Move to pit/h2. We conclude this chapter with a few properties of the move opertions in relation