X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmarks.ma;h=e82d577bc3ed666240af9ef6013d5f4b2f8d5f86;hb=bed400cf37906a25129907986b10f24cb499dbb4;hp=b4a8ca5fc0875f38d319f419818eba5471617c33;hpb=9957a050f4bc4ce95d3d98981eba19515021ce72;p=helm.git diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma index b4a8ca5fc..e82d577bc 100644 --- a/matita/matita/lib/turing/universal/marks.ma +++ b/matita/matita/lib/turing/universal/marks.ma @@ -750,28 +750,6 @@ cases Hif -Hif ] qed. -(* -lemma sem_match_and_adv : - âalpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f). -#alpha #f #intape -cases (sem_if ? (test_char ? f) ⦠tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape) -#k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc) -% [ @Hloop ] -Hloop -cases Hif -[ * #ta * whd in ⢠(%â%â?); #Hta #Houtc - #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta; - * * #x1 * whd in ⢠((??%?)â?); #H destruct (H) #Hf #Hta % % - [ @Hf | >append_cons >append_cons in Hta; #Hta @(proj1 ?? (Houtc â¦) â¦Hta) - [ #x #memx cases (memb_append â¦memx) - [@Hl1 | -memx #memx >(memb_single ⦠memx) %] - |>reverse_cons >reverse_append % ] ] -| * #ta * whd in ⢠(%â%â?); #Hta #Houtc - #l0 #x #a #l1 #x0 #a0 #l2 #Hl1 #Hintape >Hintape in Hta; - * #Hf #Hta %2 % [ @Hf % | >(proj2 ?? Houtc ⦠Hta) % ] -] -qed. -*) - definition R_match_and_adv_of â λalpha,t1,t2.current (FinProd ⦠alpha FinBool) t1 = None ? â t2 = t1. @@ -796,18 +774,6 @@ cases (sem_match_and_adv_of ? f intape) #i0 * #outc0 * #Hloop0 #HR2 >(loop_eq ⦠Hloop Hloop0) // qed. -(* - if x = c - then move_right; ---- - adv_to_mark_r; - if current (* x0 *) = 0 - then advance_mark ---- - adv_to_mark_l; - advance_mark - else STOP - else M -*) - definition comp_step_subcase â λalpha,c,elseM. ifTM ? (test_char ? (λx.x == c)) (move_r ⦠· adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c)) @@ -1143,182 +1109,7 @@ lemma sem_comp_step : ] qed. -(* old universal version - -definition R_comp_step_true â λt1,t2. - âls,c,rs.t1 = midtape (FinProd ⦠FSUnialpha FinBool) ls â©c,true⪠rs â - (* bit_or_null c = false *) - (bit_or_null c = false â t2 = midtape ? ls â©c,false⪠rs) ⧠- (* no marks in rs *) - (bit_or_null c = true â - (âc.memb ? c rs = true â is_marked ? c = false) â - âa,l. (a::l) = reverse ? (â©c,trueâª::rs) â - t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ⧠- (âl1,c0,l2. - bit_or_null c = true â - (âc.memb ? c l1 = true â is_marked ? c = false) â - rs = l1@â©c0,trueâª::l2 â - (c = c0 â - l2 = [ ] â (* test true but l2 is empty *) - t2 = rightof ? â©c0,false⪠((reverse ? l1)@â©c,trueâª::ls)) ⧠- (c = c0 â - âa,a0,b,l1',l2'. (* test true and l2 is not empty *) - â©a,falseâª::l1' = l1@[â©c0,falseâª] â - l2 = â©a0,bâª::l2' â - t2 = midtape ? (â©c,falseâª::ls) â©a,true⪠(l1'@â©a0,trueâª::l2')) ⧠- (c â c0 â(* test false *) - t2 = midtape (FinProd ⦠FSUnialpha FinBool) - ((reverse ? l1)@â©c,trueâª::ls) â©c0,false⪠l2)). - -definition R_comp_step_false â - λt1,t2. - âls,c,rs.t1 = midtape (FinProd ⦠FSUnialpha FinBool) ls c rs â - is_marked ? c = false ⧠t2 = t1. - -(* -lemma is_marked_to_exists: âalpha,c. is_marked alpha c = true â - âc'. c = â©c',trueâª. -#alpha * c *) - -lemma sem_comp_step : - accRealize ? comp_step (inr ⦠(inl ⦠(inr ⦠start_nop))) - R_comp_step_true R_comp_step_false. -@(acc_sem_if_app ⦠(sem_test_char ? (is_marked ?)) - (sem_comp_step_subcase FSUnialpha â©bit false,true⪠?? - (sem_comp_step_subcase FSUnialpha â©bit true,true⪠?? - (sem_comp_step_subcase FSUnialpha â©null,true⪠?? - (sem_clear_mark â¦)))) - (sem_nop â¦) â¦) -[#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape whd in Hta; - >Hintape in Hta; * #_ -Hintape (* forse non serve *) - cases (true_or_false (c==bit false)) #Hc - [>(\P Hc) #Hta % - [%[whd in ⢠((??%?)â?); #Hdes destruct - |#Hc @(proj1 ?? (proj1 ?? (Htb ⦠Hta) (refl â¦))) - ] - |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb ⦠Hta) (refl â¦))) - ] - |cases (true_or_false (c==bit true)) #Hc1 - [>(\P Hc1) #Hta - cut (â©bit true, true⪠â â©bit false, trueâª) [% #Hdes destruct] #Hneq % - [%[whd in ⢠((??%?)â?); #Hdes destruct - |#Hc @(proj1 ⦠(proj1 ?? (proj2 ?? (Htb ⦠Hta) Hneq ⦠Hta) (refl â¦))) - ] - |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb ⦠Hta) Hneq ⦠Hta)(refl â¦))) - ] - |cases (true_or_false (c==null)) #Hc2 - [>(\P Hc2) #Hta - cut (â©null, true⪠â â©bit false, trueâª) [% #Hdes destruct] #Hneq - cut (â©null, true⪠â â©bit true, trueâª) [% #Hdes destruct] #Hneq1 % - [%[whd in ⢠((??%?)â?); #Hdes destruct - |#Hc @(proj1 ⦠(proj1 ?? (proj2 ?? (proj2 ?? (Htb ⦠Hta) Hneq ⦠Hta) Hneq1 ⦠Hta) (refl â¦))) - ] - |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb ⦠Hta) Hneq ⦠Hta) Hneq1 ⦠Hta) (refl â¦))) - ] - |#Hta cut (bit_or_null c = false) - [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2 - cases c normalize [* normalize /2/] /2/] #Hcut % - [%[cases (Htb ⦠Hta) #_ -Htb #Htb - cases (Htb ⦠Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb - cases (Htb ⦠Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb - lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct] - * #_ #Houttape #_ @(Houttape ⦠Hta) - |>Hcut #H destruct - ] - |#l1 #c0 #l2 >Hcut #H destruct - ] - ] - ] - ] -|#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape - >Hintape in Hta; whd in ⢠(%â?); * #Hmark #Hta % [@Hmark //] - whd in Htb; >Htb // -] -qed. *) - -(* -definition R_comp_step_true â - λt1,t2. - âl0,c,rs.t1 = midtape (FinProd ⦠FSUnialpha FinBool) l0 c rs â - âc'. c = â©c',true⪠⧠- ((bit_or_null c' = true ⧠- âa,l1,c0,a0,l2. - rs = â©a,falseâª::l1@â©c0,trueâª::â©a0,falseâª::l2 â - (âc.memb ? c l1 = true â is_marked ? c = false) â - (c0 = c' ⧠- t2 = midtape ? (â©c',falseâª::l0) â©a,true⪠(l1@â©c0,falseâª::â©a0,trueâª::l2)) ⨠- (c0 â c' ⧠- t2 = midtape (FinProd ⦠FSUnialpha FinBool) - (reverse ? l1@â©a,falseâª::â©c',trueâª::l0) â©c0,false⪠(â©a0,falseâª::l2))) ⨠- (bit_or_null c' = false ⧠t2 = midtape ? l0 â©c',false⪠rs)). - -definition R_comp_step_false â - λt1,t2. - âls,c,rs.t1 = midtape (FinProd ⦠FSUnialpha FinBool) ls c rs â - is_marked ? c = false ⧠t2 = t1. - -lemma sem_comp_step : - accRealize ? comp_step (inr ⦠(inl ⦠(inr ⦠start_nop))) - R_comp_step_true R_comp_step_false. -#intape -cases (acc_sem_if ⦠(sem_test_char ? (is_marked ?)) - (sem_comp_step_subcase FSUnialpha â©bit false,true⪠?? - (sem_comp_step_subcase FSUnialpha â©bit true,true⪠?? - (sem_comp_step_subcase FSUnialpha â©null,true⪠?? - (sem_clear_mark â¦)))) - (sem_nop â¦) intape) -#k * #outc * * #Hloop #H1 #H2 -@(ex_intro ?? k) @(ex_intro ?? outc) % -[ % [@Hloop ] ] -Hloop -[ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 * - #ta * whd in ⢠(%â?); #Hleft #Hright #ls #c #rs #Hintape - >Hintape in Hleft; * * - cases c in Hintape; #c' #b #Hintape #x * whd in ⢠(??%?â?); #H destruct (H) - whd in ⢠(??%?â?); #Hb >Hb #Hta @(ex_intro ?? c') % // - cases (Hright ⦠Hta) - [ * #Hc' #H1 % % [destruct (Hc') % ] - #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1 - cases (H1 ⦠Hl1 Hrs) - [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc - | * #Hneq #Houtc %2 % - [ @sym_not_eq // - | @Houtc ] - ] - | * #Hc #Helse1 cases (Helse1 ⦠Hta) - [ * #Hc' #H1 % % [destruct (Hc') % ] - #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1 - cases (H1 ⦠Hl1 Hrs) - [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc - | * #Hneq #Houtc %2 % - [ @sym_not_eq // - | @Houtc ] - ] - | * #Hc' #Helse2 cases (Helse2 ⦠Hta) - [ * #Hc'' #H1 % % [destruct (Hc'') % ] - #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1 - cases (H1 ⦠Hl1 Hrs) - [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc - | * #Hneq #Houtc %2 % - [ @sym_not_eq // - | @Houtc ] - ] - | * #Hc'' whd in ⢠(%â?); #Helse3 %2 % - [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc; - cases c' - [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) % - | #Hfalse @False_ind @(absurd ?? Hfalse) % ] - | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) % - |*: #_ #_ #_ % ] - | @(Helse3 ⦠Hta) - ] - ] - ] - ] -| #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 * - #ta * whd in ⢠(%â%â?); #Hleft #Hright #ls #c #rs #Hintape - >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //] -] -qed.*) +(* compare *) definition compare â whileTM ? comp_step (inr ⦠(inl ⦠(inr ⦠start_nop))). @@ -1539,47 +1330,59 @@ lemma not_nil_to_exists:âA.âl: list A. l â [ ] â #A * [* #H @False_ind @H // | #a #tl #_ @(ex_intro ⦠a) @(ex_intro ⦠tl) //] qed. -axiom daemon : âP:Prop.P. - lemma terminate_compare: ât. Terminate ? compare t. #t @(terminate_while ⦠sem_comp_step) [%] cases t // #ls * #c * // -#rs lapply ls; lapply c; -ls -c +#rs (* we cannot proceed by structural induction on the right tape, since compare moves the marks! *) -elim rs - [#c #ls @wf #t1 whd in ⢠(%â?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid) +cut (âlen. |rs| = len) [/2/] +* #len lapply rs lapply c lapply ls -ls -c -rs elim len + [#ls #c #rs #Hlen >(lenght_to_nil ⦠Hlen) @wf #t1 whd in ⢠(%â?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid) * * #H1 #H2 #_ cases (true_or_false (bit_or_null c0)) #Hc0 [>(H2 Hc0 ⦠(refl â¦)) // #x whd in ⢠((??%?)â?); #Hdes destruct |>(H1 Hc0) // ] - |#a #rs' #Hind #c #ls @wf #t1 whd in ⢠(%â?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid) + |-len #len #Hind #ls #c #rs #Hlen @wf #t1 whd in ⢠(%â?); * #ls0 * #c0 * #rs0 * #Hmid destruct (Hmid) * * #H1 #H2 #H3 cases (true_or_false (bit_or_null c0)) #Hc0 - [-H1 cases (split_on_spec_ex ? (a::rs') (is_marked ?)) #rs1 * #rs2 + [-H1 cases (split_on_spec_ex ? rs0 (is_marked ?)) #rs1 * #rs2 cases rs2 [(* no marks in right tape *) * * >append_nil #H >H -H #Hmarks #_ - cases (not_nil_to_exists ? (reverse (FSUnialphaÃbool) (â©c0,trueâª::a::rs')) ?) + cases (not_nil_to_exists ? (reverse (FSUnialphaÃbool) (â©c0,trueâª::rs0)) ?) [2: % >reverse_cons #H cases (nil_to_nil ⦠H) #_ #H1 destruct] #a0 * #tl #H4 >(H2 Hc0 Hmarks a0 tl H4) // |(* the first marked element is a0 *) * #a0 #a0b #rs3 * * #H4 #H5 #H6 lapply (H3 ? a0 rs3 ⦠Hc0 H5 ?) [