From: Wilmer Ricciotti Date: Wed, 6 Nov 2013 17:20:18 +0000 (+0000) Subject: Full rework of the semantics of the binary machine (now completely working X-Git-Tag: make_still_working~1050 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a47f3e553f17690908dfcacfdfa58c0da378a9b;p=helm.git Full rework of the semantics of the binary machine (now completely working up to arithmetical proofs) --- diff --git a/matita/matita/lib/turing/multi_universal/binaryTM.ma b/matita/matita/lib/turing/multi_universal/binaryTM.ma index f2af60587..410c32716 100644 --- a/matita/matita/lib/turing/multi_universal/binaryTM.ma +++ b/matita/matita/lib/turing/multi_universal/binaryTM.ma @@ -58,7 +58,18 @@ lemma le_displ_of_move : ∀sig,mv.displ_of_move sig mv ≤ S (2*FS_crd sig). #sig * /2 by le_S/ qed. -(* controllare i contatori, molti andranno incrementati di uno *) +definition displ2_of_move ≝ λsig,mv. + match mv with + [ L ⇒ FS_crd sig + | N ⇒ O + | R ⇒ O ]. + +lemma le_displ2_of_move : ∀sig,mv.displ2_of_move sig mv ≤ S (2*FS_crd sig). +#sig * /2 by lt_to_le/ +qed. + +definition mv_tech ≝ λmv.match mv with [ N ⇒ N | _ ⇒ R ]. + definition trans_binaryTM : ∀sig,states:FinSet. (states × (option sig) → states × (option sig) × move) → ((states_binaryTM sig states) × (option bool) → @@ -79,7 +90,7 @@ definition trans_binaryTM : ∀sig,states:FinSet. | None ⇒ (* Overflow position! *) let 〈s',a',mv〉 ≝ trans 〈s0,None ?〉 in match a' with - [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,bin2,None ?,to_initN 0 ? H1〉,None ?,N〉 + [ None ⇒ (* we don't write anything: go to end of 3 *) 〈〈s',bin3,None ?,to_initN (displ2_of_move sig mv) ??〉,None ?,mv_tech mv〉 | Some _ ⇒ (* maybe extend tape *) 〈〈s0,bin4,None ?,to_initN O ? H1〉,None ?,R〉 ] ] ] | S phase ⇒ match phase with [ O ⇒ (*** PHASE 1: restart ***) @@ -115,7 +126,7 @@ definition trans_binaryTM : ∀sig,states:FinSet. match pi1 … count with [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,R〉 | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]]. -[2,3: /2 by lt_S_to_lt/] /2 by le_S_S/ +[ /2 by le_to_lt_to_lt/ | /2 by le_S_S/ |*: /2 by lt_S_to_lt/] qed. definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝ @@ -155,10 +166,6 @@ let c' ≝ option_hd ? (opt_bin_char sig (current ? t)) in let rs' ≝ (tail ? (opt_bin_char sig (current ? t))@bin_list ? (right ? t)) in mk_tape ? ls' c' rs'. -definition R_bin_lift ≝ λsig,R,t1,t2. - ∃u1.t1 = tape_bin_lift sig u1 → - ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2. - definition state_bin_lift : ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M) ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉./2 by lt_S_to_lt/ qed. @@ -173,12 +180,12 @@ lemma binaryTM_bin0_bin1 : = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. // qed. -lemma binaryTM_bin0_bin2 : +lemma binaryTM_bin0_bin3 : ∀sig,M,t,q,ch,k,qn,mv. current ? t = None ? → S k Hcur Hk0 >minus_tech +#sig #M #t #q #ls #a #rs #ch #Hhalt #Ht #k #Hk +cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(minus_tech (S (FS_crd sig))) cut (∃c,cl.bin_char sig a = c::cl) [@daemon] * #c * #cl #Ha >Ha cut (FS_crd sig = |bin_char sig a|) [@daemon] #Hlen @(trans_eq ?? (loopM ? (mk_binaryTM ? M) (S (|c::cl|) + k0) @@ -306,37 +314,39 @@ cut (FS_crd sig = |bin_char sig a|) [@daemon] #Hlen qed. lemma binaryTM_phase0_None_None : - ∀sig,M,t,q,ch,k,n,qn,mv. - O < n → n < 2*FS_crd sig → O < k → + ∀sig,M,t,q,ch,n,qn,mv. + O < n → n < 2*FS_crd sig → halt sig M q=false → current ? t = None ? → 〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 → + ∀k.O < k → loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t) = loopM ? (mk_binaryTM sig M) (k-1) - (mk_config ?? (〈q,bin2,None ?,to_initN O ??〉) t). [2,3: /2 by transitive_lt/ ] -#sig #M #t #q #ch #k #n #qn #mv #HOn #Hn #Hk #Hhalt + (mk_config ?? (〈qn,bin3,None ?,to_initN (displ2_of_move sig mv) ??〉) (tape_move ? t (mv_tech mv))). [| @le_S @le_S //|@le_S_S @le_displ2_of_move] +#sig #M #t #q #ch #n #qn #mv #HOn #Hn #Hhalt #Hcur #Htrans #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0) -cases t -[ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/ -| #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/ -| #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/ +lapply Htrans lapply Hcur -Htrans -Hcur cases t +[ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 // +| #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 // +| #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 // | #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ] qed. lemma binaryTM_phase0_None_Some : - ∀sig,M,t,q,ch,k,n,qn,chn,mv. - O < n → n < 2*FS_crd sig → O < k → + ∀sig,M,t,q,ch,n,qn,chn,mv. + O < n → n < 2*FS_crd sig → halt sig M q=false → current ? t = None ? → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,None ?〉 → + ∀k.O < k → loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t) = loopM ? (mk_binaryTM sig M) (k-1) (mk_config ?? (〈q,bin4,None ?,to_initN O ??〉) (tape_move ? t R)). [2,3: /2 by transitive_lt/ ] -#sig #M #t #q #ch #k #n #qn #chn #mv #HOn #Hn #Hk #Hhalt +#sig #M #t #q #ch #n #qn #chn #mv #HOn #Hn #Hhalt #Hcur #Htrans #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0) -cases t +lapply Htrans lapply Hcur -Hcur -Htrans cases t [ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/ | #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/ | #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/ @@ -358,8 +368,9 @@ lemma binaryTM_bin1_S : qed. lemma binaryTM_phase1 : - ∀sig,M,q,ls1,ls2,cur,rs,ch,k. - S (FS_crd sig) ≤ k → |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) → + ∀sig,M,q,ls1,ls2,cur,rs,ch. + |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) → + ∀k.S (FS_crd sig) ≤ k → loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin1,ch,FS_crd sig〉) (mk_tape ? (ls1@ls2) cur rs)) = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig)) @@ -407,8 +418,8 @@ cut (∀sig,M,q,ls1,ls2,ch,k,n,cur,rs. ] >reverse_cons >associative_append % ] -| #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #k #Hk #Hlen - cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @Hcut // ] +| #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #Hlen #Hcur #k #Hk + cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @Hcut /2/ ] qed. lemma binaryTM_bin2_O : @@ -445,26 +456,28 @@ qed. let rec iter (T:Type[0]) f n (t:T) on n ≝ match n with [ O ⇒ t | S n0 ⇒ iter T f n0 (f t) ]. -lemma binaryTM_phase2_None :∀sig,M,q,ch,qn,mv,k,n. S n ≤ k → - ∀t.n≤S (2*FS_crd sig) → +lemma binaryTM_phase2_None :∀sig,M,q,ch,qn,mv. 〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 → + ∀n.n≤S (2*FS_crd sig) → + ∀t,k.S n ≤ k → loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin2,ch,n〉) t) = loopM ? (mk_binaryTM sig M) (k - S n) (mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉) (iter ? (λt0.tape_move ? t0 R) n t)). [2,3: @le_S_S /2 by lt_S_to_lt/] -#sig #M #q #ch #qn #mv #k #n #Hk -cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech +#sig #M #q #ch #qn #mv #Htrans #n #Hn #t #k #Hk +cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech lapply Hn lapply t -Hn -t elim n -[ #t #Hle #Htrans >loopM_unfold >loop_S_false // +[ #t #Hle >loopM_unfold >loop_S_false // >(binaryTM_bin2_O … Htrans) // -| #n0 #IH #t #Hn0 #Htrans >loopM_unfold >loop_S_false // +| #n0 #IH #t #Hn0 >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) @(trans_eq ???? (IH …)) // ] qed. -lemma binaryTM_phase2_Some_of : ∀sig,M,q,ch,qn,chn,mv,ls,k. - S (FS_crd sig) ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 → +lemma binaryTM_phase2_Some_of : ∀sig,M,q,ch,qn,chn,mv,ls. + 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 → + ∀k.S (FS_crd sig) ≤ k → loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin2,ch,FS_crd sig〉) (mk_tape ? ls (None ?) [ ])) = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig)) @@ -512,11 +525,11 @@ cut (∀sig,M,q,ch,qn,chn,mv,ls,k,n. cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0) [@daemon] -Hbinchar #Hbinchar >Hbinchar @(trans_eq ???? (IH …)) // [ %{fs0} >reverse_cons >associative_append @Hbinchar - | whd in ⊢ (??%?); /2 by / ] + | whd in ⊢ (??%?); Hk0 >minus_tech @trans_eq [3: @(trans_eq ???? (Hcut ??????? ls ?? cs Htrans [ ] …)) // [ normalize % // | normalize @Hcrd | >Hcrd // ] @@ -591,18 +605,20 @@ lemma binaryTM_bin3_S : #sig #M #t #q #ch #k #HSk % qed. -lemma binaryTM_phase3 :∀sig,M,q,ch,k,n. - S n ≤ k → n ≤ S (2*FS_crd sig) → - ∀t.loopM ? (mk_binaryTM sig M) k +lemma binaryTM_phase3 :∀sig,M,q,ch,n. + n ≤ S (2*FS_crd sig) → + ∀t,k.S n ≤ k → + loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin3,ch,n〉) t) = loopM ? (mk_binaryTM sig M) (k - S n) (mk_config ?? (〈q,bin0,None ?,FS_crd sig〉) (iter ? (λt0.tape_move ? t0 L) n t)). [2,3: /2 by lt_S_to_lt, le_to_lt_to_lt/] -#sig #M #q #ch #k #n #Hk -cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech elim n -[ #Hcrd #t >loopM_unfold >loop_S_false [| % ] >binaryTM_bin3_O // -| #n0 #IH #Hlt #t >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S [|//] - Hk0 >(minus_tech (S n) k0) +lapply t lapply Hcrd -t -Hcrd elim n +[ #Hcrd #t >loopM_unfold >loop_S_false [| % ] >binaryTM_bin3_O // +| #n0 #IH #Hlt #t >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S [|@Hlt] + Hcur % qed. -lemma binaryTM_phase4_write : ∀sig,M,q,ch,k,t. - O < k → current ? t = None ? → +lemma binaryTM_phase4_write : ∀sig,M,q,ch,t.current ? t = None ? → + ∀k.O < k → loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin4,ch,O〉) t) = loopM ? (mk_binaryTM sig M) (k-1) - (mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t). [2,3: @le_S //] -#sig #M #q #ch #k #t #Hk #Hcur + (mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t). [|@le_S_S @le_O_n|@le_S_S //] +#sig #M #q #ch #t #Hcur #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech ->loopM_unfold >loop_S_false // binaryTM_bin4_None // +>loopM_unfold >loop_S_false // binaryTM_bin4_None [|//] % qed. (* we don't get here any more! * @@ -649,16 +665,16 @@ whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?); whd in match (trans FinBool ??); Hk0 >minus_tech ->loopM_unfold >loop_S_false // binaryTM_bin4_extend // +>loopM_unfold >loop_S_false // (binaryTM_bin4_extend … Hcur) [|*://] % qed. lemma binaryTM_bin5_O : @@ -677,23 +693,23 @@ qed. (* extends the tape towards the left with an unimportant sequence that will be immediately overwritten *) -lemma binaryTM_phase5 :∀sig,M,q,ch,k,n. S n ≤ k → +lemma binaryTM_phase5 :∀sig,M,q,ch,n. ∀rs.nHk0 >minus_tech -elim n -[ #rs #Hlt %{[]} % // cases rs // -| #n0 #IH #rs #Hn0 cases (IH (false::rs) ?) [|/2 by lt_S_to_lt/] - #bs * #Hbs -IH #IH - %{(bs@[false])} % [ length_append /2 by increasing_to_injective/ ] +#sig #M #q #ch #n elim n +[ #rs #Hlt %{[]} % // #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech -Hk0 + cases rs // +| #n0 #IH #rs #Hn0 cases (IH (false::rs) ?) [|/2 by lt_S_to_lt/] + #bs * #Hbs -IH #IH %{(bs@[false])} % [ length_append /2 by increasing_to_injective/ ] + #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >loopM_unfold >loop_S_false // >binaryTM_bin5_S - >associative_append normalize in match ([false]@?); associative_append normalize in match ([false]@?); <(IH (S n0 + k0)) [|//] >loopM_unfold @eq_f @eq_f cases rs // ] qed. @@ -737,6 +753,8 @@ lemma iter_split : ∀T,f,m,n,x. #n0 #IH #x IH % qed. +lemma iter_O : ∀T,f,x.iter T f O x = x.// qed. + lemma iter_tape_move_R : ∀T,n,ls,cs,rs.|cs| = n → iter ? (λt0.tape_move T t0 R) n (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs))) = mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs). @@ -760,19 +778,25 @@ lemma hd_tech : ∀T,l1,l2.O < |l1| → option_hd T (l1@l2) = option_hd ? l1. #T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/ qed. -lemma iter_tape_move_l_nil : ∀T,n,rs. +lemma iter_tape_move_L_nil : ∀T,n,rs. iter ? (λt0.tape_move T t0 L) n (mk_tape ? [ ] (None ?) rs) = mk_tape ? [ ] (None ?) rs. #T #n #rs elim n // #n0 #IH loopM_unfold + ∀sig,M,i,tf,qf. O < FS_crd sig → + ∀t,q.∃k.i ≤ k ∧ + ((loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) → + loopM ? (mk_binaryTM sig M) k + (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = + Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf))) ∧ + (loopM sig M i (mk_config ?? q t) = None ? → + loopM ? (mk_binaryTM sig M) k + (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = None ?)). +#sig #M #i #tf #qf #Hcrd elim i +[ #t #q %{O} % // % // change with (None ?) in ⊢ (??%?→?); #H destruct (H) +| -i #i #IH #t #q >loopM_unfold lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t)))) cases (halt ?? q) in ⊢ (???%→?); #Hhalt - [ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) - #H destruct (H) %{1} >loopM_unfold >loop_S_true // ] - (* interesting case: more than one step *) - >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) - (config_expand ?? (step ???)) #Hloop - lapply (IH … Hloop) [@Hcrd] -IH * #k0 #IH state_bin_lift_unfold cases (current_None_or_midtape ? t) - (* 0.1) current = None *) - [ (* #Hcur >state_bin_lift_unfold in ⊢ (??%?); - lapply (current_tape_bin_list … Hcur) #Hcur' - >binaryTM_phase0_None /2 by monotonic_lt_plus_l/ - >(?: FS_crd sig + k0 = S (FS_crd sig + k0 - 1)) [|@daemon] - >loopM_unfold >loop_S_false // lapply (refl ? t) cases t in ⊢ (???%→?); - [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H) normalize in Hcur; destruct (Hcur) - | #Ht >Ht >binaryTM_bin4_None // Ht >tape_bin_lift_unfold - >left_midtape >current_midtape >right_midtape >opt_bin_char_Some - >(binaryTM_phase0_midtape … Hhalt ? (refl ??)) [| // ] - >(?: 7*S (FS_crd sig) + k0 - S (FS_crd sig) = 6*S (FS_crd sig) + k0) [|/2 by plus_minus/] - (*** PHASE 1 ***) - >binaryTM_phase1 - [| cases (bin_list ? rs) normalize // #r0 #rs0 #H destruct (H) - | >length_reverse @daemon - | // ] - >(?:6*S (FS_crd sig) + k0 - S (FS_crd sig) = 5*S (FS_crd sig) + k0) [|/2 by plus_minus/] - >reverse_reverse >opt_cons_hd_tl + [ %{(S i)} % // + >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) % + [| #H destruct (H)] + #H destruct (H) >loopM_unfold >loop_S_true // ] + (* interesting case: more than one step *) + >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)cases (current_None_or_midtape ? t) + (*** current = None ***) + [ #Hcur lapply (current_tape_bin_list … Hcur) #Hcur' + cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,None ?〉) + [ cases (trans ? M 〈q,None ?〉) * #qn #chn #mv /4 by ex_intro/ ] + * #qn * #chn * #mv cases chn -chn + [ #Htrans lapply (binaryTM_phase0_None_None … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/] + lapply (binaryTM_phase3 ? M qn (None ?) (displ2_of_move sig mv) ? (tape_move FinBool (tape_bin_lift sig t) (mv_tech mv))) [//] + cases (IH (tape_move ? t mv) qn) -IH #k0 * #Hk0 * #IH #IHNone + #phase3 #phase0 %{(S (S (displ2_of_move sig mv))+k0)} % + [ @le_S_S @(le_plus O) // ] + >state_bin_lift_unfold >phase0 [|//] + >phase3 [|//] + >(?: S (S (displ2_of_move sig mv))+k0-1-S (displ2_of_move sig mv) = k0) + [| /2 by refl, plus_to_minus/ ] + cut (tape_move sig t mv=tape_move sig (tape_write sig t (None sig)) mv) [%] #Hcut + >(?: iter ? (λt0.tape_move ? t0 L) (displ2_of_move sig mv) (tape_move ? (tape_bin_lift ? t) (mv_tech mv)) + =tape_bin_lift ? (tape_move ? t mv)) + [|cases t in Hcur; + [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H) + | #_ whd in match (tape_bin_lift ??); + (* TODO *) + (* ∀mv.tape_move ? (niltape ?) mv = niltape ? *) + (* ∀n.iter ? (λt.tape_move ? t ?) n (niltape ?) = niltape ? *) + @daemon + | #r0 #rs0 #_ cases mv + [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L); + whd in match (rev_bin_list ??); whd in match (option_hd ??); + whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] + (* TODO *) + (* tape_move (mk_tape [ ] (None ?) rs R = ... *) + (* use iter_tape_move_R *) + @daemon + | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R); + whd in match (rev_bin_list ??); whd in match (option_hd ??); + whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] + whd in match (tape_move ? (leftof ???) R); + >tape_bin_lift_unfold >left_midtape >opt_bin_char_Some >right_midtape + >iter_O + (* TODO *) + (* tape_move (mk_tape [ ] (None ?) rs R = ... *) + @daemon + | >tape_bin_lift_unfold % ] + | #l0 #ls0 #_ cases mv + [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L); + whd in match (bin_list ??); >append_nil whd in match (option_hd ??); + whd in match (left ??); whd in match (tail ??); + whd in match (tape_move ? (rightof ???) L); + >(?: rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%] + (* TODO *) + (* tape_move (mk_tape ls (None ?) [ ] R = ... *) + (* use iter_tape_move_L *) + @daemon + | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R); + whd in match (bin_list ??); >append_nil whd in match (option_hd ??); + whd in match (left ??); whd in match (tail ??); >iter_O cases (rev_bin_list ??) // + | >tape_bin_lift_unfold % ] + ] + ] + % + [ #Hloop @IH Hcur Hcur tape_bin_lift_unfold whd in match (option_hd ??); whd in match (tail ??); + whd in match (right ??); + >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] + >Hbs % ] + cases (binaryTM_phase5 ? M q (None ?) (FS_crd sig) (bin_list ? (r0::rs0)) ?) [|//] + #cs * #Hcs + lapply (binaryTM_phase2_Some_ow ?? q (None ?) … [ ] ? (bin_list ? (r0::rs0)) Htrans Hcs) + lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ? + (mk_tape FinBool (reverse bool (bin_char sig chn)@[]) + (option_hd FinBool (bin_list sig (r0::rs0))) (tail FinBool (bin_list sig (r0::rs0))))) [//] + cases (IH (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone + #phase3 #phase2 #phase5 #phase4 #phase0 + %{(1 + 1 + (S (FS_crd sig)) + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} % + [ @le_S_S @(le_plus O) // ] + >state_bin_lift_unfold >phase0 [|//] + >phase4 [|//] + >(?: loopM ? (mk_binaryTM ??) ? (mk_config ?? 〈q,bin5,None ?,to_initN ???〉 ?) = ?) + [|| @(trans_eq ????? (phase5 ??)) + [ @eq_f @eq_f + >tape_bin_lift_unfold whd in match (rev_bin_list ??); + whd in match (right ??); whd in match (bin_list ??); + cases (bin_char ? r0) // (* bin_char can't be nil *) @daemon + | @le_S_S >associative_plus >associative_plus >commutative_plus @(le_plus O) // + |]] + >phase2 [| (*arith*) @daemon ] + >phase3 [| (*arith*) @daemon ] + >(?: 1+1+S (FS_crd sig)+S (FS_crd sig)+S (displ_of_move sig mv)+k0-1-1 + -S (FS_crd sig)-S (FS_crd sig) -S (displ_of_move sig mv) = k0) + [| (*arith*) @daemon ] + -phase0 -phase2 -phase3 -phase4 -phase5 (?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv) + (mk_tape ? (reverse ? (bin_char sig chn)@[]) + (option_hd FinBool (bin_list sig (r0::rs0))) + (tail FinBool (bin_list sig (r0::rs0)))) + = tape_bin_lift ? (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv)) + [ % #Hloop + [ @IH (?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] + cases mv + [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //] + >iter_split >iter_tape_move_L [| @daemon ] + >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//] + whd in match (tape_move ???); >tape_bin_lift_unfold % + | normalize in match (displ_of_move ??); >iter_O + normalize in match (tape_move ???); + >tape_bin_lift_unfold >opt_bin_char_Some + >hd_tech [|@daemon] >tail_tech [| @daemon ] % + | normalize in match (displ_of_move ??); + >iter_tape_move_L [|@daemon] + normalize in match (tape_move ???); >tape_bin_lift_unfold + >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ] + ] + | #_ lapply (binaryTM_phase4_write ? M q (None ?) (niltape ?) (refl ??)) + lapply (binaryTM_phase2_Some_of ?? q (None ?) … [ ] Htrans) + lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ? + (mk_tape FinBool (reverse bool (bin_char sig chn)@[]) (None ?) [ ])) [//] + cases (IH (tape_move ? (midtape ? [ ] chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone + #phase3 #phase2 #phase4 #phase0 + %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} % + [ @le_S_S @(le_plus O) // ] + >state_bin_lift_unfold >phase0 [|//] + >phase4 [|//] + >phase2 [|(*arith *) @daemon] + >phase3 [| (*arith*) @daemon ] + >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1 + -S (FS_crd sig)-S (displ_of_move sig mv) = k0) + [| (*arith*) @daemon ] + -phase0 -phase2 -phase3 -phase4 (?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv) + (mk_tape ? (reverse ? (bin_char sig chn)@[]) (None ?) [ ]) + = tape_bin_lift ? (tape_move ? (tape_write ? (niltape ?) (Some ? chn)) mv)) + [ % #Hloop + [ @IH (?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //] + >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?); + >iter_tape_move_L [| @daemon ] + >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon] + >iter_tape_move_L_left [|//] + normalize in match (tape_move ???); + >tape_bin_lift_unfold % + | normalize in match (displ_of_move ??); >iter_O + normalize in match (tape_move ???); + >tape_bin_lift_unfold % + | normalize in match (displ_of_move ??); + change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?); + >iter_tape_move_L [|@daemon] + normalize in match (tape_move ???); >tape_bin_lift_unfold + >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ] + ] + | #l0 #ls0 #_ lapply (binaryTM_phase4_write ? M q (None ?) (tape_bin_lift ? (rightof ? l0 ls0)) ?) + [ >tape_bin_lift_unfold >current_mk_tape % ] + lapply (binaryTM_phase2_Some_of ?? q (None ?) … (rev_bin_list ? (l0::ls0)) Htrans) + lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ? + (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])) [//] + cases (IH (tape_move ? (midtape ? (l0::ls0) chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone + #phase3 #phase2 #phase4 #phase0 + %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} % + [ @le_S_S @(le_plus O) // ] + >state_bin_lift_unfold >phase0 [|//] + >(?:tape_move ? (tape_bin_lift ? (rightof ? l0 ls0)) R = tape_bin_lift ? (rightof ? l0 ls0)) + [| >tape_bin_lift_unfold normalize in match (option_hd ??); normalize in match (right ??); + normalize in match (tail ??); normalize in match (left ??); + >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%] + cases (reverse ? (bin_char ? l0)) // cases (rev_bin_list ? ls0) // ] + >phase4 [|//] + >phase2 [|(*arith *) @daemon] + >phase3 [| (*arith*) @daemon] + >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1 + -S (FS_crd sig)-S (displ_of_move sig mv) = k0) + [| (*arith*) @daemon ] + -phase0 -phase2 -phase3 -phase4 (?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv) + (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ]) + = tape_bin_lift ? (tape_move ? (tape_write ? (rightof ? l0 ls0) (Some ? chn)) mv)) + [ % #Hloop + [ @IH (?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //] + >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?); + >iter_tape_move_L [| @daemon ] + >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon] + >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%] + >append_nil >iter_tape_move_L [|@daemon] + normalize in match (tape_move ???); + >tape_bin_lift_unfold @eq_f2 + [ >hd_tech [|@daemon] % + | >tail_tech [|@daemon] >opt_bin_char_Some normalize in match (bin_list ??); >append_nil %] + | normalize in match (displ_of_move ??); >iter_O + normalize in match (tape_move ???); + >tape_bin_lift_unfold % + | normalize in match (displ_of_move ??); + change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?); + >iter_tape_move_L [|@daemon] + normalize in match (tape_move ???); >tape_bin_lift_unfold + >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ] + ] + ] + ] + (*** midtape ***) + | * #ls * #c * #rs #Ht >Ht cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,Some ? c〉) [ cases (trans ? M 〈q,Some ? c〉) * #qn #chn #mv /4 by ex_intro/ ] - * #qn * #chn * #mv cases chn -chn - [ (* no write! *) #Htrans >(binaryTM_phase2_None … Htrans) [2,3: //] + * #qn * #chn * #mv #Htrans + cut (tape_bin_lift ? t = ?) [| >tape_bin_lift_unfold % ] + >Ht in ⊢ (???%→?); >opt_bin_char_Some >left_midtape >right_midtape #Ht' + lapply (binaryTM_phase0_midtape ?? (tape_bin_lift ? t) q … (None ?) Hhalt Ht') + lapply (binaryTM_phase1 ?? q (reverse ? (bin_char ? c)) (rev_bin_list ? ls) + (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)) (Some ? c) ??) + [ cases (bin_list ? rs) // @daemon | >length_reverse @daemon |] + >opt_cons_hd_tl >reverse_reverse + cases chn in Htrans; -chn + [ #Htrans + lapply (binaryTM_phase2_None … Htrans (FS_crd sig) ? + (mk_tape FinBool (rev_bin_list sig ls) + (option_hd FinBool (bin_char sig c@bin_list sig rs)) + (tail FinBool (bin_char sig c@bin_list sig rs)))) [//] + lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ? + (mk_tape FinBool (reverse bool (bin_char sig c)@rev_bin_list ? ls) + (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//] + cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone + #phase3 #phase2 #phase1 #phase0 + %{(S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0)} % + [ @le_S_S @(le_plus O) // ] + >state_bin_lift_unfold phase0 [|//] + >phase1 [|/2 by monotonic_le_minus_l/] + >phase2 [|/2 by monotonic_le_minus_l/] >iter_tape_move_R [|@daemon] - >(?:5*S (FS_crd sig) + k0 - S (FS_crd sig) = 4*S (FS_crd sig) + k0) [|/2 by plus_minus/] - >binaryTM_phase3 - [|//| cut (S (displ_of_move sig mv) ≤ 2*(S (FS_crd sig))) - [ /2 by le_S_S/ - | #H @(transitive_le ??? H) -H -Hcrd @(transitive_le ? (4*S (FS_crd sig))) /2 by le_plus_a/ ] - ] - cut (∀sig,M,m,n,cfg,cfg'.m < n → loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg') [@daemon] - #Hcut <(Hcut ??? (4*S (FS_crd sig) + k0 - S (displ_of_move sig mv)) ??? IH) - [| cases mv - [ >(?:displ_of_move sig L = 2*FS_crd sig) // - >eq_minus_S_pred - @(transitive_le ? (pred (4*FS_crd sig+k0-2*FS_crd sig))) - [ >(?:4*FS_crd sig+k0-2*FS_crd sig = 2*FS_crd sig + k0) - [ cases Hcrd /2 by le_minus_to_plus, le_n/ - | (commutative_times 4) >(commutative_times 2) - eq_minus_S_pred (?:displ_of_move sig N = FS_crd sig) // - >eq_minus_S_pred - @(transitive_le ? (pred (4*FS_crd sig+k0-1*FS_crd sig))) - [ >(?:4*FS_crd sig+k0-1*FS_crd sig = 3*FS_crd sig + k0) - [ cases Hcrd /2 by le_minus_to_plus, le_n/ - | (commutative_times 4) >(commutative_times 1) - Ht whd in match (step ???); (?:displ_of_move ? L = FS_crd sig + FS_crd sig) [| normalize // ] - >iter_split >iter_tape_move_L [|@daemon] >Ht cases ls - [ normalize in match (rev_bin_list ??); - >hd_tech [|@daemon] >tail_tech [|@daemon] - >iter_tape_move_L_left // whd in match (step ???); - phase3 [|/2 by monotonic_le_minus_l/] + -phase0 -phase1 -phase2 -phase3 + >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0 + - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv) + = k0) [| (*arith*) @daemon] + (?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv) + (mk_tape ? (reverse ? (bin_char sig c)@rev_bin_list ? ls) + (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs))) + = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv)) + [ % #Hloop + [ @IH Ht Ht (?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //] + >iter_split >iter_tape_move_L [| @daemon ] + cases ls + [ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//] >tape_bin_lift_unfold % - | #l0 #ls0 change with (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) in match (rev_bin_list ??); + | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%] + normalize in match (tape_move ???); >iter_tape_move_L [|@daemon] >hd_tech [|@daemon] >tail_tech [|@daemon] - whd in match (step ???); tape_bin_lift_unfold >left_midtape >current_midtape - >opt_bin_char_Some >right_midtape % + >tape_bin_lift_unfold % ] + | normalize in match (displ_of_move ??); >iter_O cases rs + [ normalize in match (tape_move ???); >tape_bin_lift_unfold % + | #r0 #rs0 normalize in match (tape_move ???); + >tape_bin_lift_unfold >opt_bin_char_Some + >left_midtape >right_midtape + >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] + >hd_tech [|@daemon] >tail_tech [|@daemon] % ] - | change with - (mk_tape ? (reverse ? (bin_char ? c)@rev_bin_list ? ls) + | normalize in match (displ_of_move ??); >iter_tape_move_L [|@daemon] + >hd_tech [|@daemon] >tail_tech [|@daemon] >tape_bin_lift_unfold % + ] + ] + | #chn #Htrans + lapply (binaryTM_phase2_Some_ow ?? q (Some ? c) ??? (rev_bin_list ? ls) (bin_char ? c) (bin_list ? rs) Htrans ?) + [@daemon] + lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ? + (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? ls) + (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//] + cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone + #phase3 #phase2 #phase1 #phase0 + %{(S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0)} % + [ @le_S_S @(le_plus O) // ] + >state_bin_lift_unfold phase0 [|//] + >phase1 [|/2 by monotonic_le_minus_l/] + >phase2 [|/2 by monotonic_le_minus_l/] + >phase3 [|/2 by monotonic_le_minus_l/] + -phase0 -phase1 -phase2 -phase3 + >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0 + - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv) + = k0) [| (*arith*) @daemon] + (?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv) + (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? ls) (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs))) - in ⊢ (??%?); - >reverse_bin_char_list Ht >tape_bin_lift_unfold @eq_f3 - whd in match (step ???); current_midtape >opt_bin_char_Some - [ right_midtape iter_tape_move_L [|@daemon] - >Ht whd in match (step ???); tape_bin_lift_unfold >left_midtape >current_midtape >right_midtape - >opt_bin_char_Some lapply Hcrd >(?:FS_crd sig = |bin_char ? c|) [| @daemon ] - cases (bin_char ? c) // #H normalize in H; @False_ind - cases (not_le_Sn_O O) /2/ + = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (Some ? chn)) mv)) + [ % #Hloop + [ @IH Ht Ht (?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //] + >iter_split >iter_tape_move_L [| @daemon ] + cases ls + [ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//] + >tape_bin_lift_unfold % + | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%] + normalize in match (tape_move ???); + >iter_tape_move_L [|@daemon] + >hd_tech [|@daemon] >tail_tech [|@daemon] + >tape_bin_lift_unfold % ] + | normalize in match (displ_of_move ??); >iter_O cases rs + [ normalize in match (tape_move ???); >tape_bin_lift_unfold % + | #r0 #rs0 normalize in match (tape_move ???); + >tape_bin_lift_unfold >opt_bin_char_Some + >left_midtape >right_midtape + >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] + >hd_tech [|@daemon] >tail_tech [|@daemon] % + ] + | normalize in match (displ_of_move ??); >iter_tape_move_L [|@daemon] + >hd_tech [|@daemon] >tail_tech [|@daemon] >tape_bin_lift_unfold % ] ] - - - - + ] + ] +] +qed. +definition R_bin_lift ≝ λsig,R,t1,t2. + ∀u1.t1 = tape_bin_lift sig u1 → + ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2. + (* -theorem sem_binaryTM : ∀sig,M. - mk_binaryTM sig M ⊫ R_bin_lift ? (R_TM ? M (start ? M)). -#sig #M #t #i generalize in match t; -t -@(nat_elim1 … i) #m #IH #intape #outc #Hloop - -*) \ No newline at end of file +∀sig,M,i,tf,qf. O < FS_crd sig → + ∀t,q.∃k.i ≤ k ∧ + ((loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) → + loopM ? (mk_binaryTM sig M) k + (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = + Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf))) ∧ + (loopM sig M i (mk_config ?? q t) = None ? → + loopM ? (mk_binaryTM sig M) k + (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = None ?)). + *) +axiom loop_incr : ∀sig,M,m,n,cfg,cfg'.m ≤ n → + loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'. + +theorem sem_binaryTM : + ∀sig,M,R.O < FS_crd sig → M ⊫ R → mk_binaryTM sig M ⊫ R_bin_lift ? R. +#sig #M #R #Hcrd #HM #t #k #outc #Hloopbin #u #Ht +lapply (refl ? (loopM ? M k (initc ? M u))) cases (loopM ? M k (initc ? M u)) in ⊢ (???%→?); +[ #H cases (binaryTM_loop ? M k u (start ? M) Hcrd u (start ? M)) + #k0 * #Hlt * #_ #H1 lapply (H1 H) -H -H1 state_bin_lift_unfold >(loop_incr … Hlt Hloopbin) #H destruct (H) +| * #qf #tf #H cases (binaryTM_loop ? M k tf qf Hcrd u (start ? M)) + #k0 * #Hlt * #H1 #_ lapply (H1 H) -H1 state_bin_lift_unfold >(loop_incr … Hlt Hloopbin) #Heq destruct (Heq) + % [| % [%]] @(HM … H) +qed. \ No newline at end of file