From 5535cd4e08fd8d1e7e6e067eac1bb6c1bf8fcbbf Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 8 Aug 2012 12:09:51 +0000 Subject: [PATCH] Adding GRealize to uni_step. --- matita/matita/lib/basics/relations.ma | 5 + matita/matita/lib/turing/basic_machines.ma | 5 + matita/matita/lib/turing/if_machine.ma | 115 +++++++++ matita/matita/lib/turing/mono.ma | 15 ++ matita/matita/lib/turing/universal/copy.ma | 19 +- .../matita/lib/turing/universal/uni_step.ma | 228 +++++++++++++++--- 6 files changed, 348 insertions(+), 39 deletions(-) diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index 8b6a79be5..36b5fc2a3 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -62,6 +62,11 @@ definition inv ≝ λA.λR:relation A.λa,b.R b a. definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b). interpretation "relation inclusion" 'subseteq R S = (subR ? R S). +lemma sub_reflexive : + ∀T.∀R:relation T.R ⊆ R. +#T #R #x // +qed. + lemma sub_comp_l: ∀A.∀R,R1,R2:relation A. R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R. #A #R #R1 #R2 #Hsub #a #b * #c * /4/ diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 1c1ce3020..9790cb43c 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -192,6 +192,11 @@ lemma sem_test_char : ] qed. +lemma test_char_inv : + ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0. +#sig #P #f #t #t0 #HPt * #_ // +qed. + (************************************* swap ***********************************) definition swap_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 4) alpha. diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma index 6248ab7e7..f778ff308 100644 --- a/matita/matita/lib/turing/if_machine.ma +++ b/matita/matita/lib/turing/if_machine.ma @@ -236,6 +236,7 @@ lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc. qed. (* we can probably use acc_sem_if to prove sem_if *) +(* for sure we can use acc_sem_if_guarded to prove acc_sem_if *) lemma acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc. M1 ⊨ [acc: Rtrue, Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → ifTM sig M1 (single_finalTM … M2) M3 acc ⊨ @@ -333,3 +334,117 @@ lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc. |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ] |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ] qed. + +lemma sem_single_final_guarded: ∀sig.∀M: TM sig.∀Pre,R. + GRealize sig M Pre R → GRealize sig (single_finalTM sig M) Pre R. +#sig #M #Pre #R #HR #intape #HPre +cases (sem_seq_guarded ??????? HR (Realize_to_GRealize ?? (λt.True) ? (sem_nop …)) ?? HPre) // +#k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc +@(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop | >Houtc // ] +qed. + +lemma acc_sem_if_guarded: ∀sig,M1,M2,M3,P,P2,Rtrue,Rfalse,R2,R3,acc. + M1 ⊨ [acc: Rtrue, Rfalse] → + (GRealize ? M2 P2 R2) → (∀t,t0.P t → Rtrue t t0 → P2 t0) → + M3 ⊨ R3 → + accGRealize ? (ifTM sig M1 (single_finalTM … M2) M3 acc) + (inr … (inl … (inr … start_nop))) P (Rtrue ∘ R2) (Rfalse ∘ R3). +#sig #M1 #M2 #M3 #P #P2 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HP2 #HR3 #t #HPt +cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse +cases (true_or_false (cstate ?? outc1 == acc)) #Hacc + [lapply (sem_single_final_guarded … HR2) -HR2 #HR2 + cases (HR2 (ctape sig ? outc1) ?) + [|@HP2 [||@HMtrue @(\P Hacc)] // ] + #k2 * #outc2 * #Hloop2 #HM2 + @(ex_intro … (k1+k2)) + @(ex_intro … (lift_confR … (lift_confL … outc2))) % + [% + [@(loop_merge ????????? + (mk_config ? (states sig (ifTM sig M1 (single_finalTM … M2) M3 acc)) + (inr (states sig M1) ? (inl ? (states sig M3) (start sig (single_finalTM sig M2)))) (ctape ?? outc1) ) + ? + (loop_lift ??? + (lift_confL sig (states ? M1) (FinSum (states ? (single_finalTM … M2)) (states ? M3))) + (step sig M1) (step sig (ifTM sig M1 (single_finalTM ? M2) M3 acc)) + (λc.halt sig M1 (cstate … c)) + (λc.halt_liftL ?? (halt sig M1) (cstate … c)) + … Hloop1)) + [* * + [ #sl #tl whd in ⊢ (??%? → ?); #Hl % + | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] + |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // + |#x (config_expand ?? outc1); + whd in match (lift_confL ????); + >(trans_if_M1true_acc … Hacc) + [% | @(loop_Some ?????? Hloop1)] + |cases outc1 #s1 #t1 % + |@(loop_lift ??? + (λc.(lift_confR … (lift_confL sig (states ? (single_finalTM ? M2)) (states ? M3) c))) + … Hloop2) + [ * #s2 #t2 % + | #c0 #Hhalt >(step_if_liftM2 … Hhalt) // ] + ] + |#_ @(ex_intro … (ctape ?? outc1)) % + [@HMtrue @(\P Hacc) | >(config_expand ?? outc2) @HM2 ] + ] + |>(config_expand ?? outc2) whd in match (lift_confR ????); + * #H @False_ind @H @eq_f @eq_f >(config_expand ?? outc2) + @single_final // @(loop_Some ?????? Hloop2) + ] + |cases (HR3 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM3 + @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confR … outc2))) % + [% + [@(loop_merge ????????? + (mk_config ? (states sig (ifTM sig M1 (single_finalTM … M2) M3 acc)) + (inr (states sig M1) ? (inr (states sig (single_finalTM ? M2)) ? (start sig M3))) (ctape ?? outc1) ) + ? + (loop_lift ??? + (lift_confL sig (states ? M1) (FinSum (states ? (single_finalTM … M2)) (states ? M3))) + (step sig M1) (step sig (ifTM sig M1 (single_finalTM ? M2) M3 acc)) + (λc.halt sig M1 (cstate … c)) + (λc.halt_liftL ?? (halt sig M1) (cstate … c)) + … Hloop1)) + [* * + [ #sl #tl whd in ⊢ (??%? → ?); #Hl % + | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ] + |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // + |#x (config_expand ?? outc1); + whd in match (lift_confL ????); + >(trans_if_M1true_notacc … Hacc) + [% | @(loop_Some ?????? Hloop1)] + |cases outc1 #s1 #t1 % + |@(loop_lift ??? + (λc.(lift_confR … (lift_confR sig (states ? (single_finalTM ? M2)) (states ? M3) c))) + … Hloop2) + [ * #s2 #t2 % + | #c0 #Hhalt >(step_if_liftM3 … Hhalt) // ] + ] + |>(config_expand ?? outc2) whd in match (lift_confR ????); + #H destruct (H) + ] + |#_ @(ex_intro … (ctape ?? outc1)) % + [@HMfalse @(\Pf Hacc) | >(config_expand ?? outc2) @HM3 ] + ] + ] +qed. + +lemma acc_sem_if_app_guarded: ∀sig,M1,M2,M3,P,P2,Rtrue,Rfalse,R2,R3,R4,R5,acc. + M1 ⊨ [acc: Rtrue, Rfalse] → + (GRealize ? M2 P2 R2) → (∀t,t0.P t → Rtrue t t0 → P2 t0) → + M3 ⊨ R3 → + (∀t1,t2,t3. Rtrue t1 t3 → R2 t3 t2 → R4 t1 t2) → + (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) → + accGRealize ? (ifTM sig M1 (single_finalTM … M2) M3 acc) + (inr … (inl … (inr … start_nop))) P R4 R5 . +#sig #M1 #M2 #M3 #P #P2 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc +#HRacc #HRtrue #Hinv #HRfalse #Hsub1 #Hsub2 +#t #HPt cases (acc_sem_if_guarded … HRacc HRtrue Hinv HRfalse t HPt) +#k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc) +% [% [@Hloop + |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ] + |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ] +qed. + + diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index 32bd28c87..37ce2f2de 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -292,6 +292,21 @@ lemma WRealize_to_GRealize : ∀sig.∀M: TM sig.∀Pre,R. @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) // qed. +lemma Realize_to_GRealize : ∀sig,M.∀P,R. + M ⊨ R → GRealize sig M P R. +#alpha #M #Pre #R #HR #t #HPre +cases (HR t) -HR #k * #outc * #Hloop #HR +@(ex_intro ?? k) @(ex_intro ?? outc) % + [ @Hloop | @HR ] +qed. + +lemma acc_Realize_to_acc_GRealize: ∀sig,M.∀q:states sig M.∀P,R1,R2. + M ⊨ [q:R1,R2] → accGRealize sig M q P R1 R2. +#alpha #M #q #Pre #R1 #R2 #HR #t #HPre +cases (HR t) -HR #k * #outc * * #Hloop #HRtrue #HRfalse +@(ex_intro ?? k) @(ex_intro ?? outc) % + [ % [@Hloop] @HRtrue | @HRfalse] +qed. (******************************** monotonicity ********************************) lemma Realize_to_Realize : ∀alpha,M,R1,R2. diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma index 2367910ba..95216acdb 100644 --- a/matita/matita/lib/turing/universal/copy.ma +++ b/matita/matita/lib/turing/universal/copy.ma @@ -278,6 +278,16 @@ qed. axiom daemon : ∀P:Prop.P. +lemma list_cases2_full : + ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop. + length ? l1 = length ? l2 → + (l1 = [] → l2 = [] → P) → + (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P. +#T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl) +[ #Pnil #Pcons @Pnil // +| #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ] +qed. + lemma wsem_copy0 : WRealize ? copy0 R_copy0. #intape #k #outc #Hloop lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop @@ -299,7 +309,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop cases (Htc … Htb) -Htc #Hcbitnull #Htc % [ % #Hc' >Hc' in Hcbitnull; normalize #Hfalse destruct (Hfalse) ] cut (|l1| = |reverse ? l4|) [>length_reverse @Hlen] #Hlen1 - @(list_cases2 … Hlen1) + @(list_cases2_full … Hlen1) [ (* case l1 = [] is discriminated because l1 contains at least comma *) #Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize [ #Hl1 destruct normalize in Hcbitnull; destruct (Hcbitnull) @@ -501,7 +511,9 @@ definition option_cons ≝ λA.λa:option A.λl. [ None ⇒ l | Some a' ⇒ a'::l ]. -lemma sem_copy : Realize ? copy R_copy. + +axiom sem_copy : Realize ? copy R_copy. +(* #intape cases (sem_seq … (sem_copy0 …) (sem_seq … (sem_move_l …) @@ -577,4 +589,5 @@ lapply (Hte (reverse ? (reverse ? l1@〈s1,false〉::l2)@[〈c1,false〉]) >reverse_append >reverse_append >reverse_single >reverse_cons >reverse_append >reverse_append >reverse_reverse >reverse_reverse >reverse_single >associative_append >associative_append % -qed. \ No newline at end of file +qed. +*) \ No newline at end of file diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index fc663ff2c..4761ce135 100644 --- a/matita/matita/lib/turing/universal/uni_step.ma +++ b/matita/matita/lib/turing/universal/uni_step.ma @@ -78,19 +78,19 @@ cases (sem_seq ????? (sem_mark ?) @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop #ls #l #rs #c #d #Hnogrids #Hnomarks #Hintape cases HR -HR -#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta -* #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb -Hta +#ta * whd in ⊢ (%→?); * #Hta #_ lapply (Hta … Hintape) -Hta -Hintape #Hta +* #tb * whd in ⊢ (%→?); * #_ #Htb cases (Htb … Hta) -Htb -Hta [* #Hgridc @False_ind @(absurd … Hgridc) @eqnot_to_noteq @(Hnogrids 〈c,false〉) @memb_hd ] -* #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) +* * #Hgrdic #Htb #_ lapply (Htb l 〈grid,false〉 (〈bar,false〉::〈d,false〉::rs) (refl …) (refl …) ?) [#x #membl @Hnogrids @memb_cons @membl] -Htb #Htb -* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb #Htc -* #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc #Htd -* #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd #Hte -* #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf -whd in ⊢ (%→?); #Htg cases (Htg … Htf) -Htg -Htf - [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)] -* #_ #Htg lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) +* #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb #Htc +* #td * whd in ⊢ (%→?); * #_ #Htd lapply (Htd … Htc) -Htd -Htc #Htd +* #te * whd in ⊢ (%→?); * #Hte #_ lapply (Hte … Htd) -Hte -Htd #Hte +* #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Htf -Hte #Htf +whd in ⊢ (%→?); * #_ #Htg cases (Htg … Htf) -Htg -Htf +#_ #Htg cases (Htg (refl …)) -Htg #Htg #_ +lapply (Htg (〈grid,false〉::reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?) [#x #membl @Hnomarks @daemon] -Htg #Htg >Htg >reverse_cons >reverse_reverse >associative_append % qed. @@ -134,21 +134,22 @@ cases (sem_seq ????? sem_init_current_on_match #l1 #l2 #c #ls #d #rs #Hl1marks #Hl1grids #Hl2marks #Hc #Hintape cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hl1grids Hc Hintape) -Hta -Hintape #Hta -* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta +* #tb * whd in ⊢ (%→?); * #_ #Htb lapply (Htb … Hta) -Htb -Hta generalize in match Hl1marks; -Hl1marks cases (list_last ? l1) [#eql1 >eql1 #Hl1marks whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); #Htb - * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb * + * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb * [* whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)] - * #_ #Htc lapply (Htc … (refl …) (refl …) ?) + * * #_ #Htc #_ lapply (Htc … (refl …) (refl …) ?) [#x #membx @Hl2marks @membx] - #Htc whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc + #Htc whd in ⊢ (%→?); * #Houtc #_ cases (Houtc (reverse ? l2@〈grid,false〉::〈c,true〉::〈grid,false〉::ls) comma) + -Houtc #Houtc lapply (Houtc … Htc) -Houtc -Htc #Houtc #_ >Houtc % |* #c1 * #tl #eql1 >eql1 #Hl1marks >reverse_append >reverse_single whd in ⊢ ((???%)→?); whd in ⊢ ((???(????%))→?); >associative_append whd in ⊢ ((???(????%))→?); #Htb - * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb * + * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc -Htb * [* >Hl1marks [#Htemp destruct (Htemp)] @memb_append_l2 @memb_hd] - * #_ >append_cons append_cons Houtc >reverse_append >reverse_append >reverse_single >reverse_reverse >associative_append >associative_append >associative_append % @@ -338,7 +341,7 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 | #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Hta ????????) -Htb [9:|*:(* bit_or_null c0,c1; |curconfig| = |newconfig|*) @daemon ] - #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc + #Htb * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc whd in ⊢ (%→?); #Houtc whd in Htc:(???%); whd in Htc:(???(??%%%)); lapply (Houtc rs n (〈comma,false〉::〈c1,false〉::reverse ? newconfig@〈s1,false〉::〈comma,false〉::reverse ? table1) @@ -475,13 +478,164 @@ definition R_uni_step_true ≝ λt1,t2. definition R_uni_step_false ≝ λt1,t2. ∀b. current STape t1 = Some ? 〈bit b,false〉 → b = true ∧ t2 = t1. -axiom sem_match_tuple : Realize ? match_tuple R_match_tuple. +(*axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.*) definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))). +definition Pre_uni_step ≝ λt1. + ∃n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv. + 0 < |table| ∧ table_TM (S n) table ∧ + match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉 + (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 table ∧ + legal_tape ls 〈c0,false〉 rs ∧ + t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 + (curconfig@〈c0,false〉::〈grid,false〉::table@〈grid,false〉::rs). + lemma sem_uni_step : - accRealize ? uni_step us_acc + accGRealize ? uni_step us_acc Pre_uni_step R_uni_step_true R_uni_step_false. +@(acc_sem_if_app_guarded STape … (sem_test_char ? (λc:STape.\fst c == bit false)) + ? (test_char_inv …) (sem_nop …) …) +[| @(sem_seq_app_guarded … (Realize_to_GRealize … sem_init_match) ???) + [ 5: @sub_reflexive + | 3: @(sem_seq_app_guarded … sem_match_tuple + (Realize_to_GRealize … (sem_if ????????? (sem_test_char … (λc.¬is_marked FSUnialpha c)) + (sem_seq … sem_exec_action (sem_move_r …)) + (sem_nop …)))) + [@(λx.True) + |// + |@sub_reflexive] + ||| #t1 #t2 * #n * #table * #s0 * #s1 * #c0 * #c1 * #ls * #rs * #curconfig + * #newconfig * #mv * * * * + #Hlen1 #Htable #Hmatch #Hlegal #Ht1 + whd in ⊢ (%→?); + cut (∃tup,table0.table = tup@table0 ∧ tuple_TM (S n) tup) + [@daemon] + * #tup * #table0 * #Htableeq * #qin * #cin * #qout * #cout * #mv0 + * * * * * * * * * * + #Hqinnomarks #_ #Hqinbits #_ #_ #_ #_ #_ #Hqinlen #_ #Htupeq + cut (∃d,qin0.qin = 〈d,false〉::qin0) + [ lapply Hqinlen lapply Hqinnomarks -Hqinlen -Hqinnomarks cases qin + [ #_ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) + | * #d #bd #qin0 #Hqinnomarks #_ %{d} %{qin0} + >(?:bd=false) [%] + @(Hqinnomarks 〈d,bd〉) @memb_hd ] ] + * #d * #qin0 #Hqineq + #Ht2 + lapply (Ht2 (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) + (qin0@〈cin,false〉::〈comma,false〉::qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0@〈grid,false〉::rs) s0 d ???) + [ >Ht1 @eq_f >associative_append @eq_f @eq_f @eq_f + >Htableeq >Htupeq >associative_append whd in ⊢ (??%?); + @eq_f >Hqineq >associative_append @eq_f whd in ⊢ (??%?); + @eq_f whd in ⊢ (??%?); @eq_f + >associative_append % + | @daemon + | @daemon + ] + #Ht2 % [| % [| % [| % [ @Ht2 ] + %2 + (* ls0 = ls + c = s0 + l1 = curconfig@[〈c0,false〉] + l2 = [〈bar,false〉] + c10 = d + l3 = qin0@[〈cin,false〉] + l4 = qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0 + rs00 = rs + n0 = S n ? + *) + %{ls} %{s0} %{(curconfig@[〈c0,false〉])} + %{([〈bar,false〉])} %{d} %{(qin0@[〈cin,false〉])} + %{(qout@〈cout,false〉::〈comma,false〉::〈mv0,false〉::table0)} + %{rs} %{n} @daemon (* TODO *) + ] + ] + ] + ] + | #intape #outtape + #ta whd in ⊢ (%→?); #Hta #HR + #n #fulltable #s0 #s1 #c0 #c1 #ls #rs #curconfig #newconfig #mv + #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon] + * #t0 * #table #Hfulltable >Hfulltable -fulltable + #Htable #Hmatch #Htape #Hintape #t1' #Ht1' + >Hintape in Hta; * * * #c #bc * + whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)] + cases HR -HR + #tb * whd in ⊢ (%→?); #Htb + lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???) + [ >Hta >associative_append % + | @daemon + | @daemon + | -Hta -Htb #Htb * + #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc + [| * #Hcurrent #Hfalse @False_ind + (* absurd by Hmatch *) @daemon + | >(\P Hc) % + | (* Htable (con lemma) *) @daemon + | (* Hmatch *) @daemon + | (* Htable *) @daemon + | (* Htable, Hmatch → |config| = n + necessaria modifica in R_match_tuple, le dimensioni non corrispondono + *) @daemon + ] + * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc * + [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2) + #_ #Htd + cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc + >Hnewc cut (mv1 = 〈mv,false〉) + [@daemon] #Hmv1 + * #te * whd in ⊢ (%→?); #Hte + cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls) + 〈grid,false〉 + ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: + newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs)) + [ >Htd @eq_f3 // + [ >reverse_append >reverse_single % + | >associative_append >associative_append normalize + >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f + whd in ⊢ (??%?); >associative_append % + ] + ] + -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte + [ // + | (*|curconfig| = |newconfig|*) @daemon + | (* Htable → bit_or_null c1 = true *) @daemon + | (* only_bits (〈s1,false〉::newconfig) *) @daemon + | (* only_bits (curconfig@[〈s0,false〉]) *) @daemon + | (* no_marks (reverse ? curconfig) *) @daemon + | >Hmv1 in Htableeq; >Hnewc + >associative_append >associative_append normalize + >associative_append >associative_append + #Htableeq Houttape @eq_f @eq_f @eq_f @eq_f + change with ((〈bar,false〉::〈t0,false〉::table)@?) in ⊢ (???%); + >Htableeq >associative_append >associative_append + >associative_append normalize >associative_append + >associative_append normalize >Hnewc associative_append normalize >associative_append + >Hmv1 % + | @Hliftte + ] + | // + ] + ] + ] + | * #td * whd in ⊢ (%→%→?); >Htc * #Htd + lapply (Htd ? (refl ??)) normalize in ⊢ (%→?); + #Hfalse destruct (Hfalse) + ] + ] +| #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2 + #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' % + // cases b in Hb'; normalize #H1 // +] +qed. + +(* @(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false)) (sem_seq … sem_init_match (sem_seq … sem_match_tuple @@ -497,11 +651,11 @@ lemma sem_uni_step : #Htable_len cut (∃t0,table. fulltable =〈bar,false〉::〈t0,false〉::table) [(* 0 < |table| *) @daemon] * #t0 * #table #Hfulltable >Hfulltable -fulltable #Htable #Hmatch #Htape #Hintape #t1' #Ht1' - >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta - #Hs0 lapply (\P Hs0) -Hs0 #Hs0 #Hta % // + >Hintape in Hta; * * * #c #bc * + whd in ⊢ (??%?→?); #HSome destruct (HSome) #Hc #Hta % [@(\P Hc)] cases HR -HR #tb * whd in ⊢ (%→?); #Htb - lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) s0 t0 ???) + lapply (Htb (〈grid,false〉::ls) (curconfig@[〈c0,false〉]) (table@〈grid,false〉::rs) c t0 ???) [ >Hta >associative_append % | @daemon | @daemon @@ -509,7 +663,7 @@ lemma sem_uni_step : #tc * whd in ⊢ (%→?); #Htc cases (Htc … Htable … Htb) -Htb -Htc [| * #Hcurrent #Hfalse @False_ind (* absurd by Hmatch *) @daemon - | >Hs0 % + | >(\P Hc) % | (* Htable (con lemma) *) @daemon | (* Hmatch *) @daemon | (* Htable *) @daemon @@ -518,20 +672,21 @@ lemma sem_uni_step : *) @daemon ] * #table1 * #newc * #mv1 * #table2 * #Htableeq #Htc * - [ * #td * whd in ⊢ (%→?); >Htc -Htc #Htd - cases (Htd ? (refl ??)) #_ -Htd + [ * #td * whd in ⊢ (%→?); >Htc -Htc * * #c2 * whd in ⊢ (??%?→?); #Hc2 destruct (Hc2) + #_ #Htd cut (newc = 〈s1,false〉::newconfig@[〈c1,false〉]) [@daemon] #Hnewc - >Hnewc #Htd cut (mv1 = 〈mv,false〉) + >Hnewc cut (mv1 = 〈mv,false〉) [@daemon] #Hmv1 * #te * whd in ⊢ (%→?); #Hte - cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈s0,false〉::〈grid,false〉::ls) + cut (td = midtape STape (〈c0,false〉::reverse STape curconfig@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 - ((table1@〈bar,false〉::〈s0,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: + ((table1@〈bar,false〉::〈c,false〉::curconfig@[〈c0,false〉])@〈comma,true〉::〈s1,false〉:: newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs)) [ >Htd @eq_f3 // [ >reverse_append >reverse_single % | >associative_append >associative_append normalize - >associative_append >associative_append >Hmv1 % + >associative_append >Hmv1 >Hnewc @eq_f @eq_f @eq_f @eq_f @eq_f @eq_f + whd in ⊢ (??%?); >associative_append % ] ] -Htd #Htd lapply (Hte … (S n) … Htd … Ht1') -Htd -Hte @@ -546,7 +701,7 @@ lemma sem_uni_step : >associative_append >associative_append #Htableeq Houttape @eq_f @eq_f @eq_f @eq_f @@ -562,13 +717,14 @@ lemma sem_uni_step : ] ] ] - | * #td * whd in ⊢ (%→%→?); >Htc #Htd - cases (Htd ? (refl ??)) normalize in ⊢ (%→?); + | * #td * whd in ⊢ (%→%→?); >Htc * #Htd + lapply (Htd ? (refl ??)) normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] ] | #t1 #t2 #t3 whd in ⊢ (%→%→?); #Ht1 #Ht2 - #b #Hb cases (Ht1 ? Hb) #Hb' #Ht3 >Ht2 % // - cases b in Hb'; normalize #H1 // + #b #Hb >Hb in Ht1; * #Hc #Ht1 lapply (Hc ? (refl ??)) -Hc #Hb' % + // cases b in Hb'; normalize #H1 // ] -qed. \ No newline at end of file +qed. +*) \ No newline at end of file -- 2.39.2