\ / GNU General Public License Version 2
V_____________________________________________________________*)
-include "turing/universal/move_char_c.ma".
-include "turing/universal/move_char_l.ma".
+include "turing/move_char.ma".
+include "turing/universal/marks.ma".
include "turing/universal/tuples.ma".
definition init_cell_states ≝ initN 2.
+definition ics0 : init_cell_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition ics1 : init_cell_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
definition init_cell ≝
mk_TM STape init_cell_states
(λp.let 〈q,a〉 ≝ p in
- match q with
+ match pi1 … q with
[ O ⇒ match a with
- [ None ⇒ 〈1, Some ? 〈〈null,false〉,N〉〉
- | Some _ ⇒ 〈1, None ?〉 ]
- | S _ ⇒ 〈1,None ?〉 ])
- O (λq.q == 1).
+ [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉
+ | Some _ ⇒ 〈ics1, None ?〉 ]
+ | S _ ⇒ 〈ics1,None ?〉 ])
+ ics0 (λq.q == ics1).
definition R_init_cell ≝ λt1,t2.
(∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨
axiom sem_init_cell : Realize ? init_cell R_init_cell.
-definition swap_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 4) alpha.
-
-definition swap ≝
- λalpha:FinSet.λd:alpha.
- mk_TM alpha (mcl_states alpha)
- (λp.let 〈q,a〉 ≝ p in
- let 〈q',b〉 ≝ q in
- match a with
- [ None ⇒ 〈〈3,d〉,None ?〉
- | Some a' ⇒
- match q' with
- [ O ⇒ (* qinit *)
- 〈〈1,a'〉,Some ? 〈a',R〉〉
- | S q' ⇒ match q' with
- [ O ⇒ (* q1 *)
- 〈〈2,a'〉,Some ? 〈b,L〉〉
- | S q' ⇒ match q' with
- [ O ⇒ (* q2 *)
- 〈〈3,d〉,Some ? 〈b,N〉〉
- | S _⇒ (* qacc *)
- 〈〈3,d〉,None ?〉 ] ] ] ])
- 〈0,d〉
- (λq.let 〈q',a〉 ≝ q in q' == 3).
-
-definition R_swap ≝
- λalpha,t1,t2.
- ∀a,b,ls,rs.
- t1 = midtape alpha ls b (a::rs) →
- t2 = midtape alpha ls a (b::rs).
-
-(*
-lemma swap_q0_q1 :
- ∀alpha:FinSet.∀d,a,ls,a0,rs.
- step alpha (swap alpha d)
- (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
- mk_config alpha (states ? (swap alpha d)) 〈1,a0〉
- (tape_move_right alpha ls a0 rs).
-#alpha #d #a *
-[ #a0 #rs %
-| #a1 #ls #a0 #rs %
-]
-qed.
-
-lemma swap_q1_q2 :
- ∀alpha:FinSet.∀d,a,ls,a0,rs.
- step alpha (swap alpha d)
- (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) =
- mk_config alpha (states ? (swap alpha d)) 〈2,a0〉
- (tape_move_left alpha ls a rs).
-#alpha #sep #a #ls #a0 * //
-qed.
-
-lemma swap_q2_q3 :
- ∀alpha:FinSet.∀d,a,ls,a0,rs.
- step alpha (swap alpha d)
- (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) =
- mk_config alpha (states ? (swap alpha d)) 〈3,d〉
- (tape_move_left alpha ls a rs).
-#alpha #sep #a #ls #a0 * //
-qed.
-*)
-
-lemma sem_swap :
- ∀alpha,d.
- Realize alpha (swap alpha d) (R_swap alpha).
-#alpha #d #tapein @(ex_intro ?? 4) cases tapein
-[ @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
-| #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
-| #a #al @ex_intro [| % [ % | #a #b #ls #rs #Hfalse destruct (Hfalse) ] ]
-| #ls #c #rs cases rs
- [ @ex_intro [| % [ % | #a #b #ls0 #rs0 #Hfalse destruct (Hfalse) ] ]
- | -rs #r #rs @ex_intro
- [|%
- [%
- | #r0 #c0 #ls0 #rs0 #Htape destruct (Htape) normalize cases ls0
- [% | #l1 #ls1 %] ] ] ] ]
-qed.
-
-axiom ssem_move_char_l :
- ∀alpha,sep.
- Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
-
(*
MOVE TAPE RIGHT:
(*
MOVE TAPE LEFT:
- ls # current c # table # d rs
- ^
- ls # current c # table # d rs
- ^
- ls # current c # table d # rs
- ^
- ls # current c # d table # rs
- ^
- ls # current c # d table # rs
- ^
+ ls d? # current c # table # rs
+ ^ move_l; adv_to_mark_l
+ ls d? # current c # table # rs
+ ^ move_l; adv_to_mark_l
+ ls d? # current c # table # rs
+ ^ move_l
+ ls d? # current c # table # rs
+ ^ init_cell
+ ls d # current c # table # rs
+ ^ mtl_aux
ls # current c d # table # rs
- ^
- ls # current c d # table # rs
- ^
- ls # c current c # table # rs
- ^
- ls # c current c # table # rs
+ ^ swap_r
+ ls # current d c # table # rs
+ ^ mtl_aux
+ ls # current d # table c # rs
+ ^ swap
+ ls # current d # table # c rs
+ ^ move_l; adv_to_mark_l
+ ls # current d # table # c rs
+ ^ move_l; adv_to_mark_l
+ ls # current d # table # c rs
^
- ls c # current c # table # rs
- ^
-
-move_to_grid_r;
-swap;
-move_char_l;
-move_l;
-swap;
-move_l;
-move_char_l;
-move_l;
-swap
*)
-axiom move_tape_l : TM STape.
+definition mtl_aux ≝
+ seq ? (swap STape 〈grid,false〉)
+ (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)))).
+definition R_mtl_aux ≝ λt1,t2.
+ ∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 →
+ t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3).
+
+lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
+#intape
+cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …)
+ (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉)
+ (sem_move_l …)))) intape)
+#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#l1 #l2 #l3 #r #Hintape #Hl2
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
+* #tb * whd in ⊢(%→?); #Htb lapply (Htb … Hta) -Htb -Hta whd in ⊢ (???%→?); #Htb
+* #tc * whd in ⊢(%→?); #Htc lapply (Htc … Htb) -Htc -Htb cases l2 in Hl2;
+[ #_ #Htc * #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd >Htc -Htc * #Htd #_
+ whd in ⊢ (%→?); #Houtc lapply (Htd (refl ??)) -Htd @Houtc
+| #c0 #l0 #Hnogrids #Htc *
+ #td * whd in ⊢(%→?); #Htd lapply (Htd … Htc) -Htd -Htc * #_ #Htd
+ lapply (Htd … (refl ??) ??)
+ [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
+ [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
+ [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
+ | @Hmemb ]
+ | % #Hc0 lapply (Hnogrids c0 ?)
+ [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
+ | #Htd whd in ⊢(%→?); >Htd #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
+ >reverse_cons >associative_append @Houtc
+]]
+qed.
+
+definition R_ml_atml ≝ λt1,t2.
+ ∀ls1,ls2,rs.no_grids ls1 →
+ t1 = midtape STape (ls1@〈grid,false〉::ls2) 〈grid,false〉 rs →
+ t2 = midtape STape ls2 〈grid,false〉 (reverse ? ls1@〈grid,false〉::rs).
+
+lemma sem_ml_atml :
+ Realize ? ((move_l …) · (adv_to_mark_l … (λc:STape.is_grid (\fst c)))) R_ml_atml.
+#intape
+cases (sem_seq … (sem_move_l …) (sem_adv_to_mark_l … (λc:STape.is_grid (\fst c))) intape)
+#k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop
+#ls1 #ls2 #rs #Hnogrids #Hintape cases HR -HR
+#ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta
+cases ls1 in Hnogrids;
+[ #_ #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc
+ [ * #_ >Hta #Houtc @Houtc
+ | * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+| #c0 #l0 #Hnogrids #Hta whd in ⊢ (%→?); #Houtc cases (Houtc … Hta) -Houtc
+ [ * #Hc0 lapply (Hnogrids c0 (memb_hd …)) >Hc0 #Hfalse destruct (Hfalse)
+ | * #_ #Htb >reverse_cons >associative_append @Htb //
+ #x #Hx @Hnogrids @memb_cons //
+ ]
+]
+qed.
+
+definition move_tape_l : TM STape ≝
+ seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
+ (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
+ (seq ? (move_l …)
+ (seq ? init_cell
+ (seq ? mtl_aux
+ (seq ? (swap_r STape 〈grid,false〉)
+ (seq ? mtl_aux
+ (seq ? (swap STape 〈grid,false〉)
+ (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
+ (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))))))))))).
+
(* seq ? (move_r …) (seq ? init_cell (seq ? (move_l …)
(seq ? (swap STape 〈grid,false〉)
(seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
definition R_move_tape_l ≝ λt1,t2.
∀rs,n,table,c0,bc0,curconfig,ls0.
- bit_or_null c0 = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
+ bit_or_null c0 = true → only_bits_or_nulls curconfig →
+ table_TM n (reverse ? table) → only_bits ls0 →
t1 = midtape STape (table@〈grid,false〉::〈c0,bc0〉::curconfig@〈grid,false〉::ls0)
〈grid,false〉 rs →
(ls0 = [] ∧
t2 = midtape STape ls1 〈grid,false〉
(reverse ? curconfig@l1::〈grid,false〉::reverse ? table@〈grid,false〉::〈c0,bc0〉::rs)).
-axiom sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
+lemma sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
+#tapein
+cases (sem_seq … sem_ml_atml
+ (sem_seq … sem_ml_atml
+ (sem_seq … (sem_move_l …)
+ (sem_seq … sem_init_cell
+ (sem_seq … sem_mtl_aux
+ (sem_seq … (sem_swap_r STape 〈grid,false〉)
+ (sem_seq … sem_mtl_aux
+ (sem_seq … (sem_swap STape 〈grid,false〉)
+ (sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein)
+#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein)
+[ @daemon (* by no_grids_in_table, manca un lemma sulla reverse *) ]
+-Hta #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈c0,bc0〉::curconfig) … Hta)
+[ @daemon ] -Hta -Htb #Htb
+* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+* #td * whd in ⊢ (%→?); *
+[ * #c1 * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
+ cases ls0 in Hls0;
+ [ #_ #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ #l1 #ls1 #Hls0 #Htapein #Htc change with (midtape ? ls1 l1 ?) in Htc:(???%); >Htc
+ #Hl1 whd in Hl1:(??%?); #Htd
+ * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
+ [ (* memb_reverse *) @daemon ] -Hte -Htd >reverse_reverse #Hte
+ * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+ * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
+ [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
+ * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
+ * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
+ [ (* memb_reverse *) @daemon ] -Hti -Hth #Hti
+ whd in ⊢ (%→?); #Houtc lapply (Houtc (l1::curconfig) … Hti)
+ [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) lapply (Hls0 l1 (memb_hd …)) @bit_not_grid
+ | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ]
+ -Houtc >reverse_cons >associative_append #Houtc %2 %{l1} %{ls1} % [%] @Houtc
+| * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
+ cases ls0
+ [| #l1 #ls1 #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ #Htapein #Htc change with (leftof ???) in Htc:(???%); >Htc #_ #Htd
+ * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
+ [ (*memb_reverse*) @daemon ] -Hte -Htd >reverse_reverse #Hte
+ * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+ * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
+ [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
+ * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
+ * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
+ [ (*memb_reverse*) @daemon ] -Hti -Hth #Hti
+ whd in ⊢ (%→?); #Houtc lapply (Houtc (〈null,false〉::curconfig) … Hti)
+ [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) %
+ | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ]
+ -Houtc >reverse_cons >associative_append
+ >reverse_cons >associative_append #Houtc % % [%] @Houtc
+]
+qed.
+
+(*definition mtl_aux ≝
+ seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)).
+definition R_mtl_aux ≝ λt1,t2.
+ ∀l1,l2,l3,r. t1 = midtape STape l1 r (l2@〈grid,false〉::l3) → no_grids l2 →
+ t2 = midtape STape (reverse ? l2@l1) r (〈grid,false〉::l3).
+
+lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
+#intape
+cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) (sem_move_l …)) intape)
+#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#l1 #l2 #l3 #r #Hintape #Hl2
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
+* #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
+[ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb #_ whd in ⊢ (%→?); #Houtc
+ lapply (Htb (refl ??)) -Htb >Hta @Houtc
+| #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
+ lapply (Htb … (refl ??) ??)
+ [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
+ [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
+ [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
+ | @Hmemb ]
+ | % #Hc0 lapply (Hnogrids c0 ?)
+ [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
+ | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
+ >reverse_cons >associative_append @Houtc
+]]
+qed.
+
+check swap*)
+
(*
by cases on current:
[ None ⇒ 〈null,false〉
| Some c0 ⇒ c0 ].
-definition mk_tuple ≝ λc,newc,mv.
- c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉].
-
-inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝
-| mit_hd :
- ∀tb.
- match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb)
-| mit_tl :
- ∀c0,newc0,mv0,tb.
- match_in_table c newc mv tb →
- match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb).
definition move_of_unialpha ≝
λc.match c with
definition R_uni_step ≝ λt1,t2.
∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
table_TM n table →
- match_in_table (〈c,false〉::curs@[〈curc,false〉])
- (〈c1,false〉::news@[〈newc,false〉]) mv table →
+ match_in_table n (〈c,false〉::curs) 〈curc,false〉
+ (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 table →
t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉
(curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) →
∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs →
definition no_nulls ≝
λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
+definition current_of_alpha ≝ λc:STape.
+ match \fst c with [ null ⇒ None ? | _ ⇒ Some ? c ].
+
+(*
+ no_marks (c::ls@rs)
+ only_bits (ls@rs)
+ bit_or_null c
+
+*)
+definition legal_tape ≝ λls,c,rs.
+ no_marks (c::ls@rs) ∧ only_bits (ls@rs) ∧ bit_or_null (\fst c) = true ∧
+ (\fst c ≠ null ∨ ls = [] ∨ rs = []).
+
+lemma legal_tape_left :
+ ∀ls,c,rs.legal_tape ls c rs →
+ left ? (mk_tape STape ls (current_of_alpha c) rs) = ls.
+#ls * #c #bc #rs * * * #_ #_ #_ *
+[ *
+ [ cases c
+ [ #c' #_ %
+ | * #Hfalse @False_ind /2/
+ |*: #_ % ]
+ | #Hls >Hls cases c // cases rs //
+ ]
+| #Hrs >Hrs cases c // cases ls //
+]
+qed.
+
+axiom legal_tape_current :
+ ∀ls,c,rs.legal_tape ls c rs →
+ current ? (mk_tape STape ls (current_of_alpha c) rs) = current_of_alpha c.
+
+axiom legal_tape_right :
+ ∀ls,c,rs.legal_tape ls c rs →
+ right ? (mk_tape STape ls (current_of_alpha c) rs) = rs.
+
+(*
+lemma legal_tape_cases :
+ ∀ls,c,rs.legal_tape ls c rs →
+ \fst c ≠ null ∨ (\fst c = null ∧ (ls = [] ∨ rs = [])).
+#ls #c #rs cases c #c0 #bc0 cases c0
+[ #c1 normalize #_ % % #Hfalse destruct (Hfalse)
+| cases ls
+ [ #_ %2 % // % %
+ | #l0 #ls0 cases rs
+ [ #_ %2 % // %2 %
+ | #r0 #rs0 normalize * * #_ #Hrs destruct (Hrs) ]
+ ]
+|*: #_ % % #Hfalse destruct (Hfalse) ]
+qed.
+
+axiom legal_tape_conditions :
+ ∀ls,c,rs.(\fst c ≠ null ∨ ls = [] ∨ rs = []) → legal_tape ls c rs.
+(*#ls #c #rs *
+[ *
+ [ >(eq_pair_fst_snd ?? c) cases (\fst c)
+ [ #c0 #Hc % % %
+ | * #Hfalse @False_ind /2/
+ |*: #Hc % % %
+ ]
+ | cases ls [ * #Hfalse @False_ind /2/ ]
+ #l0 #ls0
+
+ #Hc
+*)
+*)
+
definition R_move_tape_r_abstract ≝ λt1,t2.
∀rs,n,table,curc,curconfig,ls.
- bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
+ is_bit 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 →
+ legal_tape ls 〈curc,false〉 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 =
- tape_move_right STape ls 〈curc,false〉 rs).
+ lift_tape ls1 〈newc,false〉 rs1 =
+ tape_move_right STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
lemma lift_tape_not_null :
∀ls,c,rs. is_null (\fst c) = false →
[|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
//
qed.
+
+axiom bit_not_null : ∀d.is_bit d = true → is_null d = false.
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'
+#rs #n #table #curc #curconfig #ls #Hbitcurc #Hcurconfig #Htable #Ht1
+* * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
cases (Hconcrete … Htable Ht1) //
[ * #Hrs #Ht2
@(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
- @(ex_intro ?? 〈null,false〉) %
- [ >Ht2 %
- | >Hrs % ]
-| * #r0 * #rs0 * #Hrs #Ht2
+ @(ex_intro ?? null) %
+ [ %
+ [ >Ht2 %
+ | >Hrs % ]
+ | % [ % [ %
+ [ >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') %
+ | @Hnomarks @(memb_append_l1 … Hx') ]
+ | >append_nil #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') //
+ | @Hbits @(memb_append_l1 … Hx') ]]
+ | % ]
+ | %2 % ]
+ ]
+| * * #r0 #br0 * #rs0 * #Hrs
+ cut (br0 = false)
+ [ @(Hnomarks 〈r0,br0〉) @memb_cons @memb_append_l2 >Hrs @memb_hd]
+ #Hbr0 >Hbr0 in Hrs; #Hrs #Ht2
@(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
@(ex_intro ?? r0) %
- [ >Ht2 %
- | >Hrs >lift_tape_not_null
- [ %
- | @Hrsnonulls >Hrs @memb_hd ] ]
+ [ %
+ [ >Ht2 //
+ | >Hrs >lift_tape_not_null
+ [ %
+ | @bit_not_null @(Hbits 〈r0,false〉) >Hrs @memb_append_l2 @memb_hd ] ]
+ | % [ % [ %
+ [ #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') %
+ | cases (memb_append … Hx') #Hx'' @Hnomarks
+ [ @(memb_append_l1 … Hx'')
+ | >Hrs @memb_cons @memb_append_l2 @(memb_cons … Hx'') ]
+ ]
+ | whd in ⊢ (?%); #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') //
+ | cases (memb_append … Hx') #Hx'' @Hbits
+ [ @(memb_append_l1 … Hx'') | >Hrs @memb_append_l2 @(memb_cons … Hx'') ]
+ ]]
+ | whd in ⊢ (??%?); >(Hbits 〈r0,false〉) //
+ @memb_append_l2 >Hrs @memb_hd ]
+ | % % % #Hr0 lapply (Hbits 〈r0,false〉?)
+ [ @memb_append_l2 >Hrs @memb_hd
+ | >Hr0 normalize #Hfalse destruct (Hfalse)
+ ] ] ] ]
qed.
definition R_move_tape_l_abstract ≝ λt1,t2.
∀rs,n,table,curc,curconfig,ls.
- bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n (reverse ? table) →
+ is_bit 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 →
+ legal_tape ls 〈curc,false〉 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 =
- tape_move_left STape ls 〈curc,false〉 rs).
+ lift_tape ls1 〈newc,false〉 rs1 =
+ tape_move_left STape ls 〈curc,false〉 rs ∧ legal_tape ls1 〈newc,false〉 rs1).
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'
-cases (Hconcrete … Htable Ht1) //
+* * * #Hnomarks #Hbits #Hcurc #Hlegal #t1' #Ht1'
+cases (Hconcrete … Htable ? Ht1) //
[ * #Hls #Ht2
@(ex_intro ?? [])
@(ex_intro ?? (〈curc,false〉::rs))
- @(ex_intro ?? 〈null,false〉) %
- [ >Ht2 %
- | >Hls % ]
-| * #l0 * #ls0 * #Hls #Ht2
- @(ex_intro ?? ls0)
- @(ex_intro ?? (〈curc,false〉::rs))
+ @(ex_intro ?? null) %
+ [ %
+ [ >Ht2 %
+ | >Hls % ]
+ | % [ % [ %
+ [ #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') %
+ | @Hnomarks >Hls @Hx' ]
+ | #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') //
+ | @Hbits >Hls @Hx' ]]
+ | % ]
+ | % %2 % ]
+ ]
+| * * #l0 #bl0 * #ls0 * #Hls
+ cut (bl0 = false)
+ [ @(Hnomarks 〈l0,bl0〉) @memb_cons @memb_append_l1 >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 ] ]
-qed.
-
-lemma Realize_to_Realize :
- ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
-#alpha #M #R1 #R2 #Himpl #HR1 #intape
-cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
-@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
-qed.
+ [ %
+ [ >Ht2 %
+ | >Hls >lift_tape_not_null
+ [ %
+ | @bit_not_null @(Hbits 〈l0,false〉) >Hls @memb_append_l1 @memb_hd ] ]
+ | % [ % [ %
+ [ #x #Hx cases (orb_true_l … Hx) #Hx'
+ [ >(\P Hx') %
+ | cases (memb_append … Hx') #Hx'' @Hnomarks
+ [ >Hls @memb_cons @memb_cons @(memb_append_l1 … Hx'')
+ | cases (orb_true_l … Hx'') #Hx'''
+ [ >(\P Hx''') @memb_hd
+ | @memb_cons @(memb_append_l2 … Hx''')]
+ ]
+ ]
+ | whd in ⊢ (?%); #x #Hx cases (memb_append … Hx) #Hx'
+ [ @Hbits >Hls @memb_cons @(memb_append_l1 … Hx')
+ | cases (orb_true_l … Hx') #Hx''
+ [ >(\P Hx'') //
+ | @Hbits @(memb_append_l2 … Hx'')
+ ]]]
+ | whd in ⊢ (??%?); >(Hbits 〈l0,false〉) //
+ @memb_append_l1 >Hls @memb_hd ]
+ | % % % #Hl0 lapply (Hbits 〈l0,false〉?)
+ [ @memb_append_l1 >Hls @memb_hd
+ | >Hl0 normalize #Hfalse destruct (Hfalse)
+ ] ] ]
+| #x #Hx @Hbits @memb_append_l1 @Hx ]
+qed.
lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
@(Realize_to_Realize … mtl_concrete_to_abstract) //
tc_true) tc_true.
definition R_move_tape ≝ λt1,t2.
- ∀rs,n,table1,c,table2,curc,curconfig,ls.
- bit_or_null curc = true → bit_or_null c = true → only_bits_or_nulls curconfig →
- table_TM n (reverse ? table1@〈c,false〉::table2) →
+ ∀rs,n,table1,mv,table2,curc,curconfig,ls.
+ bit_or_null mv = true → only_bits_or_nulls curconfig →
+ (is_bit mv = true → is_bit curc = true) →
+ table_TM n (reverse ? table1@〈mv,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 →
+ 〈mv,false〉 (table2@〈grid,false〉::rs) →
+ legal_tape ls 〈curc,false〉 rs →
∀t1'.t1' = lift_tape ls 〈curc,false〉 rs →
∃ls1,rs1,newc.
- (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc::
- 〈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))).
+ legal_tape ls1 〈newc,false〉 rs1 ∧
+ (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@〈newc,false〉::
+ 〈grid,false〉::reverse ? table1@〈mv,false〉::table2@〈grid,false〉::rs1) ∧
+ ((mv = bit false ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_left STape ls 〈curc,false〉 rs) ∨
+ (mv = bit true ∧ lift_tape ls1 〈newc,false〉 rs1 = tape_move_right STape ls 〈curc,false〉 rs) ∨
+ (mv = null ∧ ls1 = ls ∧ rs1 = rs ∧ curc = newc))).
lemma sem_move_tape : Realize ? move_tape R_move_tape.
#intape
(sem_seq … (sem_move_l …) (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))))) 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'
+#rs #n #table1 #mv #table2 #curc #curconfig #ls
+#Hmv #Hcurconfig #Hmvcurc #Htable #Hintape #Htape #t1' #Ht1'
generalize in match HR; -HR *
-[ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?)
+[ * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
[| >Hintape % ] -Hta #Hceq #Hta lapply (\P Hceq) -Hceq #Hceq destruct (Hta Hceq)
* #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hintape) -Htb -Hintape
[ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
* #_ #Htb lapply (Htb … (refl ??) (refl ??) ?)
[ @daemon ] -Htb >append_cons <associative_append #Htb
whd in ⊢ (%→?); #Houtc lapply (Houtc … Htb … Ht1') //
- [ >reverse_append >reverse_append >reverse_reverse @Htable |]
- -Houtc -Htb * #ls1 * #rs1 * #newc * #Houtc #Hnewtape
+ [ >reverse_append >reverse_append >reverse_reverse @Htable
+ | /2/
+ ||]
+ -Houtc -Htb * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
@(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
- [ >Houtc >reverse_append >reverse_append >reverse_reverse
- >associative_append >associative_append %
- | % % % // ]
-| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈c,false〉 ?)
- [| >Hintape % ] -Hta #Hcneq cut (c ≠ bit false)
+ [ //
+ | %
+ [ >Houtc >reverse_append >reverse_append >reverse_reverse
+ >associative_append >associative_append %
+ | % % % // ]
+ ]
+| * #ta * whd in ⊢ (%→?); #Hta cases (Hta 〈mv,false〉 ?)
+ [| >Hintape % ] -Hta #Hcneq cut (mv ≠ bit false)
[ lapply (\Pf Hcneq) @not_to_not #Heq >Heq % ] -Hcneq #Hcneq #Hta destruct (Hta)
*
- [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈c,false〉 ?)
+ [ * #tb * whd in ⊢ (%→?);#Htb cases (Htb 〈mv,false〉 ?)
[| >Hintape % ] -Htb #Hceq #Htb lapply (\P Hceq) -Hceq #Hceq destruct (Htb Hceq)
* #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape) -Htc -Hintape
[ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
* #_ #Htc lapply (Htc … (refl ??) (refl ??) ?)
[ @daemon ] -Htc >append_cons <associative_append #Htc
whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc … Ht1') //
- [ >reverse_append >reverse_append >reverse_reverse @Htable |]
- -Houtc -Htc * #ls1 * #rs1 * #newc * #Houtc #Hnewtape
+ [ >reverse_append >reverse_append >reverse_reverse @Htable
+ | /2/ |]
+ -Houtc -Htc * #ls1 * #rs1 * #newc * * #Houtc #Hnewtape #Hnewtapelegal
@(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? newc) %
- [ >Houtc >reverse_append >reverse_append >reverse_reverse
- >associative_append >associative_append %
- | % %2 % // ]
- | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈c,false〉 ?)
- [| >Hintape % ] -Htb #Hcneq' cut (c ≠ bit true)
+ [ //
+ | %
+ [ >Houtc >reverse_append >reverse_append >reverse_reverse
+ >associative_append >associative_append %
+ | % %2 % // ]
+ ]
+ | * #tb * whd in ⊢ (%→?); #Htb cases (Htb 〈mv,false〉 ?)
+ [| >Hintape % ] -Htb #Hcneq' cut (mv ≠ bit true)
[ lapply (\Pf Hcneq') @not_to_not #Heq >Heq % ] -Hcneq' #Hcneq' #Htb destruct (Htb)
* #tc * whd in ⊢ (%→?); #Htc cases (Htc … Hintape)
- [ * >(bit_or_null_not_grid … Hc) #Hfalse destruct (Hfalse) ] -Htc
+ [ * >(bit_or_null_not_grid … Hmv) #Hfalse destruct (Hfalse) ] -Htc
* #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@daemon] -Htc #Htc
* #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc
whd in ⊢ (???%→?); #Htd whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc *
- [ * >(bit_or_null_not_grid … Hcurc) #Hfalse destruct (Hfalse) ]
+ [ * cases Htape * * #_ #_ #Hcurc #_
+ >(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〉) %
- [ @Houtc
- | %2 % // % // % //
- generalize in match Hcneq; generalize in match Hcneq';
- cases c in Hc; normalize //
- [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ]
- |*: #Hfalse destruct (Hfalse) ]
+ @(ex_intro ?? ls) @(ex_intro ?? rs) @(ex_intro ?? curc) %
+ [ //
+ | %
+ [ @Houtc
+ | %2 % // % // % //
+ generalize in match Hcneq; generalize in match Hcneq';
+ cases mv in Hmv; normalize //
+ [ * #_ normalize [ #Hfalse @False_ind cases Hfalse /2/ | #_ #Hfalse @False_ind cases Hfalse /2/ ]
+ |*: #Hfalse destruct (Hfalse) ]
+ ]
]
]
]
projects / helm.git / blobdiff