From 8712a9a43384e0f437e8ea97fd66c8ea4da7bcfe Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 24 Oct 2013 06:48:13 +0000 Subject: [PATCH] many changes --- matita/matita/lib/turing/basic_machines.ma | 20 ++ matita/matita/lib/turing/mono.ma | 46 ++++ .../lib/turing/multi_to_mono/exec_moves.ma | 128 +++++++++-- .../turing/multi_to_mono/exec_trace_move.ma | 217 ++++++++++-------- .../lib/turing/multi_to_mono/shift_trace.ma | 77 ++++--- .../turing/multi_to_mono/trace_alphabet.ma | 2 +- .../lib/turing/multi_universal/normalTM.ma | 45 ---- 7 files changed, 330 insertions(+), 205 deletions(-) diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 1e5fa3d2e..c1559702a 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -41,6 +41,26 @@ lemma sem_write_strong : ∀alpha,c.Realize ? (write alpha c) (R_write_strong al [|% [% |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. diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index e670c2635..393fa2af9 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -79,7 +79,53 @@ qed. 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] ≝ diff --git a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma index 496b84c5f..dae4aa6af 100644 --- a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma +++ b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma @@ -3,18 +3,81 @@ 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. @@ -35,6 +98,20 @@ definition tape_writem ≝ λ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) = @@ -43,21 +120,22 @@ axiom actions_commute : ∀sig,n,ts,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)". *) @@ -74,30 +152,30 @@ lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j → ] 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 - [aa1 @Hrboutt |@lt_to_le @ltj |@le_n] + [aa1 @Hrboutt |@ltj |@le_n] |(nth_readback … ltij) >(nth_readback … ltij) @Hrbid diff --git a/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma b/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma index dc75bc627..0fdfa86b8 100644 --- a/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma +++ b/matita/matita/lib/turing/multi_to_mono/exec_trace_move.ma @@ -1,7 +1,6 @@ (* include "turing/auxiliary_machines.ma". *) include "turing/multi_to_mono/shift_trace.ma". -include "turing/multi_universal/normalTM.ma". (* for DeqMove *) (******************************************************************************) @@ -65,18 +64,18 @@ lemma sem_mtestR: ∀sig,test. 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. @@ -98,7 +97,7 @@ lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ 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 * @@ -112,9 +111,11 @@ lemma sem_R_guarded: ∀sig,n,i,M,RM. M ⊨ RM → ] 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 *****************************) @@ -149,63 +150,63 @@ lemma orb_false_l: ∀b1,b2:bool. * * 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 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) 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 Hrs1 % @@ -214,43 +215,43 @@ cases (true_or_false (no_blank sig n i a ∨ >rb_trace_i_def >rb_trace_def <(to_blank_i_def … rs)
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 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 //

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} @@ -352,14 +371,14 @@ lemma sem_exec_move_i: ∀sig,n,i. i < n → ] 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. diff --git a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma index 016648770..1e5e36e91 100644 --- a/matita/matita/lib/turing/multi_to_mono/shift_trace.ma +++ b/matita/matita/lib/turing/multi_to_mono/shift_trace.ma @@ -96,7 +96,7 @@ definition R_move_to_blank_L ≝ λsig,n,i,t1,t2. (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. @@ -250,39 +250,47 @@ definition is_sig ≝ λA,sig.λc:sig_ext (TA A sig). [ 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 @@ -294,7 +302,7 @@ theorem sem_Rmtil: ∀A,sig,n,i. i < n → mtiL A sig n i ⊨ Rmtil A sig n i. (* 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 *) @@ -329,8 +337,7 @@ lapply (Htout … Ht2) -Htout -Ht2 * * #H3 @False_ind @(absurd (true=false)) [2://]

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 // ] |* @@ -338,43 +345,43 @@ lapply (Htout … Ht2) -Htout -Ht2 * (* 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 trace_def 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 Hcut - lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr Hcut + lapply (trace_shift … (le_S … lt_in) … Hrss) [//] whd in match (tail ??); #Htr reverse_map >map_append trace_def in ⊢ (%→?); trace_def in ⊢ (%→?); 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 eqji (* by cases wether a1 is blank *) @@ -387,17 +394,17 @@ lapply (Htout … Ht2) -Htout -Ht2 * |@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_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 @@ -406,12 +413,12 @@ lapply (Htout … Ht2) -Htout -Ht2 * ] |(*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 H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append diff --git a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma index 2c162745f..52c91909d 100644 --- a/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma +++ b/matita/matita/lib/turing/multi_to_mono/trace_alphabet.ma @@ -252,7 +252,7 @@ lemma to_blank_cons_nb: ∀sig,n,i,a,l. 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 …]). diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma index 6459cedd9..28c3920bc 100644 --- a/matita/matita/lib/turing/multi_universal/normalTM.ma +++ b/matita/matita/lib/turing/multi_universal/normalTM.ma @@ -12,51 +12,6 @@ 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: -- 2.39.2