[|% [% |cases t normalize // ] ]
qed.
+(***************************** replace a with f a *****************************)
+
+definition writef ≝ λalpha,f.
+ mk_TM alpha write_states
+ (λp.let 〈q,a〉 ≝ p in
+ match pi1 … q with
+ [ O ⇒ 〈wr1,Some ? (f a),N〉
+ | S _ ⇒ 〈wr1,None ?,N〉 ])
+ wr0 (λx.x == wr1).
+
+definition R_writef ≝ λalpha,f,t1,t2.
+ ∀c. current ? t1 = c →
+ t2 = midtape alpha (left ? t1) (f c) (right ? t1).
+
+lemma sem_writef : ∀alpha,f.
+ writef alpha f ⊨ R_writef alpha f.
+#alpha #f #t @(ex_intro … 2) @ex_intro
+ [|% [% |cases t normalize // ] ]
+qed.
+
(******************** moves the head one step to the right ********************)
definition move_states ≝ initN 2.
inductive move : Type[0] ≝
| L : move | R : move | N : move.
+
+(*************************** turning moves into a DeqSet **********************)
+
+definition move_eq ≝ λm1,m2:move.
+ match m1 with
+ [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
+ |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
+ |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
+
+lemma move_eq_true:∀m1,m2.
+ move_eq m1 m2 = true ↔ m1 = m2.
+*
+ [* normalize [% #_ % |2,3: % #H destruct ]
+ |* normalize [1,3: % #H destruct |% #_ % ]
+ |* normalize [1,2: % #H destruct |% #_ % ]
+qed.
+
+definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
+
+unification hint 0 ≔ ;
+ X ≟ DeqMove
+(* ---------------------------------------- *) ⊢
+ move ≡ carr X.
+
+unification hint 0 ≔ m1,m2;
+ X ≟ DeqMove
+(* ---------------------------------------- *) ⊢
+ move_eq m1 m2 ≡ eqb X m1 m2.
+
+
+(************************ turning DeqMove into a FinSet ***********************)
+
+definition move_enum ≝ [L;R;N].
+
+lemma move_enum_unique: uniqueb ? [L;R;N] = true.
+// qed.
+
+lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
+* // qed.
+
+definition FinMove ≝
+ mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
+unification hint 0 ≔ ;
+ X ≟ FinMove
+(* ---------------------------------------- *) ⊢
+ move ≡ FinSetcarr X.
(********************************** machine ***********************************)
record TM (sig:FinSet): Type[1] ≝
include "turing/multi_to_mono/exec_trace_move.ma".
(* include "turing/turing.ma". *)
-let rec exec_moves sig n i on i : TM (multi_sig sig n) ≝
+(**************************** Vector Operations *******************************)
+
+let rec resize A (l:list A) i d on i ≝
+ match i with
+ [ O ⇒ [ ]
+ | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
+ ].
+
+lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
+#A #l #i lapply l -l elim i
+ [#l #d %
+ |#m #Hind #l cases l
+ [#d normalize @eq_f @Hind
+ |#a #tl #d normalize @eq_f @Hind
+ ]
+ ]
+qed.
+
+lemma resize_id : ∀A,n,l,d. |l| = n →
+ resize A l n d = l.
+#A #n elim n
+ [#l #d #H >(lenght_to_nil … H) //
+ |#m #Hind * #d normalize
+ [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
+ ]
+qed.
+
+definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
+#A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
+qed.
+
+axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
+ nth i ? (resize_vec A n v j d) d = nth i ? v d.
+
+lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d.
+ resize_vec A n v n d = v.
+#A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
+qed.
+
+definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
+ mk_Vector A 1 [a] (refl ??).
+
+definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
+#A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
+>length_append >(len A n v) //
+qed.
+
+lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
+ a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
+// qed.
+
+axiom nth_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
+ nth n ? (vec_cons_right A a n v) d = a.
+(*
+#A #a #n elim n
+ [#v #d >(vector_nil … v) //
+ |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);
+ whd in match (vec_cons_right ????);
+*)
+
+lemma get_moves_cons_right: ∀Q,sig,n,q,moves,a.
+ get_moves Q sig (S n)
+ (vec_cons_right ? (Some ? (inl ?? 〈q,moves〉)) (S n) a) = moves.
+#Q #sig #n #q #moves #a whd in ⊢(??%?); >nth_cons_right //
+qed.
+
+axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
+ resize_vec ? (S n) (vec_cons_right A a n v) n d = v.
+
+let rec exec_moves Q sig n i on i : TM (MTA (HC Q n) sig (S n)) ≝
match i with
[ O ⇒ nop ? (* exec_move_i sig n 0 *)
- | S j ⇒ seq ? (exec_moves sig n j) (exec_move_i sig n j)
+ | S j ⇒ seq ? (exec_moves Q sig n j) (exec_move_i Q sig n j)
].
-
-axiom get_moves : ∀sig,n.∀a:multi_sig sig n.∀i.Vector DeqMove i.
-axiom get_moves_cons: ∀sig,n,a,j.j < n →
- get_moves sig n a (S j) =
- vec_cons ? (get_move ? n a j) j (get_moves sig n a j).
-
definition a_moves ≝
λsig,n.λactions: Vector ((option sig) × move) n.
vec_map ?? (snd ??) n actions.
λsig,n,ts,chars.
pmap_vec ??? (tape_write sig) n ts chars.
+(*
+let rec i_moves a i on i : Vector move i ≝
+ match i with
+ [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
+ | S j ⇒ vec_cons ? (nth j ? a N) j (i_moves a j)
+ ]. *)
+
+definition vec_moves ≝ λQ,sig,n,a,i.
+ resize_vec … (get_moves Q sig n a) i N.
+
+axiom vec_moves_cons: ∀Q,sig,n,a,j.j < n →
+ vec_moves Q sig n a (S j) =
+ vec_cons ? (get_move Q ? n a j) j (vec_moves Q sig n a j).
+
(*
axiom actions_commute : ∀sig,n,ts,actions.
tape_moves sig n (tape_writem ?? ts (a_chars … actions)) (a_moves … actions) =
(* devo rafforzare la semantica, dicendo che i tape non toccati
dalle moves non cambiano *)
-definition R_exec_moves ≝ λsig,n,i,t1,t2.
+
+definition R_exec_moves ≝ λQ,sig,n,i,t1,t2.
∀a,ls,rs.
t1 = midtape ? ls a rs →
- (∀i.regular_trace sig n a ls rs i) →
- nth n ? (vec … a) (blank ?) = head ? →
+ (∀i.regular_trace (TA (HC Q n) sig) (S n) a ls rs i) →
+ is_head ?? (nth n ? (vec … a) (blank ?)) = true →
no_head_in … ls →
no_head_in … rs →
∃ls1,a1,rs1.
- t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
- (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
- readback sig n ls1 (vec … a1) rs1 i =
- tape_moves ?? (readback sig n ls (vec … a) rs i) (get_moves sig n a i) ∧
+ t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
+ (∀i.regular_trace (TA (HC Q n) sig) (S n) a1 ls1 rs1 i) ∧
+ readback ? (S n) ls1 (vec … a1) rs1 i =
+ tape_moves ?? (readback ? (S n) ls (vec … a) rs i) (vec_moves Q sig n a i) ∧
(∀j. i ≤ j → j ≤ n →
- rb_trace_i sig n ls1 (vec … a1) rs1 j =
- rb_trace_i sig n ls (vec … a) rs j).
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
+ rb_trace_i ? (S n) ls (vec … a) rs j).
(* alias id "Realize_to_Realize" =
"cic:/matita/turing/mono/Realize_to_Realize.def(13)". *)
]
qed.
-lemma sem_exec_moves: ∀sig,n,i. i < n →
- exec_moves sig n i ⊨ R_exec_moves sig n i.
-#sig #n #i elim i
+lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n →
+ exec_moves Q sig n i ⊨ R_exec_moves Q sig n i.
+#Q #sig #n #i elim i
[#_ @(Realize_to_Realize … (sem_nop …))
#t1 #t2 #H #a #ls #rs #Ht1 #Hreg #H1 #H2 #H3
%{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| %]|//]
|#j #Hind #lttj lapply (lt_to_le … lttj) #ltj
- @(sem_seq_app … (Hind ltj) (sem_exec_move_i … ltj)) -Hind
+ @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind
#int #outt * #t1 * #H1 #H2
#a #ls #rs #Hint #H3 #H4 #H5 #H6
lapply (H1 … Hint H3 H4 H5 H6)
* #ls1 * #a1 * #rs1 * * * #H7 #H8 #H9 #H10
lapply (reg_inv … (H8 n) ? H4 H5 H6)
- [@H10 [@lt_to_le @ltj |@le_n]]
+ [@H10 [@ltj |@le_n]]
-H3 -H4 -H5 -H6 * * #H3 #H4 #H5
lapply (H2 … H7 H8 H3 H4 H5)
* #ls2 * #a2 * #rs2 * * * #Houtt #Hregout #Hrboutt #Hrbid
%{ls2} %{a2} %{rs2}
- cut (∀i. get_move sig n a i = get_move sig n a1 i)
+ cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i)
[@daemon] #aa1
%[%[%[@Houtt|@Hregout]
- |whd in ⊢ (??%?); @Vector_eq >(get_moves_cons … ltj)
+ |whd in ⊢ (??%?); @Vector_eq >(vec_moves_cons … lttj)
>tape_moves_def >pmap_vec_cons @eq_f2
- [<H10 [>aa1 @Hrboutt |@lt_to_le @ltj |@le_n]
+ [<H10 [>aa1 @Hrboutt |@ltj |@le_n]
|<tape_moves_def <H9 (* mitico *) @eq_f
@(eq_vec … (niltape ?)) #i #ltij
>(nth_readback … ltij) >(nth_readback … ltij) @Hrbid
(* include "turing/auxiliary_machines.ma". *)
include "turing/multi_to_mono/shift_trace.ma".
-include "turing/multi_universal/normalTM.ma". (* for DeqMove *)
(******************************************************************************)
qed.
definition guarded_M ≝ λsig,n,i,M.
- (ifTM ? (test_char ? (no_blank sig n i))
+ (ifTM ? (test_char ? (not_blank sig n i))
M
- (ifTM ? (mtestR ? (no_blank sig n i))
+ (ifTM ? (mtestR ? (not_blank sig n i))
M
(nop ?) (mtestR_acc …)) tc_true).
definition R_guarded_M ≝ λsig,n,i,RM,t1,t2.
∀ls,a,rs. t1 = midtape ? ls a rs →
- (no_blank sig n i a = false →
- no_blank sig n i (hd ? rs (all_blank …)) = false → t1=t2) ∧
- (no_blank sig n i a = true ∨
- no_blank sig n i (hd ? rs (all_blank …)) = true → RM t1 t2).
+ (not_blank sig n i a = false →
+ not_blank sig n i (hd ? rs (all_blanks …)) = false → t1=t2) ∧
+ (not_blank sig n i a = true ∨
+ not_blank sig n i (hd ? rs (all_blanks …)) = true → RM t1 t2).
lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM →
guarded_M sig n i M ⊨ R_guarded_M sig n i RM.
[#Ht1 * #t2 * * #_ #Ht2 lapply (Ht2 … Ht1) -Ht2 #Ht2
whd in ⊢ (%→?); #Htout % [//] *
[>Ha [#H destruct (H)| >Ht1 %]
- |whd in ⊢ (??%?→?); >blank_all_blank whd in ⊢ (??%?→?);
+ |whd in ⊢ (??%?→?); >blank_all_blanks whd in ⊢ (??%?→?);
#H destruct (H)
]
|#c #rs1 #Ht1 * #t2 * * #Ht2 #_ lapply (Ht2 … Ht1) -Ht2 *
]
qed.
-definition move_R_i ≝ λsig,n,i. guarded_M sig n i (mtiL sig n i).
+definition move_R_i ≝ λA,sig,n,i.
+ guarded_M ? (S n) i (mtiL A sig n i).
-definition Rmove_R_i ≝ λsig,n,i. R_guarded_M sig n i (Rmtil sig n i).
+definition Rmove_R_i ≝ λA,sig,n,i.
+ R_guarded_M ? (S n) i (Rmtil A sig n i).
(*************************** readback of the tape *****************************)
* * normalize /2/ qed.
lemma no_blank_true_to_not_blank: ∀sig,n,a,i.
- (no_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
+ (not_blank sig n i a = true) → nth i ? (vec … n a) (blank sig) ≠ blank ?.
#sig #n #a #i #H @(not_to_not … (eqnot_to_noteq … false H))
-H #H normalize >H %
qed.
-lemma rb_move_R : ∀sig,n,ls,a,rs,outt,i.
- (∀i.regular_trace sig n a ls rs i) →
- nth n ? (vec … a) (blank ?) = head ? →
+lemma rb_move_R : ∀A,sig,n,ls,a,rs,outt,i.
+ (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
+ is_head ?? (nth n ? (vec … a) (blank ?)) = true →
no_head_in … ls →
no_head_in … rs →
Rmove_R_i … i (midtape ? ls a rs) outt →
∃ls1,a1,rs1.
outt = midtape ? ls1 a1 rs1 ∧
- (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
- rb_trace_i sig n ls1 (vec … a1) rs1 i =
- tape_move ? (rb_trace_i sig n ls (vec … a) rs i) R ∧
- ∀j. j ≤n → j ≠ i →
- rb_trace_i sig n ls1 (vec … a1) rs1 j =
- rb_trace_i sig n ls (vec … a) rs j.
-#sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
+ (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
+ tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
+ ∀j. j ≤ n → j ≠ i →
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
+ rb_trace_i ? (S n) ls (vec … a) rs j.
+#A #sig #n #ls #a #rs #outt #i #Hreg #Hha #Hhls #Hhrs #Hmove
lapply (Hmove … (refl …)) -Hmove * #HMove1 #HMove2
-cases (true_or_false (no_blank sig n i a ∨
- no_blank sig n i (hd (multi_sig sig n) rs (all_blank sig n))))
+cases (true_or_false (not_blank ? (S n) i a ∨
+ not_blank ? (S n) i (hd ? rs (all_blanks ? (S n)))))
[2: #Hcase cases (orb_false_l … Hcase) -Hcase #Hb1 #Hb2
lapply (HMove1 … Hb1 Hb2) #Hout %{ls} %{a} %{rs}
%[%[%[@sym_eq @Hout |@Hreg]
|>rb_trace_i_def
- cut (nth i ? (vec … a) (blank ?) = blank sig)
+ cut (nth i ? (vec … a) (blank ?) = blank ?)
[@(\P ?) @injective_notb @Hb1] #Ha >Ha
>rb_trace_def whd in match (opt_cur ??);
- cut (to_blank sig (trace sig n i rs) = [])
+ cut (to_blank ? (trace ? (S n) i rs) = [])
[@daemon] #Hrs >Hrs
- cases (to_blank sig (trace sig n i ls)) //
+ cases (to_blank ? (trace ? (S n) i ls)) //
]
|//]
|-HMove1 #Hb
lapply(HMove2 (orb_true_l … Hb) … (refl …) Hha Hreg ? Hhls Hhrs) -HMove2
- [#Hb1 lapply Hb -Hb whd in match (no_blank sig n i a);
+ [#Hb1 lapply Hb -Hb whd in match (not_blank ? (S n) i a);
>Hb1 #H @no_blank_true_to_not_blank @H]
* #ls1 * #a1 * #rs1 * * * * * #H1 #H2 #H3 #H4 #H5 #H6
%{ls1} %{a1} %{rs1}
%[%[%[@H1|@H2]
|(* either a is blank or not *)
- cases (true_or_false (no_blank sig n i a)) #Hba
+ cases (true_or_false (not_blank ? (S n) i a)) #Hba
[(* a not blank *)
>rb_trace_i_def >rb_trace_def <to_blank_i_def >H5 >to_blank_cons_nb
[2: @no_blank_true_to_not_blank //]
lapply H6 -H6 #Hrs >(rb_trace_i_def … rs i) >rb_trace_def
<(to_blank_i_def … rs) <Hrs
- cut (opt_cur sig (nth i ? (vec … a) (blank sig)) =
- Some ? (nth i ? (vec … a) (blank sig))) [@daemon] #Ha >Ha
+ cut (opt_cur ? (nth i ? (vec … a) (blank ?)) =
+ Some ? (nth i ? (vec … a) (blank ?))) [@daemon] #Ha >Ha
(* either a1 is blank or not *)
- cases (true_or_false (no_blank sig n i a1)) #Hba1
- [cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) =
- Some ? (nth i ? (vec … a1) (blank sig))) [@daemon] #Ha1 >Ha1
+ cases (true_or_false (not_blank ? (S n) i a1)) #Hba1
+ [cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
+ Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] #Ha1 >Ha1
>to_blank_cons_nb [%|@(\Pf ?) @injective_notb @Hba1]
- |cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) = None ?) [@daemon]
+ |cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) = None ?) [@daemon]
#Ha1 >Ha1
cut (to_blank_i … i (a1::rs1) = [ ]) [@daemon] #Ha1rs1 >Ha1rs1
cut (to_blank_i … i rs1 = [ ]) [@daemon] #Hrs1 <to_blank_i_def >Hrs1 %
>rb_trace_i_def >rb_trace_def <(to_blank_i_def … rs) <H6 >H5
cut (to_blank_i … i (a::ls) = [ ]) [@daemon] #Hals >Hals
cut (to_blank_i … i ls = [ ]) [@daemon] #Hls <(to_blank_i_def … ls) >Hls
- cut (opt_cur sig (nth i ? (vec … a) (blank sig)) = None ?) [@daemon] #Ha >Ha
+ cut (opt_cur ? (nth i ? (vec … a) (blank ?)) = None ?) [@daemon] #Ha >Ha
cut (nth i ? (vec … a1) (blank ?) ≠ blank ?) [@daemon] #Ha1
>(to_blank_cons_nb … Ha1)
- cut (opt_cur sig (nth i ? (vec … a1) (blank sig)) =
- Some ? (nth i ? (vec … a1) (blank sig))) [@daemon] -Ha1 #Ha1 >Ha1 %
+ cut (opt_cur ? (nth i ? (vec … a1) (blank ?)) =
+ Some ? (nth i ? (vec … a1) (blank ?))) [@daemon] -Ha1 #Ha1 >Ha1 %
]
]
|(* case j ≠ i *)
#j #Hle #Hneq >rb_trace_i_def >rb_trace_i_def >rb_trace_def >rb_trace_def
<(to_blank_i_def … rs) <(to_blank_i_def … rs1) >(H4 j Hle Hneq)
- cut ((to_blank_i sig n j ls1 = to_blank_i sig n j ls) ∧
- (opt_cur sig (nth j (sig_ext sig) (vec … a1) (blank sig)) =
- opt_cur sig (nth j (sig_ext sig) (vec … a) (blank sig))))
- [@daemon] * #H7 #H8 >H7 >H8 //
+ cut ((to_blank_i ? (S n) j ls1 = to_blank_i ? (S n) j ls) ∧
+ (opt_cur ? (nth j ? (vec … a1) (blank ?)) =
+ opt_cur ? (nth j ? (vec … a) (blank ?))))
+ [@daemon] * #H7 #H8 <to_blank_i_def >H7 >H8 //
]
]
qed.
-definition Rmove_R_i_rb ≝ λsig,n,i,t1,t2.
+definition Rmove_R_i_rb ≝ λA,sig,n,i,t1,t2.
∀ls,a,rs.
t1 = midtape ? ls a rs →
- (∀i.regular_trace sig n a ls rs i) →
- nth n ? (vec … a) (blank ?) = head ? →
+ (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
+ is_head ?? (nth n ? (vec … a) (blank ?)) = true →
no_head_in … ls →
no_head_in … rs →
∃ls1,a1,rs1.
- t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
- (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
- rb_trace_i sig n ls1 (vec … a1) rs1 i =
- tape_move ? (rb_trace_i sig n ls (vec … a) rs i) R ∧
- ∀j. j ≤n → j ≠ i →
- rb_trace_i sig n ls1 (vec … a1) rs1 j =
- rb_trace_i sig n ls (vec … a) rs j.
-
-lemma sem_move_R_i : ∀sig,n,i.i < n →
- move_R_i sig n i ⊨ Rmove_R_i_rb sig n i.
-#sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i sig n i))
+ t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
+ (∀i.regular_trace (TA A sig) (S n) a1 ls1 rs1 i) ∧
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
+ tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) R ∧
+ ∀j. j ≤ n → j ≠ i →
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
+ rb_trace_i ? (S n) ls (vec … a) rs j.
+
+lemma sem_move_R_i : ∀A,sig,n,i.i < n →
+ move_R_i A sig n i ⊨ Rmove_R_i_rb A sig n i.
+#A #sig #n #i #ltin @(Realize_to_Realize … (Rmove_R_i A sig n i))
[#t1 #t2 #H #ls #a #rs #H1 #H2 #H3 #H4 #H5 @rb_move_R // <H1 //
|@sem_R_guarded @sem_Rmtil //
]
(* move_L_i axiomatized *)
-axiom move_L_i : ∀sig.∀n,i:nat.TM (multi_sig sig n).
+axiom move_L_i : ∀A,sig.∀n,i:nat.TM (MTA A sig (S n)).
-definition Rmove_L_i_rb ≝ λsig,n,i,t1,t2.
+definition Rmove_L_i_rb ≝ λA,sig,n,i,t1,t2.
∀ls,a,rs.
t1 = midtape ? ls a rs →
- (∀i.regular_trace sig n a ls rs i) →
- nth n ? (vec … a) (blank ?) = head ? →
+ (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
+ is_head ?? (nth n ? (vec … a) (blank ?)) = true →
no_head_in … ls →
no_head_in … rs →
∃ls1,a1,rs1.
- t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
- (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
- rb_trace_i sig n ls1 (vec … a1) rs1 i =
- tape_move ? (rb_trace_i sig n ls (vec … a) rs i) L ∧
- ∀j. j ≤n → j ≠ i →
- rb_trace_i sig n ls1 (vec … a1) rs1 j =
- rb_trace_i sig n ls (vec … a) rs j.
+ t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
+ (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
+ tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) L ∧
+ ∀j. j ≤ n → j ≠ i →
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
+ rb_trace_i ? (S n) ls (vec … a) rs j.
-axiom sem_move_L_i : ∀sig,n,i.i < n →
- move_L_i sig n i ⊨ Rmove_L_i_rb sig n i.
+axiom sem_move_L_i : ∀A,sig,n,i.i < n →
+ move_L_i A sig n i ⊨ Rmove_L_i_rb A sig n i.
(*
lemma rb_move_L : ∀sig,n,ls,a,rs,outt,i.
(* The following function read a move from a vector of moves and executes it *)
-axiom get_move : ∀sig.∀n.∀a:multi_sig sig n.nat → DeqMove.
+(* The head character contains a state and a sequence of moves *)
+
+definition HC ≝ λQ,n.FinProd Q (FinVector FinMove n).
-definition exec_move_i ≝ λsig,n,i.
- (ifTM ? (test_char ? (λa. (get_move sig n a i == R)))
- (move_R_i sig n i)
- (ifTM ? (test_char ? (λa. (get_move sig n a i == L)))
- (move_L_i sig n i)
+let rec all_N n on n : FinVector FinMove n ≝
+ match n with
+ [ O ⇒ Vector_of_list ? []
+ | S m ⇒ vec_cons ? N m (all_N m)
+ ].
+
+definition get_moves ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).
+ match nth n ? (vec … a) (blank ?) with
+ [ None ⇒ all_N n
+ | Some x ⇒ match x with
+ [inl y ⇒ snd ?? y
+ |inr y ⇒ all_N n]].
+
+definition get_move ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λi.
+ nth i ? (vec … (get_moves Q sig n a)) N.
+
+definition exec_move_i ≝ λQ,sig,n,i.
+ (ifTM ? (test_char ? (λa. (get_move Q sig n a i == R)))
+ (move_R_i (HC Q n) sig n i)
+ (ifTM ? (test_char ? (λa. (get_move Q sig n a i == L)))
+ (move_L_i (HC Q n) sig n i)
(nop ?) tc_true) tc_true).
-
-definition R_exec_move_i ≝ λsig,n,i,t1,t2.
+
+definition R_exec_move_i ≝ λQ,sig,n,i,t1,t2.
∀a,ls,rs.
- t1 = midtape ? ls a rs →
- (∀i.regular_trace sig n a ls rs i) →
- nth n ? (vec … a) (blank ?) = head ? →
+ t1 = midtape (MTA (HC Q n) sig (S n)) ls a rs →
+ (∀i.regular_trace ? (S n) a ls rs i) →
+ is_head ?? (nth n ? (vec … a) (blank ?)) = true →
no_head_in … ls →
no_head_in … rs →
∃ls1,a1,rs1.
- t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
- (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
- rb_trace_i sig n ls1 (vec … a1) rs1 i =
- tape_move ? (rb_trace_i sig n ls (vec … a) rs i) (get_move sig n a i) ∧
- ∀j. j ≤n → j ≠ i →
- rb_trace_i sig n ls1 (vec … a1) rs1 j =
- rb_trace_i sig n ls (vec … a) rs j.
+ t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
+ (∀i.regular_trace ? (S n) a1 ls1 rs1 i) ∧
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 i =
+ tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs i) (get_move Q sig n a i) ∧
+ ∀j. j ≤ n → j ≠ i →
+ rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
+ rb_trace_i ? (S n) ls (vec … a) rs j.
lemma tape_move_N: ∀A,t. tape_move A t N = t.
// qed.
-lemma sem_exec_move_i: ∀sig,n,i. i < n →
- exec_move_i sig n i ⊨ R_exec_move_i sig n i.
-#sig #n #i #ltin
+lemma sem_exec_move_i: ∀Q,sig,n,i. i < n →
+ exec_move_i Q sig n i ⊨ R_exec_move_i Q sig n i.
+#Q #sig #n #i #ltin
@(sem_if_app … (sem_test_char …)
- (sem_move_R_i … ltin)
+ (sem_move_R_i … ltin)
(sem_if … (sem_test_char …)
(sem_move_L_i … ltin) (sem_nop ?)))
#tin #tout #t1 *
[* * * #c * #Hc #HR #Ht1 #HMR
#a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
- >(\P HR) @HMR >Ht1 @Htin
+ >(\P HR) whd in HMR; @HMR >Ht1 @Htin
|* * #HR #Ht1 >Ht1 *
[* #t2 * * * #c * #Hc #HL #Ht2 #HML
#a #ls #rs #Htin >Htin in Hc; whd in ⊢ (??%?→?); #H destruct (H)
>(\P HL) @HML >Ht2 @Htin
|* #t2 * * #HL #Ht2 >Ht2 whd in ⊢ (%→?); #Htout >Htout
#a #ls #rs #Htin >Htin in HR; #HR >Htin in HL; #HL
- cut (get_move sig n a i = N)
+ cut (get_move Q sig n a i = N)
[lapply (HR a (refl … )) lapply (HL a (refl … ))
- cases (get_move sig n a i) normalize
+ cases (get_move Q sig n a i) normalize
[#H destruct (H) |#_ #H destruct (H) | //]]
#HN >HN >tape_move_N #Hreg #_ #_ #_
%{ls} %{a} %{rs}
]
qed.
-axiom reg_inv : ∀sig,n,a,ls,rs,a1,ls1,rs1.
- regular_trace sig n a1 ls1 rs1 n →
- (rb_trace_i sig n ls1 (vec … a1) rs1 n =
- rb_trace_i sig n ls (vec … n a) rs n) →
- nth n ? (vec … a) (blank ?) = head ? →
+axiom reg_inv : ∀A,sig,n,a,ls,rs,a1,ls1,rs1.
+ regular_trace (TA A sig) (S n) a1 ls1 rs1 n →
+ (rb_trace_i ? (S n) ls1 (vec … a1) rs1 n =
+ rb_trace_i ? (S n) ls (vec … a) rs n) →
+ is_head ?? (nth n ? (vec … (S n) a) (blank ?)) = true →
no_head_in … ls →
no_head_in … rs →
- nth n ? (vec … a1) (blank ?) = head ? ∧
+ is_head ?? (nth n ? (vec … a1) (blank ?)) = true ∧
no_head_in … ls1 ∧ no_head_in … rs1.
(hd ? (ls1@b::ls2) (all_blanks …)) (tail ? (ls1@b::ls2)) rs j) ∧
(not_blank sig n i b = false) ∧
(hd (multi_sig sig n) (ls1@[b]) (all_blanks …) = a) ∧ (* not implied by the next fact *)
- (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
+ (∀j.j < n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
theorem sem_move_to_blank_L: ∀sig,n,i.
[ inl _ ⇒ false
| inr _ ⇒ true]].
-definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) n.
+definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) (S n).
¬(is_head A sig (nth n ? (vec … c) (blank ?))).
+lemma not_head_all_blanks : ∀A,sig,n.
+ not_head A sig n (all_blanks … (S n)) = true.
+#A #sig #n whd in ⊢ (??%?); >blank_all_blanks //
+qed.
+
definition no_head_in ≝ λA,sig,n,l.
- ∀x. mem ? x (trace (TA A sig) n n l) → is_head … x = false.
+ ∀x. mem ? x (trace (TA A sig) (S n) n l) → is_head … x = false.
(*
lemma not_head_true: ∀A,sig,n,c. not_head A sig n c = true →
is_head … (nth n ? (vec … c) (blank ?)) = false.
*)
+lemma hd_nil : ∀A,d. hd A [ ] d = d.
+// qed.
+
definition mtiL ≝ λA,sig,n,i.
- move_to_blank_L (TA A sig) n i ·
- shift_i_L (TA A sig) n i ·
+ move_to_blank_L (TA A sig) (S n) i ·
+ shift_i_L (TA A sig) (S n) i ·
move_until ? L (not_head A sig n).
definition Rmtil ≝ λA,sig,n,i,t1,t2.
∀ls,a,rs.
- t1 = midtape (MTA A sig n) ls a rs →
+ t1 = midtape (MTA A sig (S n)) ls a rs →
is_head A sig (nth n ? (vec … a) (blank ?)) = true →
- (∀i.regular_trace (TA A sig) n a ls rs i) →
+ (∀i.regular_trace (TA A sig) (S n) a ls rs i) →
(* next: we cannot be on rightof on trace i *)
(nth i ? (vec … a) (blank ?) = (blank ?)
→ nth i ? (vec … (hd ? rs (all_blanks …))) (blank ?) ≠ (blank ?)) →
no_head_in … ls →
no_head_in … rs →
(∃ls1,a1,rs1.
- t2 = midtape (MTA A sig n) ls1 a1 rs1 ∧
+ t2 = midtape (MTA A sig (S n)) ls1 a1 rs1 ∧
(∀i.regular_trace … a1 ls1 rs1 i) ∧
- (∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
- (∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
- (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
- (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
+ (∀j. j ≤ n → j ≠ i → to_blank_i ? (S n) j (a1::ls1) = to_blank_i ? (S n) j (a::ls)) ∧
+ (∀j. j ≤ n → j ≠ i → to_blank_i ? (S n) j rs1 = to_blank_i ? (S n) j rs) ∧
+ (to_blank_i ? (S n) i ls1 = to_blank_i ? (S n) i (a::ls)) ∧
+ (to_blank_i ? (S n) i (a1::rs1)) = to_blank_i ? (S n) i rs).
theorem sem_Rmtil: ∀A,sig,n,i. i < n → mtiL A sig n i ⊨ Rmtil A sig n i.
#A #sig #n #i #lt_in
(* we start looking into Rmitl *)
#ls #a #rs #Htin (* tin is a midtape *)
#Hheada #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
-cut (regular_i ? n (a::ls) i)
+cut (regular_i ? (S n) (a::ls) i)
[cases (Hreg i) * //
cases (true_or_false (nth i ? (vec … a) (blank ?) == (blank ?))) #Htest
[#_ @daemon (* absurd, since hd rs non e' blank *)
* #H3 @False_ind @(absurd (true=false)) [2://] <H3 @sym_eq
<(notb_notb true) @(eq_f … notb) @Hnohead_rs >H2 >trace_append @mem_append_l2
lapply Hb0 cases rs2
- [whd in match (hd ???); #H >H in H3; whd in match (not_head ????);
- >all_blank_n normalize -H #H destruct (H); @False_ind
+ [>hd_nil #H >H in H3; >not_head_all_blanks #Habs destruct (Habs)
|#c #r #H4 %1 >H4 //
]
|*
(* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
* #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
cut (∀j.j ≠ i →
- trace ? n j (reverse (multi_sig (TA A sig) n) rs1@b::ls2) =
- trace ? n j (ls10@a1::ls20))
+ trace ? (S n) j (reverse (multi_sig (TA A sig) (S n)) rs1@b::ls2) =
+ trace ? (S n) j (ls10@a1::ls20))
[#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
- lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
+ lapply (trace_shift_neq … (le_S … lt_in) ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
<(trace_def … (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
#Htracej
- cut (trace ? n i (reverse (multi_sig (TA A sig) n) (rs1@[b0])@ls2) =
- trace ? n i (ls10@a1::ls20))
+ cut (trace ? (S n) i (reverse (multi_sig (TA A sig) (S n)) (rs1@[b0])@ls2) =
+ trace ? (S n) i (ls10@a1::ls20))
[>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
- cut (trace ? n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
- lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
+ cut (trace ? (S n) i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
+ lapply (trace_shift … (le_S … lt_in) … Hrss) [//] whd in match (tail ??); #Htr <Htr
>reverse_map >map_append <trace_def <Hls20 %
]
#Htracei
cut (∀j. j ≠ i →
- (trace ? n j (reverse (MTA A sig n) rs11) = trace ? n j ls10) ∧
- (trace ? n j (ls1@b::ls2) = trace ? n j (a1::ls20)))
+ (trace ? (S n) j (reverse (MTA A sig (S n)) rs11) = trace ? (S n) j ls10) ∧
+ (trace ? (S n) j (ls1@b::ls2) = trace ? (S n) j (a1::ls20)))
[@daemon (* si fa
#j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
[lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
>trace_def in ⊢ (%→?); <map_append #H @H
| *) ] #H2
- cut ((trace ? n i (b0::reverse ? rs11) = trace ? n i (ls10@[a1])) ∧
- (trace ? n i (ls1@ls2) = trace ? n i ls20))
+ cut ((trace ? (S n) i (b0::reverse ? rs11) = trace ? (S n) i (ls10@[a1])) ∧
+ (trace ? (S n) i (ls1@ls2) = trace ? (S n) i ls20))
[>H1 in Htracei; >reverse_append >reverse_single >reverse_append
>reverse_reverse >associative_append >associative_append
@daemon
] #H3
cut (∀j. j ≠ i →
- trace ? n j (reverse (MTA A sig n) ls10@rs2) = trace ? n j rs)
- [#j #jneqi @(injective_append_l … (trace ? n j (reverse ? ls1)))
+ trace ? (S n) j (reverse ? ls10@rs2) = trace ? (S n) j rs)
+ [#j #jneqi @(injective_append_l … (trace ? (S n) j (reverse ? ls1)))
>map_append >map_append >Hrs1 >H1 >associative_append
<map_append <map_append in ⊢ (???%); @eq_f
<map_append <map_append @eq_f2 // @sym_eq
<(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
@eq_f @(proj1 … (H2 j jneqi))] #Hrs_j
- %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (MTA A sig n) rs2)}
+ %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail ? rs2)}
%[%[%[%[%[@Htout
|#j cases (decidable_eq_nat j i)
[#eqji >eqji (* by cases wether a1 is blank *)
|@sym_eq @Hrs_j //
]
]]
- |#j #lejn #jneqi <(Hls1 … lejn)
+ |#j #lejn #jneqi <(Hls1 … (le_S_S … lejn))
>to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
|#j #lejn #jneqi >reverse_cons >associative_append >Hb0
<to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f @Hrs_j //]
- |<(Hls1 i) [2:@lt_to_le //]
+ |<(Hls1 i) [2:@le_S //]
lapply (all_blank_after_blank … reg_ls1_i)
[@(\P ?) @daemon] #allb_ls2
whd in match (to_blank_i ????); <(proj2 … H3)
@daemon ]
|>reverse_cons >associative_append
- cut (to_blank_i ? n i rs = to_blank_i ? n i (rs11@[b0])) [@daemon]
+ cut (to_blank_i ? (S n) i rs = to_blank_i ? (S n) i (rs11@[b0])) [@daemon]
#Hcut >Hcut >(to_blank_i_chop … b0 (a1::reverse …ls10)) [2: @Hb0blank]
>to_blank_i_def >to_blank_i_def @eq_f
>trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
]
|(*we do not find the head: this is absurd *)
* #b1 * #lss * * #H2 @False_ind
- cut (∀x0. mem ? x0 (trace ? n n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
+ cut (∀x0. mem ? x0 (trace ? (S n) n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
[@daemon] -H2 #H2
- lapply (trace_shift_neq ? n i n … lt_in … Hrss)
+ lapply (trace_shift_neq ? (S n) i n … (le_S … lt_in) … Hrss)
[@lt_to_not_eq @lt_in | // ]
#H3 @(absurd
- (is_head … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … n))) (blank ?)) = true))
+ (is_head … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … (S n)))) (blank ?)) = true))
[>Hhead //
|@eqnot_to_noteq @H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
>H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
qed.
axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
- (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
+ (∀i. i < n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
lemma to_blank_i_ext : ∀sig,n,i,l.
to_blank_i sig n i l = to_blank_i sig n i (l@[all_blanks …]).
include "turing/multi_universal/alphabet.ma".
include "turing/mono.ma".
-(************************* turning DeqMove into a DeqSet **********************)
-definition move_eq ≝ λm1,m2:move.
- match m1 with
- [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
- |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
- |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
-
-lemma move_eq_true:∀m1,m2.
- move_eq m1 m2 = true ↔ m1 = m2.
-*
- [* normalize [% #_ % |2,3: % #H destruct ]
- |* normalize [1,3: % #H destruct |% #_ % ]
- |* normalize [1,2: % #H destruct |% #_ % ]
-qed.
-
-definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
-
-unification hint 0 ≔ ;
- X ≟ DeqMove
-(* ---------------------------------------- *) ⊢
- move ≡ carr X.
-
-unification hint 0 ≔ m1,m2;
- X ≟ DeqMove
-(* ---------------------------------------- *) ⊢
- move_eq m1 m2 ≡ eqb X m1 m2.
-
-
-(************************ turning DeqMove into a FinSet ***********************)
-definition move_enum ≝ [L;R;N].
-
-lemma move_enum_unique: uniqueb ? [L;R;N] = true.
-// qed.
-
-lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
-* // qed.
-
-definition FinMove ≝
- mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
-
-unification hint 0 ≔ ;
- X ≟ FinMove
-(* ---------------------------------------- *) ⊢
- move ≡ FinSetcarr X.
-
(*************************** normal Turing Machines ***************************)
(* A normal turing machine is just an ordinary machine where:
projects / helm.git / commitdiff