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=bfa8b8a748b48c7702770253ac1809da712f8971;hpb=ce60ad8a7d4c56f218d95c3547abe896057de040;p=helm.git diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma index bfa8b8a74..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)) @@ -996,27 +962,27 @@ let rec split_on A (l:list A) f acc on l ≝ if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc) ]. -lemma split_on_spec: ∀A,l,f,acc,res1,res2. +lemma split_on_spec: ∀A:DeqSet.∀l,f,acc,res1,res2. split_on A l f acc = 〈res1,res2〉 → (∃l1. res1 = l1@acc ∧ reverse ? l1@res2 = l ∧ - ∀x. mem ? x l1 → f x = false) ∧ + ∀x. memb ? x l1 =true → f x = false) ∧ ∀a,tl. res2 = a::tl → f a = true. #A #l #f elim l [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct % - [@(ex_intro … []) % normalize [% % | #x @False_ind] + [@(ex_intro … []) % normalize [% % | #x #H destruct] |#a #tl #H destruct ] |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?); cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?); #H destruct - [% [@(ex_intro … []) % normalize [% % | #x @False_ind] + [% [@(ex_intro … []) % normalize [% % | #x #H destruct] |#a1 #tl1 #H destruct (H) //] |cases (Hind (a::acc) res1 res2 H) * #l1 * * #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) % [% [>associative_append @Hres1 | >reverse_append H //| @False_ind] + |#x #Hmemx cases (memb_append ???? Hmemx) + [@Hfalse | #H >(memb_single … H) //] ] ] ] @@ -1024,14 +990,14 @@ qed. axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l. -lemma split_on_spec_ex: ∀A,l,f.∃l1,l2. - l1@l2 = l ∧ (∀x:A. mem ? x l1 → f x = false) ∧ +lemma split_on_spec_ex: ∀A:DeqSet.∀l,f.∃l1,l2. + l1@l2 = l ∧ (∀x:A. memb ? x l1 = true → f x = false) ∧ ∀a,tl. l2 = a::tl → f a = true. #A #l #f @(ex_intro … (reverse … (\fst (split_on A l f [])))) @(ex_intro … (\snd (split_on A l f []))) cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * * >append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue % - [% [@Hl|#x #memx @Hfalse @mem_reverse //] | @Htrue] + [% [@Hl|#x #memx @Hfalse <(reverse_reverse … l1) @memb_reverse //] | @Htrue] qed. (* versione esistenziale *) @@ -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))). @@ -1455,124 +1246,143 @@ lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%] >reverse_append >reverse_append >associative_append >associative_append % ] - |lapply Hbs1 lapply Hbs2 lapply Hrs -Hbs1 -Hbs2 -Hrs + |lapply Hbs1 lapply Hb0s1 lapply Hbs2 lapply Hb0s2 lapply Hrs + -Hbs1 -Hb0s1 -Hbs2 -Hb0s2 -Hrs @(list_cases2 … Hlen) - [#Hrs #_ #_ >associative_append >associative_append #Htapeb #_ + [#Hrs #_ #_ #_ #_ >associative_append >associative_append #Htapeb #_ lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb cases (IH … Htapeb) -IH * #Hout #_ #_ %1 % [>(\P eqbb0) % |>(Hout grid (refl …) (refl …)) @eq_f normalize >associative_append % ] - |* #a1 #ba1 * #a2 #ba2 #tl1 #tl2 #HlenS #Hrs #Hbs1 #Hbs2 - cut (ba1 = false) [@(Hbs1 〈a1,ba1〉) @memb_hd] #Hba1 >Hba1 + |* #a1 #ba1 * #a2 #ba2 #tl1 #tl2 #HlenS #Hrs #Hb0s2 #Hbs2 #Hb0s1 #Hbs1 + cut (ba1 = false) [@(Hbs2 〈a1,ba1〉) @memb_hd] #Hba1 >Hba1 >associative_append >associative_append #Htapeb #_ lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb cases (IH … Htapeb) -IH * #_ #_ + cut (ba2=false) [@(Hb0s2 〈a2,ba2〉) @memb_hd] #Hba2 >Hba2 #IH cases(IH a1 a2 ?? (l1@[〈b0,false〉]) l2 HlenS ????? (refl …) ??) - [ - - -(* - cut (∃a,l1'.〈a,false〉::l1'=((bs@[〈grid,false〉])@l1)@[〈b0,false〉]) - [generalize in match Hbs2; cases bs - [#_ @(ex_intro … grid) @(ex_intro … (l1@[〈b0,false〉])) - >associative_append % - |* #bsc #bsb #bstl #Hbs2 @(ex_intro … bsc) - @(ex_intro … (((bstl@[〈grid,false〉])@l1)@[〈b0,false〉])) - normalize @eq_f2 [2:%] @eq_f @sym_eq @(Hbs2 〈bsc,bsb〉) @memb_hd - ] - ] - * #a * #l1' #H2 - cut (∃a0,b1,l2'.b0s@〈comma,false〉::l2=〈a0,b1〉::l2') - [cases b0s - [@(ex_intro … comma) @(ex_intro … false) @(ex_intro … l2) % - |* #bsc #bsb #bstl @(ex_intro … bsc) @(ex_intro … bsb) - @(ex_intro … (bstl@〈comma,false〉::l2)) % - ] - ] *) - * #a0 * #b1 * #l2' #H3 - lapply (Htapeb … (\P eqbb0) a a0 b1 l1' l2' H2 H3) -Htapeb #Htapeb - cases (IH … Htapeb) -IH * - - - [2: * >Hc' #Hfalse @False_ind destruct ] * #_ - @(list_cases2 … Hlen) - [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?); - -Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft - [ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_ - % % - [ >Heqb >Hbs >Hb0s % - | >Hbs >Hb0s @IH % - ] - |* #Hneqb #Htapeb %2 - @(ex_intro … [ ]) @(ex_intro … b) - @(ex_intro … b0) @(ex_intro … [ ]) - @(ex_intro … [ ]) % - [ % [ % [@sym_not_eq //| >Hbs %] | >Hb0s %] - | cases (IH … Htapeb) -IH * #_ #IH #_ >(IH ? (refl ??)) - @Htapeb - ] - | @Hl1 ] - | * #b' #bitb' * #b0' #bitb0' #bs' #b0s' #Hbs #Hb0s - generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?); - cut (bit_or_null b' = true ∧ bit_or_null b0' = true ∧ - bitb' = false ∧ bitb0' = false) - [ % [ % [ % [ >Hbs in Hbs1; #Hbs1 @(Hbs1 〈b',bitb'〉) @memb_hd - | >Hb0s in Hb0s1; #Hb0s1 @(Hb0s1 〈b0',bitb0'〉) @memb_hd ] - | >Hbs in Hbs2; #Hbs2 @(Hbs2 〈b',bitb'〉) @memb_hd ] - | >Hb0s in Hb0s2; #Hb0s2 @(Hb0s2 〈b0',bitb0'〉) @memb_hd ] - | * * * #Ha #Hb #Hc #Hd >Hc >Hd - #Hrs #Hleft - cases (Hleft b' (bs'@〈grid,false〉::l1) b0 b0' - (b0s'@〈comma,false〉::l2) ??) -Hleft - [ 3: >Hrs normalize @eq_f >associative_append % - | * #Hb0 #Htapeb cases (IH …Htapeb) -IH * #_ #_ #IH - cases (IH b' b0' bs' b0s' (l1@[〈b0,false〉]) l2 ??????? Ha ?) -IH - [ * #Heq #Houtc % % - [ >Hb0 @eq_f >Hbs in Heq; >Hb0s in ⊢ (%→?); #Heq - destruct (Heq) >Hb0s >Hc >Hd % - | >Houtc >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append - >associative_append % + [3:#x #memx @Hbs1 @memb_cons @memx + |4:#x #memx @Hb0s1 @memb_cons @memx + |5:#x #memx @Hbs2 @memb_cons @memx + |6:#x #memx @Hb0s2 @memb_cons @memx + |7:#x #memx cases (memb_append …memx) -memx #memx + [@Hl1 @memx | >(memb_single … memx) %] + |8:@(Hbs1 〈a1,ba1〉) @memb_hd + |9: >associative_append >associative_append % + |-IH -Hbs1 -Hb0s1 -Hbs2 -Hrs * + #Ha1a2 #Houtc %1 % + [>(\P eqbb0) @eq_f destruct (Ha1a2) % + |>Houtc @eq_f3 + [>reverse_cons >associative_append % + |% + |>associative_append % + ] ] - | * #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #H4 %2 - @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d') - @(ex_intro … lb) @(ex_intro … lc) - % [ % [ % // >Hbs >Hc >H2 % | >Hb0s >Hd >H3 >Hb0 % ] - | >H4 >Hbs >Hb0s >Hc >Hd >Hb0 >reverse_append - >reverse_cons >reverse_cons - >associative_append >associative_append - >associative_append >associative_append % + |-IH -Hbs1 -Hb0s1 -Hbs2 -Hrs * + #la * #c' * #d' * #lb * #lc * * * + #Hcd #H1 #H2 #Houtc %2 + @(ex_intro … (〈b,false〉::la)) @(ex_intro … c') @(ex_intro … d') + @(ex_intro … lb) @(ex_intro … lc) % + [%[%[@Hcd | >H1 %] |>(\P eqbb0) >Hba2 >H2 %] + |>Houtc @eq_f3 + [>(\P eqbb0) >reverse_append >reverse_cons + >reverse_cons >associative_append >associative_append + >associative_append >associative_append % + |% + |% ] - | generalize in match Hlen; >Hbs >Hb0s - normalize #Hlen destruct (Hlen) @e0 - | #c0 #Hc0 @Hbs1 >Hbs @memb_cons // - | #c0 #Hc0 @Hb0s1 >Hb0s @memb_cons // - | #c0 #Hc0 @Hbs2 >Hbs @memb_cons // - | #c0 #Hc0 @Hb0s2 >Hb0s @memb_cons // - | #c0 #Hc0 cases (memb_append … Hc0) - [ @Hl1 | #Hc0' >(memb_single … Hc0') % ] - | % - | >associative_append >associative_append % ] - | * #Hneq #Htapeb %2 - @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0) - @(ex_intro … bs) @(ex_intro … b0s) % - [ % // % // @sym_not_eq // - | >Hbs >Hb0s >Hc >Hd >reverse_cons >associative_append - >reverse_append in Htapeb; >reverse_cons - >associative_append >associative_append - #Htapeb Hbs @memb_cons @Hyp - | cases (orb_true_l … Hyp) - [ #Hyp2 >(\P Hyp2) % - | @Hl1 - ] - ] - ] -]]]]] -qed. + ] + ] + ] + ] + ] + ] + ] +] +qed. + +lemma WF_cst_niltape: + WF ? (inv ? R_comp_step_true) (niltape (FinProd FSUnialpha FinBool)). +@wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct +qed. + +lemma WF_cst_rightof: + ∀a,ls. WF ? (inv ? R_comp_step_true) (rightof (FinProd FSUnialpha FinBool) a ls). +#a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct +qed. + +lemma WF_cst_leftof: + ∀a,ls. WF ? (inv ? R_comp_step_true) (leftof (FinProd FSUnialpha FinBool) a ls). +#a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #c * #rs * #H destruct +qed. + +lemma WF_cst_midtape_false: + ∀ls,c,rs. WF ? (inv ? R_comp_step_true) + (midtape (FinProd … FSUnialpha FinBool) ls 〈c,false〉 rs). +#ls #c #rs @wf #t1 whd in ⊢ (%→?); * #ls' * #c' * #rs' * #H destruct +qed. + +(* da spostare *) +lemma not_nil_to_exists:∀A.∀l: list A. l ≠ [ ] → + ∃a,tl. a::tl = l. + #A * [* #H @False_ind @H // | #a #tl #_ @(ex_intro … a) @(ex_intro … tl) //] + qed. + +lemma terminate_compare: + ∀t. Terminate ? compare t. +#t @(terminate_while … sem_comp_step) [%] +cases t // #ls * #c * // +#rs +(* we cannot proceed by structural induction on the right tape, + since compare moves the marks! *) +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) // + ] + |-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 ? 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〉::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 ?) + [

(Ht1 (\P eqc0a0) (refl …)) // + |(* a1 will be marked *) + cases (not_nil_to_exists ? (rs1@[〈a0,false〉]) ?) + [2: % #H cases (nil_to_nil … H) #_ #H1 destruct] + * #a2 #a2b * #tl2 #H7 * #a1 #a1b #rs4 #H4 #_ #Ht1 #_ + cut (a2b =false) + [lapply (memb_hd ? 〈a2,a2b〉 tl2) >H7 #mema2 + cases (memb_append … mema2) + [@H5 |#H lapply(memb_single … H) #H2 destruct %] + ] + #Ha2b >Ha2b in H7; #H7 + >(Ht1 (\P eqc0a0) … H7 (refl …)) @Hind -Hind -Ht1 -Ha2b -H2 -H3 -H5 -H6 +

length_append normalize length_append normalize <(injective_S … Hlen1) @eq_f2 // + cut (|〈a2,false〉::tl2|=|rs1@[〈a0,false〉]|) [>H7 %] + >length_append normalize (Ht1 (\Pf eqc0a0)) // + ] + ] + ] + |>(H1 Hc0) // + ] +qed. -axiom sem_compare : Realize ? compare R_compare. +lemma sem_compare : Realize ? compare R_compare. +/2/ qed.