record mTM (sig:FinSet) (tapes_no:nat) : Type[1] ≝
{ states : FinSet;
trans : states × (Vector (option sig) (S tapes_no)) →
- states × (Vector (option (sig × move))(S tapes_no));
+ states × (Vector ((option sig) × move) (S tapes_no));
start: states;
halt : states → bool
}.
definition current_chars ≝ λsig.λn.λtapes.
vec_map ?? (current sig) (S n) tapes.
+lemma nth_current_chars : ∀sig,n,tapes,i.
+ nth i ? (current_chars sig n tapes) (None ?)
+ = current sig (nth i ? tapes (niltape sig)).
+#sig #n #tapes #i >(nth_vec_map … (current sig) i (S n)) %
+qed.
+
+definition tape_move_multi ≝
+ λsig,n,ts,mvs.
+ pmap_vec ??? (tape_move_mono sig) n ts mvs.
+
+lemma tape_move_multi_def : ∀sig,n,ts,mvs.
+ tape_move_multi sig n ts mvs = pmap_vec ??? (tape_move_mono sig) n ts mvs.
+// qed.
+
definition step ≝ λsig.λn.λM:mTM sig n.λc:mconfig sig (states ?? M) n.
let 〈news,mvs〉 ≝ trans sig n M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in
- mk_mconfig ???
- news
- (pmap_vec ??? (tape_move sig) ? (ctapes ??? c) mvs).
+ mk_mconfig ??? news (tape_move_multi sig ? (ctapes ??? c) mvs).
definition empty_tapes ≝ λsig.λn.
mk_Vector ? n (make_list (tape sig) (niltape sig) n) ?.
definition nop ≝
λalpha:FinSet.λn.mk_mTM alpha n nop_states
- (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉)
+ (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (〈None ?,N〉) (S n)) ?〉)
start_nop (λ_.true).
elim n normalize //
qed.
(************************** Sequential Composition ****************************)
definition null_action ≝ λsig.λn.
-mk_Vector ? (S n) (make_list (option (sig × move)) (None ?) (S n)) ?.
+mk_Vector ? (S n) (make_list (option sig × move) (〈None ?,N〉) (S n)) ?.
elim (S n) // normalize //
qed.
lemma tape_move_null_action: ∀sig,n,tapes.
- pmap_vec ??? (tape_move sig) (S n) tapes (null_action sig n) = tapes.
+ tape_move_multi sig (S n) tapes (null_action sig n) = tapes.
#sig #n #tapes cases tapes -tapes #tapes whd in match (null_action ??);
#Heq @Vector_eq <Heq -Heq elim tapes //
#a #tl #Hind whd in ⊢ (??%?); @eq_f2 // @Hind
% [@Hloop |@Hsub @Houtc]
qed.
+theorem acc_sem_seq : ∀sig,n.∀M1,M2:mTM sig n.∀R1,Rtrue,Rfalse,acc.
+ M1 ⊨ R1 → M2 ⊨ [ acc: Rtrue, Rfalse ] →
+ M1 · M2 ⊨ [ inr … acc: R1 ∘ Rtrue, R1 ∘ Rfalse ].
+#sig #n #M1 #M2 #R1 #Rtrue #Rfalse #acc #HR1 #HR2 #t
+cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
+cases (HR2 (ctapes sig (states ?? M1) n outc1)) #k2 * #outc2 * * #Hloop2
+#HMtrue #HMfalse
+@(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
+% [ %
+[@(loop_merge ???????????
+ (loop_lift ??? (lift_confL sig n (states sig n M1) (states sig n M2))
+ (step sig n M1) (step sig n (seq sig n M1 M2))
+ (λc.halt sig n M1 (cstate … c))
+ (λc.halt_liftL ?? (halt sig n M1) (cstate … c)) … Hloop1))
+ [ * *
+ [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+ | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+ || #c0 #Hhalt <step_seq_liftL //
+ | #x <p_halt_liftL %
+ |6:cases outc1 #s1 #t1 %
+ |7:@(loop_lift … (initc ??? (ctapes … outc1)) … Hloop2)
+ [ * #s2 #t2 %
+ | #c0 #Hhalt <step_seq_liftR // ]
+ |whd in ⊢ (??(????%)?);whd in ⊢ (??%?);
+ generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
+ >(trans_liftL_true sig n M1 M2 ??)
+ [ whd in ⊢ (??%?); whd in ⊢ (???%);
+ @mconfig_eq whd in ⊢ (???%); //
+ | @(loop_Some ?????? Hloop10) ]
+ ]
+| >(mconfig_expand … outc2) in ⊢ (%→?); whd in ⊢ (??%?→?);
+ #Hqtrue destruct (Hqtrue)
+ @(ex_intro … (ctapes ? (FinSum (states ?? M1) (states ?? M2)) ? (lift_confL … outc1)))
+ % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R /2/ ]
+| >(mconfig_expand … outc2) in ⊢ (%→?); whd in ⊢ (?(??%?)→?); #Hqfalse
+ @(ex_intro … (ctapes ? (FinSum (states ?? M1) (states ?? M2)) ? (lift_confL … outc1)))
+ % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R @HMfalse
+ @(not_to_not … Hqfalse) //
+]
+qed.
+
+lemma acc_sem_seq_app : ∀sig,n.∀M1,M2:mTM sig n.∀R1,Rtrue,Rfalse,R2,R3,acc.
+ M1 ⊨ R1 → M2 ⊨ [acc: Rtrue, Rfalse] →
+ (∀t1,t2,t3. R1 t1 t3 → Rtrue t3 t2 → R2 t1 t2) →
+ (∀t1,t2,t3. R1 t1 t3 → Rfalse t3 t2 → R3 t1 t2) →
+ M1 · M2 ⊨ [inr … acc : R2, R3].
+#sig #n #M1 #M2 #R1 #Rtrue #Rfalse #R2 #R3 #acc
+#HR1 #HRacc #Hsub1 #Hsub2
+#t cases (acc_sem_seq … HR1 HRacc t)
+#k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc)
+% [% [@Hloop
+ |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
+ |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
+qed.