From aa900a8d853f1040716bb050e38406463de08271 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 24 Oct 2013 10:54:17 +0000 Subject: [PATCH] step (almost) done --- .../lib/turing/multi_to_mono/exec_moves.ma | 93 +++---------------- .../turing/multi_to_mono/exec_trace_move.ma | 80 ++++++++++++++-- .../matita/lib/turing/multi_to_mono/step.ma | 56 +++++++---- 3 files changed, 126 insertions(+), 103 deletions(-) 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 dae4aa6af..9f6cb718b 100644 --- a/matita/matita/lib/turing/multi_to_mono/exec_moves.ma +++ b/matita/matita/lib/turing/multi_to_mono/exec_moves.ma @@ -2,75 +2,6 @@ include "turing/multi_to_mono/exec_trace_move.ma". (* include "turing/turing.ma". *) - -(**************************** 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 @@ -131,15 +62,18 @@ definition R_exec_moves ≝ λQ,sig,n,i,t1,t2. ∃ls1,a1,rs1. 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 → + (∀j. j < i → j ≤ n → + rb_trace_i ? (S n) ls1 (vec … a1) rs1 j = + tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs j) (get_move Q sig n a j)) ∧ + (* 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 ? (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)". *) +(* lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j → nth i ? (readback sig n ls a rs j) (niltape ?) = rb_trace_i sig n ls a rs (j - S i). @@ -150,14 +84,14 @@ lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j → |#m #Hmj >minus_S_S @Hind @le_S_S_to_le // ] ] -qed. +qed. *) 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]| %]|//] + %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| #j #ltjO @False_ind /2/]|//] |#j #Hind #lttj lapply (lt_to_le … lttj) #ltj @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind #int #outt * #t1 * #H1 #H2 @@ -173,13 +107,10 @@ lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n → cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i) [@daemon] #aa1 %[%[%[@Houtt|@Hregout] - |whd in ⊢ (??%?); @Vector_eq >(vec_moves_cons … lttj) - >tape_moves_def >pmap_vec_cons @eq_f2 - [aa1 @Hrboutt |@ltj |@le_n] - |(nth_readback … ltij) >(nth_readback … ltij) @Hrbid - [@(transitive_le … ltj) // |@lt_to_not_eq @lt_plus_to_minus //] + |#k #ltk cases (le_to_or_lt_eq … ltk) #Hk #lekn + [>(Hrbid … lekn) [2:@lt_to_not_eq @le_S_S_to_le @Hk] + @(H9 k ? lekn) @le_S_S_to_le @Hk + |destruct (Hk) (Hrbid … Han) 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 0fdfa86b8..4c4ee013d 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 @@ -117,7 +117,71 @@ definition move_R_i ≝ λA,sig,n,i. definition Rmove_R_i ≝ λA,sig,n,i. R_guarded_M ? (S n) i (Rmtil A sig n i). +(**************************** 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_n: ∀A.∀a:A.∀n.∀v:Vector A n.∀d. + nth n ? (vec_cons_right A a n v) d = a. + +axiom nth_cons_right_lt: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.∀i. i < n → + nth i ? (vec_cons_right A a n v) d = nth i ? v d. +(* +#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 ????); +*) + +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. (*************************** readback of the tape *****************************) definition opt_cur ≝ λsig,a. @@ -139,12 +203,10 @@ lemma rb_trace_i_def: ∀sig,n,ls,a,rs,i. rb_trace sig (trace ? n i ls) (nth i ? a (blank ?)) (trace ? n i rs). // qed. -let rec readback sig n ls a rs i on i : Vector (tape (sig_ext sig)) i ≝ - match i with - [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??) - | S j ⇒ vec_cons ? (rb_trace_i sig n ls a rs j) j (readback sig n ls a rs j) - ]. - +(* +definition readback :∀sig,n,ls,a,rs,i.Vector (tape (sig_ext sig)) i ≝ +vec_map (rb_trace_i *) + lemma orb_false_l: ∀b1,b2:bool. (b1 ∨ b2) = false → (b1 = false) ∧ (b2 = false). * * normalize /2/ qed. @@ -316,6 +378,12 @@ definition get_moves ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S 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. + +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_n // +qed. definition exec_move_i ≝ λQ,sig,n,i. (ifTM ? (test_char ? (λa. (get_move Q sig n a i == R))) diff --git a/matita/matita/lib/turing/multi_to_mono/step.ma b/matita/matita/lib/turing/multi_to_mono/step.ma index 2defb7c40..fb133e747 100644 --- a/matita/matita/lib/turing/multi_to_mono/step.ma +++ b/matita/matita/lib/turing/multi_to_mono/step.ma @@ -113,9 +113,25 @@ definition to_sig_tape ≝ λQ,sig,t. | Some x ⇒ midtape ? (to_sig_map Q sig ls) x (to_sig_map Q sig rs) ] ]. -definition rb_tapes ≝ λQ,sig,n,ls.λa:MTA Q sig (S n).λrs. - vec_map ?? (to_sig_tape ??) n (readback ? (S n) ls (vec … a) rs n). - +let rec rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs i on i ≝ + match i with + [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??) + | S j ⇒ vec_cons_right ? (to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs j)) j + (rb_tapes Q sig n ls a rs j)]. + +lemma nth_rb_tapes : ∀Q,sig,n,ls.∀a:MTA Q sig (S n).∀rs,j,i. i < j → + nth i ? (rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs j) (niltape ?) = + to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs i). +#Q #sig #n #ls #a #rs #j elim j + [#i #H @False_ind /2/ + |#k #Hind #i #lti cases (le_to_or_lt_eq … (le_S_S_to_le … lti)) + [#Hlt >nth_cons_right_lt [@Hind //|//] + |#Heq >Heq @nth_cons_right_n + ] + ] +qed. + + (* q0 is a default value *) definition get_state ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λq0. match nth n ? (vec … a) (blank ?) with @@ -139,7 +155,7 @@ definition readback_config ≝ λQ,sig,n,q0,ls.λa:MTA (HC Q (S n)) sig (S (S n)).λrs. mk_mconfig sig Q n (get_state Q sig (S n) a q0) - (rb_tapes (HC Q (S n)) sig (S n) ls a rs). + (rb_tapes (HC Q (S n)) sig (S n) ls a rs (S n)). lemma state_readback : ∀Q,sig,n,q0,ls,a,rs. cstate … (readback_config Q sig n q0 ls a rs) = @@ -148,7 +164,7 @@ lemma state_readback : ∀Q,sig,n,q0,ls,a,rs. lemma tapes_readback : ∀Q,sig,n,q0,ls,a,rs. ctapes … (readback_config Q sig n q0 ls a rs) = - rb_tapes (HC Q (S n)) sig (S n) ls a rs. + rb_tapes (HC Q (S n)) sig (S n) ls a rs (S n). // qed. definition R_stepM ≝ λsig.λn.λM:mTM sig n.λt1,t2. @@ -241,7 +257,11 @@ axiom to_sig_write : ∀Q,sig,n,t,c. (tape_write ? t (to_sig_conv ??? c)) = tape_write sig (to_sig_tape ?? t) c. +definition opt ≝ λA.λoc1: option A.λc2. + match oc1 with [None ⇒ c2 | Some c1 ⇒ c1]. + axiom rb_write: ∀sig,n,ls,a,rs,i,c1,c2. + nth i ? c1 (None ?) = opt ? c2 (nth i ? c1 (None ?)) → rb_trace_i ? n ls c1 rs i = tape_write ? (rb_trace_i sig n ls a rs i) c2. @@ -265,7 +285,7 @@ lapply (transf_eq … HaSn (refl ??) (refl ??) (eq_pair_fst_snd …) (refl ??) ( *) lapply (Hmoves … Ht1 ?? H3 H4) [>(transf_eq … HaSn (refl ??) (refl ??) (eq_pair_fst_snd …) (refl ??) (refl ??)) - >nth_cons_right % + >nth_cons_right_n % | (* regularity is preserved *) @daemon |* #ls1 * #a1 * #rs1 * * * #Htout #Hreg #Hrb #HtrSn lapply (HtrSn (S n) (le_n ?) (le_n ?)) -HtrSn #HtrSn @@ -282,26 +302,30 @@ lapply (Hmoves … Ht1 ?? H3 H4) [(* state *) >state_readback whd in match (step ????); >(cstate_rb … HaSn) >eq_current_chars_resize >get_chars_def Htrans whd in ⊢ (???%); - whd in ⊢ (??%?); >Ha1 >HaSn >Htransf >nth_cons_right % + whd in ⊢ (??%?); >Ha1 >HaSn >Htransf >nth_cons_right_n % |>tapes_readback whd in match (step ????); >(cstate_rb … HaSn) >eq_current_chars_resize >get_chars_def Htrans >ctapes_mk_config @(eq_vec … (niltape ?)) #i #lti - >nth_vec_map_lt [2:@lti |3:@niltape] - >Hrb tapes_readback - >Htransf whd in match (vec_moves ?????); - >get_moves_cons_right >resize_id [2:@(len ?? moves)] + >nth_rb_tapes [2:@lti] + >Hrb [2:@lt_to_le @lti|3:@lti] + >Htransf whd in match (get_move ?????); (* whd in match (vec_moves ?????); *) + >get_moves_cons_right (* lhs *) nth_vec_map_lt [2:@lti |3:@niltape] - >(eq_pair_fst_snd … (nth i ? actions ?)) + >ctapes_mk_config >nth_rb_tapes [2:@lti] + (* >nth_vec_map_lt [2:@lti |3:@niltape] *) + >(eq_pair_fst_snd … (nth i ? actions ?)) >tape_move_mono_def cut (snd ?? (nth i ? actions 〈None sig,N〉) = nth i ? moves N) [>Hmoves @nth_vec_map] #Hmoves1 >Hmoves1 - >(nth_readback … lti) >(nth_readback … lti) >to_sig_move @eq_f2 [2://] - nth_cons_right_lt [2:@lti] + >Hnew_chars Hcase % |#c #Hcase % ] ] ] ] -- 2.39.2