From f5ccde287dec5598a3b88197be03da87ac50ce98 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 22 Jan 2013 14:37:41 +0000 Subject: [PATCH] termination! --- .../lib/turing/multi_universal/universal.ma | 278 ++---------------- 1 file changed, 21 insertions(+), 257 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/universal.ma b/matita/matita/lib/turing/multi_universal/universal.ma index e43851aa3..e371e4d90 100644 --- a/matita/matita/lib/turing/multi_universal/universal.ma +++ b/matita/matita/lib/turing/multi_universal/universal.ma @@ -93,267 +93,31 @@ theorem sem_universal2: ∀M:normalTM. ∀R. % [% [@(R_TM_to_R … HRTM) @HMR | //] | //] qed. -axiom terminate_UTM: ∀M:normalTM.∀t. - M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)). - - - - - - - - -lemma current_embedding: ∀c. - high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c. - * normalize // qed. - -lemma tape_embedding: ∀ls,c,rs. - high_tape - (map ?? (λb.〈bit b,false〉) ls) - (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) - (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs. -#ls #c #rs >high_tape_eq >bool_embedding >bool_embedding ->current_embedding % -qed. - -definition high_move ≝ λc,mv. - match c with - [ bit b ⇒ Some ? 〈b,move_of_unialpha mv〉 - | _ ⇒ None ? - ]. - -definition map_move ≝ - λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ]. - -definition low_step_R_true ≝ λt1,t2. - ∀M:normalTM. - ∀c: nconfig (no_states M). - t1 = low_config M c → - halt ? M (cstate … c) = false ∧ - t2 = low_config M (step ? M c). - -definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝ -λM:normalTM.λt. - let current_low ≝ match current … t with - [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in - let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in - let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in - mk_tape STape low_left current_low low_right. - -lemma left_of_low_tape: ∀M,t. - left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t). -#M * // -qed. - -lemma right_of_low_tape: ∀M,t. - right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t). -#M * // -qed. - -definition low_move ≝ λaction:option (bool × move). - match action with - [None ⇒ None ? - |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)]. - -(* simulation lemma *) -lemma low_tape_move : ∀M,action,t. - tape_move STape (low_tape_aux M t) (low_move action) = - low_tape_aux M (tape_move FinBool t action). -#M * // (* None *) -* #b #mv #t cases mv cases t // - [#ls #c #rs cases ls //|#ls #c #rs cases rs //] -qed. - -lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls. -#ls * #c #b #rs cases c // cases ls // cases rs // -qed. - -lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs → - right ? (lift_tape ls c rs) = rs. -#ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr -#H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct] -qed. - - -lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs → - current STape (lift_tape ls 〈c,b〉 rs) = - match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉]. -#ls #c #b #rs cases c // whd in ⊢ (%→?); * #_ -* [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //] - |#Hrs >Hrs whd in ⊢ (??%%); cases ls //] -qed. - -lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs → - current STape (lift_tape ls 〈c,b〉 rs) = None ? → - c = null. -#ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize - [#b #H destruct |// |3,4,5:#H destruct ] -qed. - -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. +(* termination *) -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 ??); 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 Hlift @right_of_low_tape - ] +lemma halting_case: ∀M:normalTM.∀t,q. halt ? M q = true → + universalTM↓low_tapes M (mk_config ?? q t). +#M #t #q #Hhalt +@(terminate_while ?? uni_body ????? (sem_uni_body … M)) [%] +% #ta whd in ⊢ (%→?); #H cases (H … (refl ??)) #_ >Hhalt +#Habs destruct (Habs) 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 - 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 % - ] +theorem terminate_UTM: ∀M:normalTM.∀t. + M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)). +#M #t #H @(terminate_while ?? uni_body ????? (sem_uni_body … M)) [%] +lapply H -H * #x (* we need to generalize to an arbitrary initial configuration *) +whd in match (initc ? M t); generalize in match (start ? M); lapply t -t +elim x + [#t #q * #outc whd in ⊢ (??%?→?); #Habs destruct + |#n #Hind #t #q cases (true_or_false (halt ? M q)) #Hhaltq + [* #outc whd in ⊢ (??%?→?); >Hhaltq whd in ⊢ (??%?→?); #HSome destruct (HSome) + % #ta whd in ⊢ (%→?); #H cases (H … (refl ??)) #_ >Hhaltq + #Habs destruct (Habs) + |* #outc whd in ⊢ (??%?→?); >Hhaltq whd in ⊢ (??%?→?); #Hloop + % #t1 whd in ⊢ (%→?); #Hstep lapply (Hstep … (refl ??)) * + #Ht1 #_ >Ht1 @Hind %{outc} Ht1 whd in ⊢ (??%?); @eq_f -normalize in Hqin; destruct (Hqin) % -qed. - -definition low_R ≝ λM,qstart,R,t1,t2. - ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) → - ∃q,tape2.R tape1 tape2 ∧ - halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2). - -lemma sem_uni_step1: - uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false]. -qed. - -definition universalTM ≝ whileTM ? uni_step us_acc. - -theorem sem_universal: ∀M:normalTM. ∀qstart. - universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)). -qed. - -theorem sem_universal2: ∀M:normalTM. ∀R. - M ⊫ R → universalTM ⊫ (low_R M (start ? M) R). -#M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize -#t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1) -#q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2) -% [% [@(R_TM_to_R … HRTM) @HMR | //] | //] -qed. - -axiom terminate_UTM: ∀M:normalTM.∀t. - M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)). - -- 2.39.2