*)
-include "turing/while_machine.ma".
include "turing/if_machine.ma".
+include "turing/basic_machines.ma".
include "turing/universal/alphabet.ma".
-include "turing/universal/tests.ma".
(* ADVANCE TO MARK (right)
definition atm_states ≝ initN 3.
+definition atm0 : atm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
+definition atm1 : atm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
+definition atm2 : atm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
+
definition atmr_step ≝
λalpha:FinSet.λtest:alpha→bool.
mk_TM alpha atm_states
(λp.let 〈q,a〉 ≝ p in
match a with
- [ None ⇒ 〈1, None ?〉
+ [ None ⇒ 〈atm1, None ?〉
| Some a' ⇒
match test a' with
- [ true ⇒ 〈1,None ?〉
- | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
- O (λx.notb (x == 0)).
+ [ true ⇒ 〈atm1,None ?〉
+ | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
+ atm0 (λx.notb (x == atm0)).
definition Ratmr_step_true ≝
λalpha,test,t1,t2.
lemma atmr_q0_q1 :
∀alpha,test,ls,a0,rs. test a0 = true →
step alpha (atmr_step alpha test)
- (mk_config ?? 0 (midtape … ls a0 rs)) =
- mk_config alpha (states ? (atmr_step alpha test)) 1
+ (mk_config ?? atm0 (midtape … ls a0 rs)) =
+ mk_config alpha (states ? (atmr_step alpha test)) atm1
(midtape … ls a0 rs).
-#alpha #test #ls #a0 #ts #Htest normalize >Htest %
+#alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
+whd in match (trans … 〈?,?〉); >Htest %
qed.
lemma atmr_q0_q2 :
∀alpha,test,ls,a0,rs. test a0 = false →
step alpha (atmr_step alpha test)
- (mk_config ?? 0 (midtape … ls a0 rs)) =
- mk_config alpha (states ? (atmr_step alpha test)) 2
+ (mk_config ?? atm0 (midtape … ls a0 rs)) =
+ mk_config alpha (states ? (atmr_step alpha test)) atm2
(mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
-#alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
+#alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
+whd in match (trans … 〈?,?〉); >Htest cases ts //
qed.
lemma sem_atmr_step :
∀alpha,test.
accRealize alpha (atmr_step alpha test)
- 2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
+ atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
#alpha #test *
[ @(ex_intro ?? 2)
- @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
- [ % // #Hfalse destruct | #_ % // % % ]
-| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
- % [ % // #Hfalse destruct | #_ % // % % ]
-| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
- % [ % // #Hfalse destruct | #_ % // % % ]
+ @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
+ [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
+ % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
+| #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
+ % [ % // whd in ⊢ ((??%%)→?); #Hfalse destruct | #_ % // % % ]
| #ls #c #rs @(ex_intro ?? 2)
cases (true_or_false (test c)) #Htest
- [ @(ex_intro ?? (mk_config ?? 1 ?))
+ [ @(ex_intro ?? (mk_config ?? atm1 ?))
[| %
[ %
[ whd in ⊢ (??%?); >atmr_q0_q1 //
- | #Hfalse destruct ]
+ | whd in ⊢ ((??%%)→?); #Hfalse destruct ]
| #_ % // %2 @(ex_intro ?? c) % // ]
]
- | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
+ | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
%
[ %
[ whd in ⊢ (??%?); >atmr_q0_q2 //
t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
definition adv_to_mark_r ≝
- λalpha,test.whileTM alpha (atmr_step alpha test) 2.
+ λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
lemma wsem_adv_to_mark_r :
∀alpha,test.
definition mark_states ≝ initN 2.
+definition ms0 : mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition ms1 : mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
definition mark ≝
λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
(λp.let 〈q,a〉 ≝ p in
match a with
- [ None ⇒ 〈1,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',true〉,N〉〉
- | S q ⇒ 〈1,None ?〉 ] ])
- O (λq.q == 1).
+ [ None ⇒ 〈ms1,None ?〉
+ | Some a' ⇒ match (pi1 … q) with
+ [ O ⇒ let 〈a'',b〉 ≝ a' in 〈ms1,Some ? 〈〈a'',true〉,N〉〉
+ | S q ⇒ 〈ms1,None ?〉 ] ])
+ ms0 (λq.q == ms1).
definition R_mark ≝ λalpha,t1,t2.
∀ls,c,b,rs.
@ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
qed.
-(* MOVE RIGHT
-
- moves the head one step to the right
-
-*)
-
-definition move_states ≝ initN 2.
-
-definition move_r ≝
- λalpha:FinSet.mk_TM alpha move_states
- (λp.let 〈q,a〉 ≝ p in
- match a with
- [ None ⇒ 〈1,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ 〈1,Some ? 〈a',R〉〉
- | S q ⇒ 〈1,None ?〉 ] ])
- O (λq.q == 1).
-
-definition R_move_r ≝ λalpha,t1,t2.
- ∀ls,c,rs.
- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
-
-lemma sem_move_r :
- ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
-#alpha #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-| #ls #c #rs
- @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
- cases rs0 // ] ] ]
-qed.
-
-(* MOVE LEFT
-
- moves the head one step to the right
-
-*)
-
-definition move_l ≝
- λalpha:FinSet.mk_TM alpha move_states
- (λp.let 〈q,a〉 ≝ p in
- match a with
- [ None ⇒ 〈1,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ 〈1,Some ? 〈a',L〉〉
- | S q ⇒ 〈1,None ?〉 ] ])
- O (λq.q == 1).
-
-definition R_move_l ≝ λalpha,t1,t2.
- ∀ls,c,rs.
- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
-
-lemma sem_move_l :
- ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
-#alpha #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-| #ls #c #rs
- @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
- cases ls0 // ] ] ]
-qed.
(* MOVE RIGHT AND MARK machine
definition mrm_states ≝ initN 3.
+definition mrm0 : mrm_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
+definition mrm1 : mrm_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
+definition mrm2 : mrm_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
+
definition move_right_and_mark ≝
λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mrm_states
(λp.let 〈q,a〉 ≝ p in
match a with
- [ None ⇒ 〈2,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ 〈1,Some ? 〈a',R〉〉
+ [ None ⇒ 〈mrm2,None ?〉
+ | Some a' ⇒ match pi1 … q with
+ [ O ⇒ 〈mrm1,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).
+ 〈mrm2,Some ? 〈〈a'',true〉,N〉〉
+ | S _ ⇒ 〈mrm2,None ?〉 ] ] ])
+ mrm0 (λq.q == mrm2).
definition R_move_right_and_mark ≝ λalpha,t1,t2.
∀ls,c,d,b,rs.
definition clear_mark_states ≝ initN 3.
+definition clear0 : clear_mark_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
+definition clear1 : clear_mark_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
+definition claer2 : clear_mark_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
+
definition clear_mark ≝
λalpha:FinSet.mk_TM (FinProd … alpha FinBool) clear_mark_states
(λp.let 〈q,a〉 ≝ p in
match a with
- [ None ⇒ 〈1,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ let 〈a'',b〉 ≝ a' in 〈1,Some ? 〈〈a'',false〉,N〉〉
- | S q ⇒ 〈1,None ?〉 ] ])
- O (λq.q == 1).
+ [ None ⇒ 〈clear1,None ?〉
+ | Some a' ⇒ match pi1 … q with
+ [ O ⇒ let 〈a'',b〉 ≝ a' in 〈clear1,Some ? 〈〈a'',false〉,N〉〉
+ | S q ⇒ 〈clear1,None ?〉 ] ])
+ clear0 (λq.q == clear1).
definition R_clear_mark ≝ λalpha,t1,t2.
∀ls,c,b,rs.
| * #Hx0 #Houtc %2
% [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
| >Houtc % ]
- | (* members of lists are invariant under reverse *) @daemon ]
+ | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ]
| %2 % [ @(\Pf Hc) ]
>Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
>Hx in Hc;#Hc destruct (Hc) ]
is_marked ? c = false ∧ t2 = t1.
lemma sem_comp_step :
- accRealize ? comp_step (inr … (inl … (inr … 0)))
+ accRealize ? comp_step (inr … (inl … (inr … start_nop)))
R_comp_step_true R_comp_step_false.
#intape
cases (acc_sem_if … (sem_test_char ? (is_marked ?))
qed.
definition compare ≝
- whileTM ? comp_step (inr … (inl … (inr … 0))).
+ whileTM ? comp_step (inr … (inl … (inr … start_nop))).
(*
definition R_compare :=
reverse ? la@ls)
〈d',false〉 (lc@〈comma,false〉::l2)).
-lemma list_ind2 :
- ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
- length ? l1 = length ? l2 →
- (P [] []) →
- (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
- P l1 l2.
-#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
-generalize in match Hl; generalize in match l2;
-elim l1
-[#l2 cases l2 // normalize #t2 #tl2 #H destruct
-|#t1 #tl1 #IH #l2 cases l2
- [normalize #H destruct
- |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
-]
-qed.
-
-lemma list_cases_2 :
- ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
- length ? l1 = length ? l2 →
- (l1 = [] → l2 = [] → P) →
- (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
-#T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
-[ #Pnil #Pcons @Pnil //
-| #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
-qed.
-
lemma wsem_compare : WRealize ? compare R_compare.
#t #i #outc #Hloop
lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
|#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
#Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
[2: * >Hc' #Hfalse @False_ind destruct ] * #_
- @(list_cases_2 … Hlen)
+ @(list_cases2 … Hlen)
[ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
-Hrs #Hrs normalize in Hrs; #Hleft cases (Hleft ????? Hrs ?) -Hleft
[ * #Heqb #Htapeb cases (IH … Htapeb) -IH * #IH #_ #_
]
]]]]]
qed.
-
+
axiom sem_compare : Realize ? compare R_compare.
\ No newline at end of file
projects / helm.git / blobdiff