From 3447747453bbf439d071d21dcb68149cae3a9068 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Sun, 27 Jan 2013 12:58:58 +0000 Subject: [PATCH] almost there --- .../lib/turing/multi_universal/unistep.ma | 47 +++++-- .../lib/turing/multi_universal/unistep_aux.ma | 129 +++++++++++++----- 2 files changed, 124 insertions(+), 52 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/unistep.ma b/matita/matita/lib/turing/multi_universal/unistep.ma index a4a038184..7fa80f381 100644 --- a/matita/matita/lib/turing/multi_universal/unistep.ma +++ b/matita/matita/lib/turing/multi_universal/unistep.ma @@ -15,21 +15,11 @@ include "turing/multi_universal/unistep_aux.ma". definition exec_move ≝ cfg_to_obj · tape_move_obj · restart_tape prg 2 · obj_to_cfg. -definition low_char' ≝ λc. - match c with - [ None ⇒ null - | Some b ⇒ if (is_bit b) then b else null - ]. - -lemma low_char_option : ∀s. - low_char' (option_map FinBool FSUnialpha bit s) = low_char s. -* // -qed. - definition R_exec_move ≝ λt1,t2:Vector (tape FSUnialpha) 3. ∀c,m,ls1,ls2,rs2. nth cfg ? t1 (niltape ?) = mk_tape FSUnialpha (c::ls1@[bar]) (None ?) [ ] → nth prg ? t1 (niltape ?) = midtape FSUnialpha (ls2@[bar]) m rs2 → + only_bits (list_of_tape ? (nth obj ? t1 (niltape ?))) → c ≠ bar → m ≠ bar → let new_obj ≝ tape_move_mono ? (nth obj ? t1 (niltape ?)) @@ -43,9 +33,9 @@ definition R_exec_move ≝ λt1,t2:Vector (tape FSUnialpha) 3. lemma sem_exec_move: exec_move ⊨ R_exec_move. @(sem_seq_app ??????? sem_cfg_to_obj1 (sem_seq ?????? sem_tape_move_obj - (sem_seq ?????? (sem_restart_tape ???) sem_obj_to_cfg))) // + (sem_seq ?????? (sem_restart_tape ???) sem_obj_to_cfg1))) // #ta #tout * #t1 * #semM1 * #t2 * #semM2 * #t3 * #semM3 #semM4 -#c #m #ls1 #ls2 #rs2 #Hcfg #Hprg #Hc #Hm +#c #m #ls1 #ls2 #rs2 #Hcfg #Hprg #Honlybits #Hc #Hm (* M1 = cfg_to_obj *) lapply (semM1 … Hcfg Hc) #Ht1 (* M2 = tape_move *) @@ -61,8 +51,35 @@ whd in semM3; >Ht2 in semM3; #semM3 lapply (semM3 … (refl ??)); -semM3 >nth_change_vec_neq [2:@eqb_false_to_not_eq %] >nth_change_vec_neq [2:@eqb_false_to_not_eq %] #Ht3 (* M4 = obj_to_cfg *) - - +whd in semM4; >Ht3 in semM4; +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec [2:@leb_true_to_le %] #semM4 lapply (semM4 … (refl ??)) -semM4 +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec_neq [2:@eqb_false_to_not_eq %] +>nth_change_vec [2:@leb_true_to_le %] #semM4 >(semM4 ?) + [(* tape by tape *) + @(eq_vec … (niltape ?)) #i #lei2 + cases (le_to_or_lt_eq … (le_S_S_to_le …lei2)) + [#lei1 cases (le_to_or_lt_eq … (le_S_S_to_le …lei1)) + [#lei0 lapply(le_n_O_to_eq … (le_S_S_to_le …lei0)) #eqi nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec [2:@leb_true_to_le %] % + |#Hi >Hi (* obj tape *) + >nth_change_vec [2:@leb_true_to_le %] whd in ⊢ (???%); + >reverse_cons >reverse_append >reverse_single + whd in match (option_hd ??); whd in match (tail ??); + whd in ⊢ (??%?); % + ] + |#Hi >Hi (* prg tape *) + >nth_change_vec_neq [2:@eqb_false_to_not_eq %] + >nth_change_vec [2:@leb_true_to_le %] whd in ⊢ (???%); + >Hprg whd in match (list_of_tape ??); >reverse_append + >reverse_single % + ] + | + definition unistep ≝ match_m cfg prg FSUnialpha 2 · restart_tape cfg 2 · mmove cfg ? 2 R · copy prg cfg FSUnialpha 2 · diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma index bb730a558..701e59fdc 100644 --- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma +++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma @@ -15,42 +15,6 @@ include "turing/multi_universal/copy.ma". include "turing/multi_universal/alphabet.ma". include "turing/multi_universal/tuples.ma". -(* - - in.obj : ... x ... - ^ - in.cfg : ... ? ? ... - ^ - - out.cfg : ... 1 x ... - ^ - - --------------------- - current (in.obj) = None - - in.cfg : ... ? ? ... - ^ - - out.cfg : ... 0 0 ... - ^ - - obj_to_cfg ≝ - move_l(cfg); - move_l(cfg); - (if (current(in.obj)) == None - then write(0,cfg); - move_r(cfg); - write(0,cfg); - else write(1,cfg); - move_r(cfg); - copy_step(obj,cfg); - move_l(obj);) - move_to_end_l(cfg); - move_r(cfg); - - - cfg_to_obj -*) definition obj ≝ (0:DeqNat). definition cfg ≝ (1:DeqNat). @@ -104,6 +68,10 @@ lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d. | >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ] qed. +lemma None_or_Some: ∀A.∀a. a =None A ∨ ∃b. a = Some ? b. +#A * /2/ #a %2 %{a} % +qed. + lemma not_None_to_Some: ∀A.∀a. a ≠ None A → ∃b. a = Some ? b. #A * /2/ * #H @False_ind @H % qed. @@ -170,6 +138,40 @@ cases Hif -Hif ] qed. +(* another semantics for obj_to_cfg *) +definition low_char' ≝ λc. + match c with + [ None ⇒ null + | Some b ⇒ if (is_bit b) then b else null + ]. + +lemma low_char_option : ∀s. + low_char' (option_map FinBool FSUnialpha bit s) = low_char s. +* // +qed. + +definition R_obj_to_cfg1 ≝ λt1,t2:Vector (tape FSUnialpha) 3. + ∀c,ls. + nth cfg ? t1 (niltape ?) = midtape ? ls c [ ] → + let x ≝ current ? (nth obj ? t1 (niltape ?)) in + (∀b. x= Some ? b → is_bit b = true) → + t2 = change_vec ?? t1 + (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (low_char' x::ls))) + (tail ? (reverse ? (low_char' x::ls)))) cfg. + +lemma sem_obj_to_cfg1: obj_to_cfg ⊨ R_obj_to_cfg1. +@(Realize_to_Realize … sem_obj_to_cfg) #t1 #t2 #Hsem +#c #ls #Hcfg lapply(Hsem c ls Hcfg) * #HSome #HNone #Hb +cases (None_or_Some ? (current ? (nth obj ? t1 (niltape ?)))) + [#Hcur >Hcur @HNone @Hcur + |* #b #Hb1 >Hb1 + cut (low_char' (Some ? b) = b) [whd in ⊢ (??%?); >(Hb b Hb1) %] #Hlow >Hlow + lapply(current_to_midtape … Hb1) * #lsobj * #rsobj #Hmid + @(HSome … Hmid) + ] +qed. + +(* test_null_char *) definition test_null_char ≝ test_char FSUnialpha (λc.c == null). definition R_test_null_char_true ≝ λt1,t2. @@ -388,9 +390,63 @@ lemma sem_tape_move_obj : tape_move_obj ⊨ R_tape_move_obj. ] qed. +(************** list of tape ******************) definition list_of_tape ≝ λsig.λt:tape sig. reverse ? (left ? t)@option_cons ? (current ? t) (right ? t). +lemma list_of_midtape: ∀sig,ls,c,rs. + list_of_tape sig (midtape ? ls c rs) = reverse ? ls@c::rs. +// qed-. + +lemma list_of_rightof: ∀sig,ls,c. + list_of_tape sig (rightof ? c ls) = reverse ? (c::ls). +#sig #ls #c <(append_nil ? (reverse ? (c::ls))) +// qed-. + +lemma list_of_tape_move: ∀sig,t,m. + list_of_tape sig t = list_of_tape sig (tape_move ? t m). +#sig #t * // cases t // + [(* rightof, move L *) #a #l >list_of_midtape + >append_cons list_of_midtape >list_of_midtape + >reverse_cons >associative_append % + |(* midtape, move R *) #ls #c * + [>list_of_midtape >list_of_rightof >reverse_cons % + |#a #rs >list_of_midtape >list_of_midtape >reverse_cons + >associative_append % + ] + ] +qed. + +lemma list_of_tape_write: ∀sig,cond,t,c. +(∀b. c = Some ? b → cond b =true) → +(∀x. mem ? x (list_of_tape ? t) → cond x =true ) → +∀x. mem ? x (list_of_tape sig (tape_write ? t c)) → cond x =true. +#sig #cond #t #c #Hc #Htape #x lapply Hc cases c + [(* c is None *) #_ whd in match (tape_write ???); @Htape + |#b #Hb lapply (Hb … (refl ??)) -Hb #Hb + whd in match (tape_write ???); >list_of_midtape + #Hx cases(mem_append ???? Hx) -Hx + [#Hx @Htape @mem_append_l1 @Hx + |* [//] + #Hx @Htape @mem_append_l2 cases (current sig t) + [@Hx | #c1 %2 @Hx] + ] + ] +qed. + +lemma current_in_list: ∀sig,t,b. + current sig t = Some ? b → mem ? b (list_of_tape sig t). +#sig #t #b cases t + [whd in ⊢ (??%?→?); #Htmp destruct + |#l #b whd in ⊢ (??%?→?); #Htmp destruct + |#l #b whd in ⊢ (??%?→?); #Htmp destruct + |#ls #c #rs whd in ⊢ (??%?→?); #Htmp destruct + >list_of_midtape @mem_append_l2 % % + ] +qed. + definition restart_tape ≝ λi,n. mmove i FSUnialpha n L · inject_TM ? (move_to_end FSUnialpha L) n i · @@ -455,4 +511,3 @@ whd in ⊢ (%→?); #Htb * ] ] qed. - -- 2.39.2