matita/matita/lib/turing/multi_to_mono/step.ma

   1
   2 include "turing/multi_to_mono/exec_moves.ma".
   3
   4 definition Mono_realize ≝ Realize.
   5
   6 definition to_sig ≝ λQ,sig.λc:sig_ext (TA Q sig).
   7   match c with
   8   [None ⇒ None ?
   9   |Some a ⇒ match a with
  10     [inl x ⇒ None ? (* this is not possible *)
  11     |inr x ⇒ Some ? x]].
  12
  13 definition to_sig_inv ≝ λQ,sig.λc1:(option sig) × move.λc2.
  14   match (fst ?? c1) with
  15   [None ⇒ c2
  16   |Some a ⇒ Some ? (inr Q ? a)].
  17
  18 definition transf ≝ λQ,sig:FinSet.λn.
  19  λt: Q × (Vector (option sig) n) → Q × (Vector ((option sig) × move) n).
  20  λa:MTA (HC Q n) sig (S n).
  21   let qM ≝ nth n ? (vec … a) (blank ?) in
  22   let a1 ≝ resize_vec ? (S n) a n (blank ?) in
  23   let a2 ≝ vec_map ?? (to_sig ? sig) n a1 in
  24   match qM with
  25   [None ⇒ all_blanks (TA (HC Q n) sig) (S n)
  26   |Some p ⇒
  27     match p with
  28     [inl p1 ⇒
  29       let 〈q1,actions〉 ≝ t 〈fst ?? p1, a2〉 in
  30       let moves ≝ vec_map ?? (snd ??) n actions in
  31       let new_chars ≝ pmap_vec ??? (to_sig_inv (HC Q n) ?) n actions a1 in
  32       vec_cons_right ? (Some ? (inl ?? 〈q1,moves〉)) n new_chars
  33     |inr p2 ⇒ all_blanks (TA (HC Q n) sig) (S n)]
  34   ].
  35
  36 lemma transf_eq: ∀Q,sig,n,t.∀a:MTA (HC Q n) sig (S n).
  37   ∀a1,a2,q,m,q1,actions,moves,new_chars.
  38   nth n ? (vec … a) (blank ?) = Some ? (inl ?? 〈q,m〉) →
  39   a1 = resize_vec ? (S n) a n (blank ?) →
  40   a2 = vec_map ?? (to_sig ? sig) n a1 →
  41   t 〈q, a2〉 = 〈q1,actions〉 →
  42   moves = vec_map ?? (snd ??) n actions →
  43   new_chars = pmap_vec ??? (to_sig_inv (HC Q n) ?) n actions a1  →
  44   transf Q sig n t a =
  45     vec_cons_right ? (Some ? (inl ?? 〈q1,moves〉)) n new_chars.
  46 #Q #sig #n #t #a #a1 #a2 #q #m #q1 #actions #moves #new_chars
  47 #Hnth #Ha1 #Ha2 #Ht #Hmoves #Hnew_chars
  48 whd in ⊢ (??%?); >Hnth whd in ⊢ (??%?); <Ha1 <Ha2 >Ht
  49 @eq_cons_right [<Hmoves // |<Hnew_chars // ]
  50 qed.
  51
  52 lemma transf_eq_ex: ∀Q,sig,n,t.∀a:MTA (HC Q n) sig (S n).
  53   ∀q,m.nth n ? (vec … a) (blank ?) = Some ? (inl ?? 〈q,m〉)→
  54   ∃a1.a1 = resize_vec ? (S n) a n (blank ?) ∧
  55   ∃a2. a2 = vec_map ?? (to_sig ? sig) n a1 ∧
  56   ∃q1,actions. t 〈q, a2〉 = 〈q1,actions〉 ∧
  57   ∃moves.moves = vec_map ?? (snd ??) n actions ∧
  58   ∃new_chars.new_chars = pmap_vec ??? (to_sig_inv (HC Q n) ?) n actions a1 ∧
  59   transf Q sig n t a =
  60     vec_cons_right ? (Some ? (inl ?? 〈q1,moves〉)) n new_chars.
  61 #Q #sig #n #t #a #q #m #H
  62 %{(resize_vec ? (S n) a n (blank ?))} % [%]
  63 % [2:% [%] | skip] % [2: % [ 2: % [@eq_pair_fst_snd ] |skip] | skip]
  64 % [2:% [%] | skip] % [2:% [%] | skip] whd in ⊢ (??%?); >H whd in ⊢ (??%?);
  65 >(eq_pair_fst_snd … (t …)) %
  66 qed.
  67
  68 (*
  69 lemma nth_transf: ∀Q,sig,n,t.∀a:MTA (HC Q n) sig (S n).
  70   ∀a1,a2,q,m,q1,actions,moves.
  71   nth n ? (vec … a) (blank ?) = Some ? (inl ?? 〈q,m〉) →
  72   a1 = resize_vec ? (S n) a n (blank ?) →
  73   a2 = vec_map ?? (to_sig ? sig) n a1 →
  74   t 〈q, a2〉 = 〈q1,actions〉 →
  75   moves = vec_map ?? (snd ??) n actions →
  76   nth n ? (vec … (transf Q sig n t a)) (blank ?) = Some ? (inl ?? 〈q1,moves〉).
  77 #Q #sig #n #t #a #a1 #a2 #q #m #q1 #actions #moves
  78 #Hnth #Ha1 #Ha2 #Ht #Hmoves
  79 *)
  80
  81 (*********************************** stepM ************************************)
  82 definition optf ≝ λA,B:Type[0].λf:A →B.λd,oa.
  83   match oa with
  84   [ None ⇒ d
  85   | Some a ⇒ f a ].
  86
  87 lemma optf_Some : ∀A,B,f,a,d. optf A B f d (Some A a) = f a.
  88 // qed.
  89
  90 definition stepM ≝ λQ,sig,n,trans.
  91   writef ? (optf ?? (transf Q sig (S n) trans) (all_blanks …)) ·
  92   exec_moves Q sig (S n) (S n).
  93
  94 let rec to_sig_map Q sig l on l ≝
  95   match l with
  96   [ nil ⇒ nil ?
  97   | cons a tl ⇒ match to_sig Q sig a with
  98     [ None ⇒ nil ?
  99     | Some c ⇒ c::(to_sig_map Q sig tl)]].
 100
 101
 102 definition to_sig_tape ≝ λQ,sig,t.
 103   match t with
 104   [ niltape  ⇒ niltape ?
 105   | leftof a l ⇒ match to_sig Q sig a with
 106     [ None ⇒ niltape ?
 107     | Some x ⇒ leftof ? x (to_sig_map Q sig l) ]
 108   | rightof a l ⇒ match to_sig Q sig a with
 109     [ None ⇒ niltape ?
 110     | Some x ⇒ rightof ? x (to_sig_map Q sig l) ]
 111   | midtape ls a rs ⇒ match to_sig Q sig a with
 112     [ None ⇒ niltape ?
 113     | Some x ⇒ midtape ? (to_sig_map Q sig ls) x (to_sig_map Q sig rs) ]
 114   ].
 115
 116 let rec rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs i on i ≝
 117   match i with
 118   [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
 119   | S j ⇒ vec_cons_right ? (to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs j)) j
 120            (rb_tapes Q sig n ls a rs j)].
 121
 122 lemma nth_rb_tapes : ∀Q,sig,n,ls.∀a:MTA Q sig (S n).∀rs,j,i. i < j →
 123   nth i ? (rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs j) (niltape ?) =
 124     to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs i).
 125 #Q #sig #n #ls #a #rs #j elim j
 126   [#i #H @False_ind /2/
 127   |#k #Hind #i #lti cases (le_to_or_lt_eq … (le_S_S_to_le … lti))
 128     [#Hlt >nth_cons_right_lt [@Hind //|//]
 129     |#Heq >Heq @nth_cons_right_n
 130     ]
 131   ]
 132 qed.
 133
 134
 135 (* q0 is a default value *)
 136 definition get_state ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).λq0.
 137   match nth n ? (vec … a) (blank ?) with
 138   [ None ⇒ q0 (* impossible *)
 139   | Some qM ⇒ match qM with
 140     [inl qM1 ⇒ fst ?? qM1
 141     |inr _ ⇒ q0 (* impossible *) ]].
 142
 143 definition get_chars ≝ λQ,sig,n.λa:MTA (HC Q n) sig (S n).
 144   let a1 ≝ resize_vec ? (S n) a n (blank ?) in
 145   vec_map ?? (to_sig ? sig) n a1.
 146
 147 lemma get_chars_def : ∀Q,sig,n.∀a:MTA (HC Q n) sig (S n).
 148   get_chars … a =
 149     vec_map ?? (to_sig ? sig) n (resize_vec ? (S n) a n (blank ?)).
 150 // qed.
 151
 152 include "turing/turing.ma".
 153
 154 definition readback_config ≝
 155   λQ,sig,n,q0,ls.λa:MTA (HC Q (S n)) sig (S (S n)).λrs.
 156   mk_mconfig sig Q n
 157     (get_state Q sig (S n) a q0)
 158     (rb_tapes (HC Q (S n)) sig (S n) ls a rs (S n)).
 159
 160 lemma state_readback : ∀Q,sig,n,q0,ls,a,rs.
 161   cstate … (readback_config Q sig n q0 ls a rs) =
 162     get_state Q sig (S n) a q0.
 163 // qed.
 164
 165 lemma tapes_readback : ∀Q,sig,n,q0,ls,a,rs.
 166   ctapes … (readback_config Q sig n q0 ls a rs) =
 167     rb_tapes (HC Q (S n)) sig (S n) ls a rs (S n).
 168 // qed.
 169
 170 definition R_stepM ≝ λsig.λn.λM:mTM sig n.λt1,t2.
 171 ∀a,ls,rs.
 172   t1 = midtape ? ls a rs →
 173   (∀i.regular_trace (TA (HC (states … M) (S n)) sig) (S(S n)) a ls rs i) →
 174   is_head ?? (nth (S n) ? (vec … a) (blank ?)) = true →
 175   no_head_in … ls →
 176   no_head_in … rs →
 177   ∃ls1,a1,rs1.
 178    t2 = midtape (MTA (HC (states … M) (S n)) sig (S(S n))) ls1 a1 rs1 ∧
 179    (∀i.regular_trace (TA (HC (states … M) (S n)) sig) (S(S n)) a1 ls1 rs1 i) ∧
 180    readback_config ? sig n (start … M) ls1 a1 rs1 =
 181      step sig n M (readback_config ? sig n (start … M) ls a rs).
 182
 183 lemma nth_vec_map_lt :
 184   ∀A,B,f,i,n.∀v:Vector A n.∀d1,d2.i < n →
 185   nth i ? (vec_map A B f n v) d1 = f (nth i ? v d2).
 186 #A #B #f #i #n #v #d1 #d2 #ltin >(nth_default B i n ? d1 (f d2) ltin) @sym_eq @nth_vec_map
 187 qed.
 188
 189 lemma ctapes_mk_config : ∀sig,Q,n,s,t.
 190   ctapes sig Q n (mk_mconfig sig Q n s t) = t.
 191 // qed.
 192
 193 lemma cstate_rb: ∀sig,n.∀M:mTM sig n.∀ls,a,rs.∀q,m.
 194   nth (S n) ? (vec … a) (blank ?) = Some ? (inl ?? 〈q,m〉) →
 195   cstate sig (states sig n M) n
 196       (readback_config (states sig n M) sig n (start sig n M) ls a rs) = q.
 197 #sig #n #M #ls #a #rs #q #m #H
 198 >state_readback whd in ⊢ (??%?); >H %
 199 qed.
 200
 201 axiom eq_cstate_get_state: ∀sig,n.∀M:mTM sig n.∀ls,a,rs.
 202   is_head ?? (nth (S n) ? (vec … a) (blank ?)) = true →
 203   cstate sig (states sig n M) n
 204       (readback_config (states sig n M) sig n (start sig n M) ls a rs) =
 205   get_state (states sig n M) sig (S n) a (start sig n M).
 206
 207 axiom eq_current_chars_resize: ∀sig,n.∀M:mTM sig n.∀ls,a,rs.
 208   current_chars sig n
 209    (ctapes sig (states sig n M) n
 210     (readback_config (states sig n M) sig n (start sig n M) ls a rs)) =
 211   get_chars … a.
 212
 213 (*
 214 lemma rb_trans : ∀sig,Q,n.∀M:mTM sig n.∀ls,a,rs,q,m.
 215   nth (S n) ? (vec … a) (blank ?) = Some ? (inl ?? 〈q,m〉) →
 216   transf (states sig n M) sig (S n) (trans sig n M) a =
 217   trans sig n M 〈q,get_chars … a〉.
 218 *)
 219
 220 lemma nth_pmap_lt :
 221   ∀A,B,C,f,i,n.∀v1:Vector A n.∀v2:Vector B n.∀d1,d2,d3.i < n→
 222   f (nth i ? v1 d1) (nth i ? v2 d2) = nth i ? (pmap_vec A B C f n v1 v2) d3.
 223 #A #B #C #f #i elim i
 224 [ *
 225   [ #v1 #v2 #d1 #d2 #d3 #Hlt @False_ind /2/
 226   | #n0 #v1 #v2 #d1 #d2 #d3 #_ >(vec_expand … v1)
 227     >(vec_expand … v2) >(nth_default … d3 (f d1 d2)) [% | // ]]
 228 | #i0 #IH *
 229   [ #v1 #v2 #d1 #d2 #d3 #Hlt @False_ind /2/
 230   | #n #v1 #v2 #d1 #d2 #d3 #Hlt>(vec_expand … v1)
 231      >(vec_expand … v2)
 232      whd in match (nth …d1); whd in match (tail ??);
 233      whd in match (nth … d2); whd in match (tail B ?);
 234      whd in match (nth … d3); whd in match (tail C ?);
 235      <(IH n ?? d1 d2 d3) [2:@le_S_S_to_le @Hlt] %
 236   ] ]
 237 qed.
 238
 239 lemma tape_move_mono_def : ∀sig,t,a,m.
 240   tape_move_mono sig t 〈a,m〉 = tape_move sig (tape_write sig t a) m.
 241 // qed.
 242
 243 axiom to_sig_move : ∀Q,sig,n,t,m.
 244   to_sig_tape (HC Q (S n)) sig
 245   (tape_move (sig_ext (TA (HC Q (S n)) sig)) t m)
 246   = tape_move sig (to_sig_tape ?? t) m.
 247
 248 definition to_sig_conv :∀Q,sig:FinSet.∀n.
 249  option sig → option (sig_ext (TA (HC Q (S n)) sig))
 250 ≝ λQ,sig,n,c.
 251   match c with
 252   [None ⇒ None ?
 253   |Some a ⇒ Some ? (Some ? (inr (HC Q (S n)) ? a))].
 254
 255 axiom to_sig_write : ∀Q,sig,n,t,c.
 256   to_sig_tape (HC Q (S n)) sig
 257   (tape_write ? t (to_sig_conv ??? c))
 258    = tape_write sig (to_sig_tape ?? t) c.
 259
 260 definition opt ≝ λA.λoc1: option A.λc2.
 261   match oc1 with [None ⇒ c2 | Some c1 ⇒ c1].
 262
 263 axiom rb_write: ∀sig,n,ls,a,rs,i,c1,c2.
 264   nth i ? c1 (None ?) = opt ? c2 (nth i ? c1 (None ?)) →
 265   rb_trace_i ? n ls c1 rs i =
 266   tape_write ? (rb_trace_i sig n ls a rs i) c2.
 267
 268 lemma sem_stepM : ∀sig,n.∀M:mTM sig n.
 269   stepM (states sig n M) sig n (trans sig n M) ⊨
 270     R_stepM sig n M.
 271 #sig #n #M
 272 @(sem_seq_app … (sem_writef … ) (sem_exec_moves … (le_n ?)))
 273 #tin #tout * #t1 * whd in ⊢ (%→?); #Hwrite #Hmoves
 274 #a #ls #rs #Htin #H1 #H2 #H3 #H4 >Htin in Hwrite; #Hwrite
 275 lapply (Hwrite … (refl …)) -Hwrite whd in match (right ??); whd in match (left ??);
 276 >optf_Some #Ht1
 277 cut (∃q,m. nth (S n) ? (vec … a) (blank ?) = Some ? (inl ?? 〈q,m〉))
 278     [lapply H2 cases (nth (S n) ? (vec … a) (blank ?))
 279       [whd in ⊢ (??%?→?); #H destruct (H)
 280       |* #x whd in ⊢ (??%?→?); #H destruct (H) cases x #q #m %{q} %{m} %
 281       ]
 282     ] * #q * #m #HaSn
 283 (*
 284 lapply (transf_eq … HaSn (refl ??) (refl ??) (eq_pair_fst_snd …) (refl ??) (refl ??))
 285 *)
 286 lapply (Hmoves … Ht1 ?? H3 H4)
 287   [>(transf_eq … HaSn (refl ??) (refl ??) (eq_pair_fst_snd …) (refl ??) (refl ??))
 288    >nth_cons_right_n %
 289   | (* regularity is preserved *) @daemon
 290   |* #ls1 * #a1 * #rs1 * * * #Htout #Hreg #Hrb #HtrSn
 291    lapply (HtrSn (S n) (le_n ?) (le_n ?)) -HtrSn #HtrSn
 292    cut (nth (S n) ? (vec … a1) (blank ?) =
 293         nth (S n ) ? (vec … (transf (states sig n M) sig (S n) (trans sig n M) a)) (blank ?))
 294     [@daemon (* from HtrSn *)] #Ha1
 295    %{ls1} %{a1} %{rs1}
 296    %[%[@Htout |@Hreg]
 297     |(* commutation *)
 298      lapply(transf_eq_ex …  (trans sig n M) … HaSn)
 299      * #c1 * #Hc1 * #c2 * #Hc2 * #q1 * #actions *
 300      #Htrans * #moves * #Hmoves * #new_chars * #Hnew_chars #Htransf
 301      @mconfig_eq
 302       [(* state *) >state_readback whd in match (step ????);
 303        >(cstate_rb … HaSn) >eq_current_chars_resize >get_chars_def
 304        <Hc1 <Hc2 >Htrans whd in ⊢ (???%);
 305        whd in ⊢ (??%?); >Ha1 >HaSn >Htransf >nth_cons_right_n %
 306       |>tapes_readback whd in match (step ????);
 307        >(cstate_rb … HaSn) >eq_current_chars_resize >get_chars_def
 308        <Hc1 <Hc2 >Htrans >ctapes_mk_config
 309        @(eq_vec … (niltape ?)) #i #lti
 310        >nth_rb_tapes [2:@lti]
 311        >Hrb [2:@lt_to_le @lti|3:@lti]
 312        >Htransf whd in match (get_move ?????); (* whd in match (vec_moves ?????); *)
 313        >get_moves_cons_right
 314        (* lhs *)
 315        <nth_pmap_lt [2:@lti|3:%[@None|@N]|4:@niltape]
 316        >ctapes_mk_config >nth_rb_tapes [2:@lti]
 317        (* >nth_vec_map_lt [2:@lti |3:@niltape] *)
 318        >(eq_pair_fst_snd … (nth i ? actions ?))
 319        >tape_move_mono_def
 320        cut (snd ?? (nth i ? actions 〈None sig,N〉) = nth i ? moves N)
 321          [>Hmoves @nth_vec_map] #Hmoves1 >Hmoves1
 322        >to_sig_move @eq_f2 [2://]
 323        <to_sig_write @eq_f @rb_write
 324        >nth_cons_right_lt [2:@lti]
 325        >Hnew_chars <nth_pmap_lt [2:@lti|3:@None |4:%[@None|@N]]
 326        whd in ⊢ (??%%);
 327        inversion (\fst  (nth i ? actions 〈None sig,N〉))
 328         [#Hcase whd in ⊢ (??%%); >Hcase % |#c #Hcase % ]
 329       ]
 330     ]
 331   ]
 332 qed.
 333
 334
 335
 336
 337
 338
 339
 340
 341
 342
 343
 344
 345
 346
 347
 348