- >(?:qin0@(〈cin0,false〉::〈comma,false〉::qout0@[〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@〈bar,false〉::T0
- = mk_tuple qin cin qout cout mv@〈bar,false〉::T0)
- [|>Hqin >Hqout >Hcin >Hcout >Hmv normalize >associative_append >associative_append
- normalize >associative_append % ]
- % %{qin0} %{cin0} %{qout0} %{cout0} %{mv0} % // % [|@Hlenqout0] % // %
- [ | @Hcout0mv0 ] % // % // % // % // % // % // %
- | #c0 #cs0 #HT cut (∃cs1.c0::cs0 = tuple@〈bar,false〉::cs1)
- [ cases (append_eq_tech1 ?????? HT ?)
- [ -HT #ta #Hta cases (append_eq_tech2 … Hta ?)
- [ -Hta #tb #Htb %{tb} @Htb
- | @daemon ]
- | @le_S_S >length_append >(plus_n_O (|tuple|)) >commutative_plus @le_plus
- [ @le_O_n
- | >Htuple normalize >length_append >length_append @le_plus [ >Hlenqin >Hlenqin0 % ]
- @le_S_S @le_S_S >length_append >length_append @le_plus [ >Hlenqout >Hlenqout0 % ] %] ]
- ]
- * #cs1 #Hcs1 >Hcs1 in HT; >associative_append >associative_append #HT
- lapply (append_l2_injective … HT) // -HT #HT
- lapply (cons_injective_r ????? HT) -HT
- <associative_append #HT >Htuple %2 // @(IH … HT)
- ]
-]
-qed.
-
-(*
-lemma table_invert_l : ∀n,T0,qin,cin,qout,cout,mv.
- table_TM n (mk_tuple qin cin qout cout mv@〈bar,false〉::T0) →
- tuple_TM n (mk_tuple qin cin qout cout mv).
-#n #T #qin #cin #qout #cout #mv #HT inversion HT
-[ change with (append ???) in ⊢ (??(??%?)?→?);cases qin [ #Hfalse | #t0 #ts0 #Hfalse] normalize in Hfalse; destruct (Hfalse)
-| #t0 #T0 #Ht0 #HT0 #_
-
-
-lemma table_invert_r : ∀n,T0,qin,cin,qout,cout,mv.
- table n (mk_tuple qin cin qout cout mv@〈bar,false〉::T0) → table n T0.
-*)
-
-lemma no_grids_in_tuple : ∀n,l.tuple_TM n l → no_grids l.
-#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * *
-#_ #_ #Hqin #Hqout #Hcin #Hcout #Hmv #_ #_ #_ #Hl >Hl
-#c #Hc normalize in Hc; cases (memb_append … Hc) -Hc #Hc
-[ @bit_not_grid @(Hqin … Hc)
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid //
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
-| cases (memb_append …Hc) -Hc #Hc
-[ @bit_not_grid @(Hqout … Hc)
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid //
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
-| >(memb_single … Hc) @bit_or_null_not_grid @Hmv
-]]]]]]
-qed.
-
-lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l.
-#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * *
-#Hqin #Hqout #_ #_ #_ #_ #_ #_ #_ #_ #Hl >Hl
-#c #Hc normalize in Hc; cases (memb_append … Hc) -Hc #Hc
-[ @(Hqin … Hc)
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) %
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
-| cases (memb_append … Hc) -Hc #Hc
-[ @(Hqout … Hc)
-| cases (orb_true_l … Hc) -Hc #Hc
-[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) %
-| cases (orb_true_l … Hc) -Hc #Hc
-
-[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
-| >(memb_single … Hc) %
-]]]]]]
-qed.
-
-lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l.
-#n #l #t elim t
- [normalize #c #H destruct
- |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_grids_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx
- cases (memb_append … Hx) -Hx #Hx
- [ @(Ht1 … Hx)
- | cases (orb_true_l … Hx) -Hx #Hx
- [ >(\P Hx) %
- | @(IH … Hx) ] ] ]
-qed.
-
-lemma no_marks_in_table: ∀n.∀l.table_TM n l → no_marks l.
-#n #l #t elim t
- [normalize #c #H destruct
- |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_marks_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx
- cases (memb_append … Hx) -Hx #Hx
- [ @(Ht1 … Hx)
- | cases (orb_true_l … Hx) -Hx #Hx
- [ >(\P Hx) %
- | @(IH … Hx) ] ] ]
-qed.
-
-axiom last_of_table: ∀n,l,b.¬ table_TM n (l@[〈bar,b〉]).
-
-(*
-l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2
- ^ ^
-
-if current (* x *) = #
- then
- else if x = 0
- then move_right; ----
- adv_to_mark_r;
- if current (* x0 *) = 0
- then advance_mark ----
- adv_to_mark_l;
- advance_mark
- else STOP
- else x = 1 (* analogo *)
-
-*)
-
-
-(*
- MARK NEXT TUPLE machine
- (partially axiomatized)
-
- marks the first character after the first bar (rightwards)
- *)
-
-definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c).
-
-definition mark_next_tuple ≝
- seq ? (adv_to_mark_r ? bar_or_grid)
- (ifTM ? (test_char ? (λc:STape.is_bar (\fst c)))
- (move_right_and_mark ?) (nop ?) 1).
-
-definition R_mark_next_tuple ≝
- λt1,t2.
- ∀ls,c,rs1,rs2.
- (* c non può essere un separatore ... speriamo *)
- t1 = midtape STape ls c (rs1@〈grid,false〉::rs2) →
- no_marks rs1 → no_grids rs1 → bar_or_grid c = false →
- (∃rs3,rs4,d,b.rs1 = rs3 @ 〈bar,false〉 :: rs4 ∧
- no_bars rs3 ∧
- Some ? 〈d,b〉 = option_hd ? (rs4@〈grid,false〉::rs2) ∧
- t2 = midtape STape (〈bar,false〉::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@〈grid,false〉::rs2)))
- ∨
- (no_bars rs1 ∧ t2 = midtape ? (reverse ? rs1@c::ls) 〈grid,false〉 rs2).
-
-axiom tech_split :
- ∀A:DeqSet.∀f,l.
- (∀x.memb A x l = true → f x = false) ∨
- (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f x = false).
-(*#A #f #l elim l
-[ % #x normalize #Hfalse *)
-
-theorem sem_mark_next_tuple :
- Realize ? mark_next_tuple R_mark_next_tuple.
-#intape
-lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
- (ifTM ? (test_char ? (λc:STape.is_bar (\fst c))) (move_right_and_mark ?) (nop ?) 1) ????)
-[@sem_if [5: // |6: @sem_move_right_and_mark |7: // |*:skip]
-| //
-|||#Hif cases (Hif intape) -Hif
- #j * #outc * #Hloop * #ta * #Hleft #Hright
- @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
- -Hloop
- #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hrs1' #Hc
- cases (Hleft … Hrs)
- [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
- | * #_ #Hta cases (tech_split STape (λc.is_bar (\fst c)) rs1)
- [ #H1 lapply (Hta rs1 〈grid,false〉 rs2 (refl ??) ? ?)
- [ * #x #b #Hx whd in ⊢ (??%?); >(Hrs1' … Hx) >(H1 … Hx) %
- | %
- | -Hta #Hta cases Hright
- [ * #tb * whd in ⊢ (%→?); #Hcurrent
- @False_ind cases (Hcurrent 〈grid,false〉 ?)
- [ normalize #Hfalse destruct (Hfalse)
- | >Hta % ]
- | * #tb * whd in ⊢ (%→?); #Hcurrent
- cases (Hcurrent 〈grid,false〉 ?)
- [ #_ #Htb whd in ⊢ (%→?); #Houtc
- %2 %
- [ @H1
- | >Houtc >Htb >Hta % ]
- | >Hta % ]
- ]
- ]
- | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
- % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
- lapply (Hta rs3 c0 (rs4@〈grid,false〉::rs2) ???)
- [ #x #Hrs3' whd in ⊢ (??%?); >Hsplit in Hrs1;>Hsplit in Hrs3;
- #Hrs3 #Hrs1 >(Hrs1 …) [| @memb_append_l1 @Hrs3'|]
- >(Hrs3 … Hrs3') @Hrs1' >Hsplit @memb_append_l1 //
- | whd in ⊢ (??%?); >Hc0 %
- | >Hsplit >associative_append % ] -Hta #Hta
- cases Hright
- [ * #tb * whd in ⊢ (%→?); #Hta'
- whd in ⊢ (%→?); #Htb
- cases (Hta' c0 ?)
- [ #_ #Htb' >Htb' in Htb; #Htb
- generalize in match Hsplit; -Hsplit
- cases rs4 in Hta;
- [ #Hta #Hsplit >(Htb … Hta)
- >(?:c0 = 〈bar,false〉)
- [ @(ex_intro ?? grid) @(ex_intro ?? false)
- % [ % [ %
- [(* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
- | (* Hc0 *) @daemon ]
- | #r5 #rs5 >(eq_pair_fst_snd … r5)
- #Hta #Hsplit >(Htb … Hta)
- >(?:c0 = 〈bar,false〉)
- [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
- % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
- | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
- | * #tb * whd in ⊢ (%→?); #Hta'
- whd in ⊢ (%→?); #Htb
- cases (Hta' c0 ?)
- [ #Hfalse @False_ind >Hfalse in Hc0;
- #Hc0 destruct (Hc0)
- | >Hta % ]
-]]]]
-qed.
-
-definition init_current_on_match ≝
- (seq ? (move_l ?)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?) (mark ?)))).
-
-definition R_init_current_on_match ≝ λt1,t2.
- ∀l1,l2,c,rs. no_grids l1 → is_grid c = false →
- t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::l2) 〈grid,false〉 rs →
- t2 = midtape STape (〈grid,false〉::l2) 〈c,true〉 ((reverse ? l1)@〈grid,false〉::rs).
-
-lemma sem_init_current_on_match :
- Realize ? init_current_on_match R_init_current_on_match.
-#intape
-cases (sem_seq ????? (sem_move_l ?)
- (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (sem_seq ????? (sem_move_r ?) (sem_mark ?))) intape)
-#k * #outc * #Hloop #HR
-@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
-#l1 #l2 #c #rs #Hl1 #Hc #Hintape
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape
-generalize in match Hl1; cases l1
- [#Hl1 whd in ⊢ ((???(??%%%))→?); #Hta
- * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Hta
- [* >Hc #Htemp destruct (Htemp) ]
- * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1)
- whd in ⊢ ((???(??%%%))→?); -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd
- whd in ⊢ ((???(??%%%))→?); #Htd
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc
- >Houtc %
- |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Hta
- * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb
- [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)]
- * #Hd >append_cons #Htb lapply (Htb … (refl ??) (refl …) ?)
- [#x #membx cases (memb_append … membx) -membx #membx
- [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]]-Htb #Htb
- * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc
- >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc #Houtc
- >Houtc >reverse_cons >associative_append %
- ]
-qed.
-
-(*
-definition init_current_gen ≝
- seq ? (adv_to_mark_l ? (is_marked ?))
- (seq ? (clear_mark ?)
- (seq ? (move_l ?)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?) (mark ?))))).
-
-definition R_init_current_gen ≝ λt1,t2.
- ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 →
- Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) →
- t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs →
- t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉
- ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)).
-
-lemma sem_init_current_gen : Realize ? init_current_gen R_init_current_gen.
-#intape
-cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
- (sem_seq ????? (sem_clear_mark ?)
- (sem_seq ????? (sem_move_l ?)
- (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (sem_seq ????? (sem_move_r ?) (sem_mark ?))))) intape)
-#k * #outc * #Hloop #HR
-@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
-#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hintape
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape
- [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
-* #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%] -Hta #Hta
-* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta #Htb
-* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb
-generalize in match Hc; generalize in match Hl2; cases l2
- [#_ whd in ⊢ ((???%)→?); #Htemp destruct (Htemp)
- whd in ⊢ ((???(??%%%))→?); #Htc
- * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
- [2: * whd in ⊢ (??%?→?); #Htemp destruct (Htemp) ]
- * #_ #Htd >Htd in Htc; -Htd #Htd
- * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd
- >reverse_append >reverse_cons
- whd in ⊢ ((???(??%%%))→?); #Hte
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc
- >Houtc %
- |#d #tl #Htl #Hc0 whd in ⊢ ((???(??%%%))→?); #Htc
- * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
- [* >(Htl … (memb_hd …)) whd in ⊢ (??%?→?); #Htemp destruct (Htemp)]
- * #Hd #Htd lapply (Htd … (refl ??) (refl ??) ?)
- [#x #membx @Htl @memb_cons @membx] -Htd #Htd
- * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd
- >reverse_append >reverse_cons >reverse_cons
- >reverse_cons in Hc0; >reverse_cons cases (reverse ? tl)
- [normalize in ⊢ (%→?); #Hc0 destruct (Hc0) #Hte
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc
- >Houtc %
- |* #c2 #b2 #tl2 normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
- whd in ⊢ ((???(??%%%))→?); #Hte
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc
- >Houtc >associative_append >associative_append >associative_append %
- ]
- ]
-qed.
-*)
-definition init_current ≝
- seq ? (adv_to_mark_l ? (is_marked ?))
- (seq ? (clear_mark ?)
- (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?) (mark ?)))).
-
-definition R_init_current ≝ λt1,t2.
- ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → is_grid c = false →
- Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) →
- t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs →
- t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉
- ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)).
-
-lemma sem_init_current : Realize ? init_current R_init_current.
-#intape
-cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?))
- (sem_seq ????? (sem_clear_mark ?)
- (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
- (sem_seq ????? (sem_move_r ?) (sem_mark ?)))) intape)
-#k * #outc * #Hloop #HR
-@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop]
-cases HR -HR #ta * whd in ⊢ (%→?); #Hta
-* #tb * whd in ⊢ (%→?); #Htb
-* #tc * whd in ⊢ (%→?); #Htc
-* #td * whd in ⊢ (%→%→?); #Htd #Houtc
-#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hc0 #Hintape
-cases (Hta … Hintape) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
--Hta * #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%]
--Hta #Hta lapply (Htb … Hta) -Htb #Htb cases (Htc … Htb) [ >Hc -Hc * #Hc destruct (Hc) ]
--Htc * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@Hl2]
--Htc #Htc lapply (Htd … Htc) -Htd
->reverse_append >reverse_cons
->reverse_cons in Hc0; cases (reverse … l2)
-[ normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
- #Htd >(Houtc … Htd) %
-| * #c2 #b2 #tl2 normalize in ⊢ (%→?);
- #Hc0 #Htd >(Houtc … Htd)
- whd in ⊢ (???%); destruct (Hc0)
- >associative_append >associative_append %