From 356324638c26395cb2ff465b615640c857db05be Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 22 May 2012 09:50:14 +0000 Subject: [PATCH] Progress --- matita/matita/lib/turing/universal/copy.ma | 3 +- .../matita/lib/turing/universal/move_tape.ma | 48 ++++---- .../matita/lib/turing/universal/uni_step.ma | 112 ++++++++++++++---- 3 files changed, 117 insertions(+), 46 deletions(-) diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma index 3ee552d5b..019f06540 100644 --- a/matita/matita/lib/turing/universal/copy.ma +++ b/matita/matita/lib/turing/universal/copy.ma @@ -448,5 +448,4 @@ definition R_copy ≝ λt1,t2. 〈merge_char c0 c1,false〉::reverse ? l1@〈s1,false〉::ls) 〈comma,false〉 rs. -axiom sem_copy : Realize ? copy R_copy. -i \ No newline at end of file +axiom sem_copy : Realize ? copy R_copy. \ No newline at end of file diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index acd45dcd7..716388c86 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -359,12 +359,12 @@ definition R_move_tape_r_abstract ≝ λt1,t2. bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 〈grid,false〉 rs → - no_nulls rs → + no_nulls rs → no_marks rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. - (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc:: + (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧ - lift_tape ls1 newc rs1 = + lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs). lemma lift_tape_not_null : @@ -379,20 +379,22 @@ lemma mtr_concrete_to_abstract : ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2. #t1 #t2 whd in ⊢(%→?); #Hconcrete #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1 -#Hrsnonulls #t1' #Ht1' +#Hrsnonulls #Hrsnomarks #t1' #Ht1' cases (Hconcrete … Htable Ht1) // [ * #Hrs #Ht2 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? []) - @(ex_intro ?? 〈null,false〉) % + @(ex_intro ?? null) % [ >Ht2 % | >Hrs % ] -| * #r0 * #rs0 * #Hrs #Ht2 +| * * #r0 #br0 * #rs0 * #Hrs + cut (br0 = false) [@(Hrsnomarks 〈r0,br0〉) >Hrs @memb_hd] + #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2 @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0) @(ex_intro ?? r0) % - [ >Ht2 % + [ >Ht2 // | >Hrs >lift_tape_not_null [ % - | @Hrsnonulls >Hrs @memb_hd ] ] + | @(Hrsnonulls 〈r0,false〉) >Hrs @memb_hd ] ] qed. definition R_move_tape_l_abstract ≝ λt1,t2. @@ -400,34 +402,36 @@ definition R_move_tape_l_abstract ≝ λt1,t2. bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) → t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 〈grid,false〉 rs → - no_nulls ls → + no_nulls ls → no_marks ls → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. - (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc:: + (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: 〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧ - lift_tape ls1 newc rs1 = + lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs). lemma mtl_concrete_to_abstract : ∀t1,t2.R_move_tape_l t1 t2 → R_move_tape_l_abstract t1 t2. #t1 #t2 whd in ⊢(%→?); #Hconcrete #rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1 -#Hlsnonulls #t1' #Ht1' +#Hlsnonulls #Hlsnomarks #t1' #Ht1' cases (Hconcrete … Htable Ht1) // [ * #Hls #Ht2 @(ex_intro ?? []) @(ex_intro ?? (〈curc,false〉::rs)) - @(ex_intro ?? 〈null,false〉) % + @(ex_intro ?? null) % [ >Ht2 % | >Hls % ] -| * #l0 * #ls0 * #Hls #Ht2 +| * * #l0 #bl0 * #ls0 * #Hls + cut (bl0 = false) [@(Hlsnomarks 〈l0,bl0〉) >Hls @memb_hd] + #Hbl0 >Hbl0 in Hls; #Hls #Ht2 @(ex_intro ?? ls0) @(ex_intro ?? (〈curc,false〉::rs)) @(ex_intro ?? l0) % [ >Ht2 % | >Hls >lift_tape_not_null [ % - | @Hlsnonulls >Hls @memb_hd ] ] + | @(Hlsnonulls 〈l0,false〉) >Hls @memb_hd ] ] qed. lemma Realize_to_Realize : @@ -499,14 +503,14 @@ definition R_move_tape ≝ λt1,t2. table_TM n (reverse ? table1@〈c,false〉::table2) → t1 = midtape STape (table1@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 〈c,false〉 (table2@〈grid,false〉::rs) → - no_nulls ls → no_nulls rs → + no_nulls ls → no_nulls rs → no_marks ls → no_marks rs → ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → ∃ls1,rs1,newc. - (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc:: + (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉:: 〈grid,false〉::reverse ? table1@〈c,false〉::table2@〈grid,false〉::rs1) ∧ - ((c = bit false ∧ lift_tape ls1 newc rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨ - (c = bit true ∧ lift_tape ls1 newc rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨ - (c = null ∧ ls1 = ls ∧ rs1 = rs ∧ 〈curc,false〉 = newc))). + ((c = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨ + (c = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨ + (c = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))). lemma sem_move_tape : Realize ? move_tape R_move_tape. #intape @@ -519,7 +523,7 @@ cases (sem_if ? (test_char ??) … tc_true (sem_test_char ? (λc:STape.c == 〈b #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop #rs #n #table1 #c #table2 #curc #curconfig #ls -#Hcurc #Hc #Hcurconfig #Htable #Hintape #Hls #Hrs #t1' #Ht1' +#Hcurc #Hc #Hcurconfig #Htable #Hintape #Hls #Hrs #Hls1 #Hrs1 #t1' #Ht1' generalize in match HR; -HR * [ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?) [| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq) @@ -561,7 +565,7 @@ generalize in match HR; -HR * whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc * [ * >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ] * #_ #Houtc lapply (Houtc … (refl ??) (refl ??) ?) [@daemon] -Houtc #Houtc - @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? 〈curc,false〉) % + @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) % [ @Houtc | %2 % // % // % // generalize in match Hcneq; generalize in match Hcneq'; diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma index 1198bb9f1..6a6bdc07c 100644 --- a/matita/matita/lib/turing/universal/uni_step.ma +++ b/matita/matita/lib/turing/universal/uni_step.ma @@ -241,11 +241,36 @@ definition exec_move ≝ (seq ? copy (seq ? (move_r …) move_tape)). +definition map_move ≝ + λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ]. + +definition current_of_alpha ≝ λc:STape. + match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ]. + +definition legal_tape ≝ λls,c,rs. + let t ≝ mk_tape STape ls (current_of_alpha c) rs in + left ? t = ls ∧ right ? t = rs ∧ current ? t = current_of_alpha c. + +lemma legal_tape_cases : + ∀ls,c,rs.legal_tape ls c rs → + \fst c ≠ null ∨ (\fst c = null ∧ ls = []) ∨ (\fst c = null ∧ rs = []). +#ls #c #rs cases c #c0 #bc0 cases c0 +[ #c1 normalize #_ % % % #Hfalse destruct (Hfalse) +| cases ls + [ #_ % %2 % % + | #l0 #ls0 cases rs + [ #_ %2 % % + | #r0 #rs0 normalize * * #Hls #Hrs destruct (Hrs) ] + ] +|*: #_ % % % #Hfalse destruct (Hfalse) ] +qed. + definition R_exec_move ≝ λt1,t2. ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2. table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → only_bits (〈s1,false〉::newconfig) → - no_nulls ls → no_nulls rs → + no_nulls ls → no_nulls rs → no_marks ls → no_marks rs → + legal_tape ls 〈c0,false〉 rs → t1 = midtape STape (〈c0,false〉::curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 (table1@〈comma,true〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) → ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → @@ -254,8 +279,23 @@ definition R_exec_move ≝ λt1,t2. (〈s1,false〉::newconfig@〈c2,false〉::〈grid,false〉:: table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs1) ∧ lift_tape ls1 〈c2,false〉 rs1 = - tape_move STape t1' (Some ? 〈〈c2,false〉,move_of_unialpha mv〉). + tape_move STape t1' (map_move c1 mv). +(* move the following 2 lemmata to mono.ma *) +lemma tape_move_left_eq : + ∀A.∀t:tape A.∀c. + tape_move ? t (Some ? 〈c,L〉) = + tape_move_left ? (left ? t) c (right ? t). +// +qed. + +lemma tape_move_right_eq : + ∀A.∀t:tape A.∀c. + tape_move ? t (Some ? 〈c,R〉) = + tape_move_right ? (left ? t) c (right ? t). +// +qed. + lemma sem_exec_move : Realize ? exec_move R_exec_move. #intape cases (sem_seq … sem_init_copy @@ -264,7 +304,7 @@ cases (sem_seq … sem_init_copy #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop #n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2 -#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hls #Hrs #Hintape #t1' #Ht1' +#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hls #Hrs #Hls1 #Hrs1 #Htape #Hintape #t1' #Ht1' cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta @@ -278,38 +318,66 @@ lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1 #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〉::〈s1,false〉::reverse ? newconfig@@〈comma,false〉::reverse ? table1) - mv table2 (merge_char curc d1) (merge_config curconfig (reverse ? newconfig1)) ls ????? - Hls Hrs ??) + (〈comma,false〉::〈c1,false〉::reverse ? newconfig@〈s1,false〉::〈comma,false〉::reverse ? table1) + mv table2 (merge_char c0 c1) (reverse ? newconfig@[〈s1,false〉]) ls ????? + Hls Hrs Hls1 Hrs1 ??) [3: >Htc @(eq_f3 … (midtape ?)) - [ @eq_f >associative_append >Hnewconfig - >reverse_cons >associative_append @eq_f - whd in ⊢ (???%); @eq_f whd in ⊢ (???%); @eq_f - Hnewconfig1 >reverse_append - >merge_cons % + [ @eq_f @eq_f >associative_append >associative_append % | % | % ] | % - || >reverse_cons >reverse_append >reverse_reverse >reverse_cons - >reverse_reverse + || >reverse_cons >reverse_cons >reverse_append >reverse_reverse + >reverse_cons >reverse_cons >reverse_reverse >associative_append >associative_append >associative_append - normalize @Htable + >associative_append >associative_append + @Htable | (* only bits or nulls c1,c2 → only bits or nulls (merge c1 c2) *) @daemon | (* add to hyps? *) @daemon | (* bit_or_null c1,c2 → bit_or_null (merge_char c1 c2) *) @daemon | -Houtc * #ls1 * #rs1 * #newc * #Houtc * [ * [ * #Hmv #Htapemove - @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? (\fst newc)) + @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) % - [ >Houtc >reverse_merge_config [| @daemon ] - >reverse_reverse @eq_f - >reverse_cons >reverse_append >reverse_cons - >reverse_reverse >reverse_reverse - @daemon - | >Hmv >Ht1' whd in Htapemove:(???%); whd in ⊢ (???%); + [ >Houtc -Houtc >reverse_append + >reverse_reverse >reverse_single @eq_f + >reverse_cons >reverse_cons >reverse_append >reverse_cons + >reverse_cons >reverse_reverse >reverse_reverse + >associative_append >associative_append + >associative_append >associative_append + >associative_append >associative_append % + | >Hmv >Ht1' >Htapemove + (* mv = bit false -→ c1 = bit ? + whd in Htapemove:(???%); whd in ⊢ (???%); whd in match (lift_tape ???) in ⊢ (???%); - >Htapemove + >Htapemove *) + cut (∃c1'.c1 = bit c1') [ @daemon ] * #c1' #Hc1 + >Hc1 >tape_move_left_eq cases c0 + [ #c0' % + | cases ls + [ cases rs + [ % + | #r0 #rs0 % ] + | #l0 #ls0 cases rs + [ % + | #r0 #rs0 + + ls #... null # ... # rs + ls #... c # ... # rs + + ∃t.left ? t = ls, right ? t = rs, current t = [[ c ]] + + % ] + + + @eq_f3 + [ + + whd in match (merge_char ??); + whd in match (map_move ??); + + ] + | -- 2.39.2