-lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
- current STape (lift_tape ls c rs) = Some ? c1 →
- c = c1.
-#ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
- [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
-qed.
-
-lemma current_of_low_None: ∀M,t. current FinBool t = None ? →
- current STape (low_tape_aux M t) = None ?.
-#M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
-qed.
-
-lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b →
- current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
-#M #t cases t
- [#b whd in ⊢ ((??%?)→?); #H destruct
- |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
- |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
- |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
- ]
-qed.
-
-lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
- lift_tape ls c rs = low_tape_aux M tape →
- c = 〈match current … tape with
- [ None ⇒ null | Some b ⇒ bit b], false〉.
-#M #tape #ls * #c #cb #rs #Hlegal #Hlift
-cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
- [@eq_f @Hlift] -Hlift #Hlift
-cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
- [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *
- [#Hcurrent >Hcurrent normalize
- >(current_of_low_None …Hcurrent) in Hlift; #Hlift
- >(current_of_lift_None … Hlegal Hlift)
- @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
- |* #b #Hcurrent >Hcurrent normalize
- >(current_of_low_Some …Hcurrent) in Hlift; #Hlift
- @(current_of_lift_Some … Hlegal Hlift)
- ]
-qed.
-
-(*
-lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
- lift_tape ls c rs = low_tape_aux M tape →
- c = 〈match current … tape with
- [ None ⇒ null | Some b ⇒ bit b], false〉.
-#M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
- [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
- #b #_ #_ cases tape
- [whd in ⊢ ((??%%)→?); #H destruct
- |#a #l whd in ⊢ ((??%%)→?); #H destruct
- |#a #l whd in ⊢ ((??%%)→?); #H destruct
- |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
- ]
- |cases c
- [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
- |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
- #_ * [* [#Habs @False_ind /2/
- |#Hls >Hls whd in ⊢ ((??%%)→?); *)
-
-
-(* sufficent conditions to have a low_level_config *)
-lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
-legal_tape ls c rs →
-table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
-lift_tape ls c rs = low_tape_aux M tape →
-〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
-midtape STape (〈grid,false〉::ls)
- 〈qhd,false〉
- (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) =
- low_config M (mk_config ?? s tape).
-#ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
-#Hlift #Hstate whd in match (low_config ??); <Hstate
-@eq_f3
- [@eq_f <(left_of_lift ls c rs) >Hlift //
- | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
- [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
- @(Hcut …Hstate)
- |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
- <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
- ]
-qed.
-
-lemma unistep_true_to_low_step: ∀t1,t2.
- R_uni_step_true t1 t2 → low_step_R_true t1 t2.
-#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
-cases (low_config_eq … eqt1)
-#low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
-***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
-letin trg ≝ (t 〈qin,current ? tape〉)
-letin qout_low ≝ (m_bits_of_state n h (\fst trg))
-letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
-letin qout_low_tl ≝ (tail ? qout_low)
-letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
-letin low_cout ≝ (\fst low_act)
-letin low_m ≝ (\snd low_act)
-lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
- current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1)
- [@daemon
- |>Htable
- @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
- >Hq_low >Hcurrent_low whd in match (mk_tuple ?????);
- >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
- >(eq_pair_fst_snd … (low_action …)) %
- |//
- |@daemon
- ]
--Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
-#q_low_head_false * #ls1 * #rs1 * #c2 * *
-#Ht2 #Hlift #Hlegal %
- [whd in ⊢ (??%?); >q_low_head_false in Hq_low;
- whd in ⊢ ((???%)→?); generalize in match (h qin);
- #x #H destruct (H) %
- |>Ht2 whd in match (step FinBool ??);
- whd in match (trans ???);
- >(eq_pair_fst_snd … (t ?))
- @is_low_config // >Hlift
- <low_tape_move @eq_f2
- [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%);
- cases (current …tape) [%] #b whd in ⊢ (??%%); %
- |whd in match low_cout; whd in match low_m; whd in match low_act;
- generalize in match (\snd (t ?)); * [%] * #b #mv
- whd in ⊢ (??(?(???%)?)%); cases mv %
- ]