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 :
∀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.
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 :
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
#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)
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';
(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 →
(〈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
#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
#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
- <Heqcurconfig <reverse_cons >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 ??);
+
+ ]
+ |
projects / helm.git / commitdiff