- | % #t1 whd in ⊢ (% → ?); * #ls * #c * #rs
- * * generalize in match c; generalize in match ls;
- -ls -c elim rs
- [ #ls #c #Ht #Hc #Ht1
- % >Ht1 #t2 * #ls0 * #c0 * #rs0 * *
- normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
-
-
- #Ht #Hc #t1
- elim t
- [ % #a whd in ⊢ (% → ?);
-
- #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcc_step alpha sep))
- [%
- |generalize in match Hsep; -Hsep
- generalize in match Ht; -Ht
- generalize in match ls; -ls
- generalize in match a; -a
- generalize in match b; -b
- generalize in match t; -t
- elim rs
- [#t #b #a #ls #Ht #Hsep % #tinit
- whd in ⊢ (%→?); #H @False_ind
- cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
- cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
- |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
- whd in ⊢ (%→?); #H
- cases (H … Ht) #Hbsep #Htinit
- @(Hind … Htinit) cases Hsep
- [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
- [#eqsep %1 >(\P eqsep) // | #H %2 //]
+ | cases t
+ [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
+ |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
+ | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
+ elim rs
+ [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
+ #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
+ % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
+ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+ | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
+ #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
+ >Ht1 @IH
+ ]
+ ]
+ ]
+qed.
+
+lemma sem_adv_to_mark_r :
+ ∀alpha,test.
+ Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
+/2/
+qed.
+
+(* NO OPERATION
+
+ t1 = t2
+ *)
+
+definition nop_states ≝ initN 1.
+
+definition nop ≝
+ λalpha:FinSet.mk_TM alpha nop_states
+ (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
+ O (λ_.true).
+
+definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
+
+lemma sem_nop :
+ ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
+#alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
+qed.
+
+(*
+ q0 _ → q1, R
+ q1 〈a,false〉 → qF, 〈a,true〉, N
+ q1 〈a,true〉 → qF, _ , N
+ qF _ → None ?
+ *)
+
+definition mark_states ≝ initN 3.
+
+definition mark ≝
+ λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
+ (λp.let 〈q,a〉 ≝ p in
+ match a with
+ [ None ⇒ 〈2,None ?〉
+ | Some a' ⇒ match q with
+ [ O ⇒ 〈1,Some ? 〈a',R〉〉
+ | S q ⇒ match q with
+ [ O ⇒ let 〈a'',b〉 ≝ a' in
+ 〈2,Some ? 〈〈a'',true〉,N〉〉
+ | S _ ⇒ 〈2,None ?〉 ] ] ])
+ O (λq.q == 2).
+
+definition R_mark ≝ λalpha,t1,t2.
+ ∀ls,c,d,b,rs.
+ t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
+ t2 = midtape ? (c::ls) 〈d,true〉 rs.
+
+(*lemma mark_q0_q1 :
+ ∀alpha,ls,c,rs.
+ step alpha (mark alpha)
+ (mk_config ?? 0 (midtape … ls c rs)) =
+ mk_config alpha (states ? (mark alpha)) 1
+ (midtape … (ls a0 rs).*)
+
+lemma sem_mark :
+ ∀alpha.Realize ? (mark alpha) (R_mark alpha).
+#alpha #intape @(ex_intro ?? 3) cases intape
+[ @ex_intro
+ [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
+|#a #al @ex_intro
+ [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
+|#a #al @ex_intro
+ [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
+| #ls #c *
+ [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
+ | * #d #b #rs @ex_intro
+ [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
+qed.
+
+include "turing/if_machine.ma".
+
+(* TEST CHAR
+
+ stato finale diverso a seconda che il carattere
+ corrente soddisfi un test booleano oppure no
+
+ q1 = true or no current char
+ q2 = false
+*)
+
+definition tc_states ≝ initN 3.
+
+definition test_char ≝
+ λalpha:FinSet.λtest:alpha→bool.
+ mk_TM alpha tc_states
+ (λp.let 〈q,a〉 ≝ p in
+ match a with
+ [ None ⇒ 〈1, None ?〉
+ | Some a' ⇒
+ match test a' with
+ [ true ⇒ 〈1,None ?〉
+ | false ⇒ 〈2,None ?〉 ]])
+ O (λx.notb (x == 0)).
+
+definition Rtc_true ≝
+ λalpha,test,t1,t2.
+ ∀c. current alpha t1 = Some ? c →
+ test c = true ∧ t2 = t1.
+
+definition Rtc_false ≝
+ λalpha,test,t1,t2.
+ ∀c. current alpha t1 = Some ? c →
+ test c = false ∧ t2 = t1.
+
+lemma tc_q0_q1 :
+ ∀alpha,test,ls,a0,rs. test a0 = true →
+ step alpha (test_char alpha test)
+ (mk_config ?? 0 (midtape … ls a0 rs)) =
+ mk_config alpha (states ? (test_char alpha test)) 1
+ (midtape … ls a0 rs).
+#alpha #test #ls #a0 #ts #Htest normalize >Htest %
+qed.
+
+lemma tc_q0_q2 :
+ ∀alpha,test,ls,a0,rs. test a0 = false →
+ step alpha (test_char alpha test)
+ (mk_config ?? 0 (midtape … ls a0 rs)) =
+ mk_config alpha (states ? (test_char alpha test)) 2
+ (midtape … ls a0 rs).
+#alpha #test #ls #a0 #ts #Htest normalize >Htest %
+qed.
+
+lemma sem_test_char :
+ ∀alpha,test.
+ accRealize alpha (test_char alpha test)
+ 1 (Rtc_true alpha test) (Rtc_false alpha test).
+#alpha #test *
+[ @(ex_intro ?? 2)
+ @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
+ [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
+ % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
+ % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
+| #ls #c #rs @(ex_intro ?? 2)
+ cases (true_or_false (test c)) #Htest
+ [ @(ex_intro ?? (mk_config ?? 1 ?))
+ [| %
+ [ %
+ [ whd in ⊢ (??%?); >tc_q0_q1 //
+ | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
+ | * #Hfalse @False_ind @Hfalse % ]
+ ]
+ | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
+ %
+ [ %
+ [ whd in ⊢ (??%?); >tc_q0_q2 //
+ | #Hfalse destruct (Hfalse) ]
+ | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
+ ]