matita/matita/lib/turing/multi_to_mono/exec_moves.ma

   1 (* include "turing/auxiliary_machines.ma". *)
   2
   3 include "turing/multi_to_mono/exec_trace_move.ma".
   4 (* include "turing/turing.ma". *)
   5
   6 let rec exec_moves sig n i on i : TM (multi_sig sig n) ≝
   7   match i with
   8   [ O ⇒ nop ? (* exec_move_i sig n 0 *)
   9   | S j ⇒ seq ? (exec_moves sig n j) (exec_move_i sig n j)
  10   ].
  11
  12 axiom get_moves : ∀sig,n.∀a:multi_sig sig n.∀i.Vector DeqMove i.
  13
  14 axiom get_moves_cons: ∀sig,n,a,j.j < n →
  15  get_moves sig n a (S j) =
  16  vec_cons ? (get_move ? n a j) j (get_moves sig n a j).
  17
  18 definition a_moves ≝
  19   λsig,n.λactions: Vector ((option sig) × move) n.
  20   vec_map ?? (snd ??) n actions.
  21
  22 definition a_chars ≝
  23   λsig,n.λactions: Vector ((option sig) × move) n.
  24   vec_map ?? (fst ??) n actions.
  25
  26 definition tape_moves ≝
  27   λsig,n,ts,mvs.
  28   pmap_vec ??? (tape_move sig) n ts mvs.
  29
  30 lemma tape_moves_def : ∀sig,n,ts,mvs.
  31   tape_moves sig n ts mvs = pmap_vec ??? (tape_move sig) n ts mvs.
  32 // qed.
  33
  34 definition tape_writem ≝
  35   λsig,n,ts,chars.
  36   pmap_vec ??? (tape_write sig) n ts chars.
  37
  38 (*
  39 axiom actions_commute : ∀sig,n,ts,actions.
  40   tape_moves sig n (tape_writem ?? ts (a_chars … actions)) (a_moves … actions) =
  41     tape_move_multi ?? ts actions. *)
  42
  43 (* devo rafforzare la semantica, dicendo che i tape non toccati
  44 dalle moves non cambiano *)
  45
  46 definition R_exec_moves ≝ λsig,n,i,t1,t2.
  47 ∀a,ls,rs.
  48   t1 = midtape ? ls a rs →
  49   (∀i.regular_trace sig n a ls rs i) →
  50   nth n ? (vec … a) (blank ?) = head ? →
  51   no_head_in … ls →
  52   no_head_in … rs →
  53   ∃ls1,a1,rs1.
  54    t2 = midtape (multi_sig sig n) ls1 a1 rs1 ∧
  55    (∀i.regular_trace sig n a1 ls1 rs1 i) ∧
  56    readback sig n ls1 (vec … a1) rs1 i =
  57      tape_moves ?? (readback sig n ls (vec … a) rs i) (get_moves sig n a i) ∧
  58    (∀j. i ≤ j → j ≤ n →
  59     rb_trace_i sig n ls1 (vec … a1) rs1 j =
  60       rb_trace_i sig n ls (vec … a) rs j).
  61
  62 (* alias id "Realize_to_Realize" =
  63   "cic:/matita/turing/mono/Realize_to_Realize.def(13)". *)
  64
  65 lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j →
  66  nth i ? (readback sig n ls a rs j) (niltape ?) =
  67    rb_trace_i sig n ls a rs (j - S i).
  68 #sig #n #ls #a #rs #j elim j
  69   [#i #lti0 @False_ind /2/
  70   |-j #j #Hind *
  71     [#_ >minus_S_S <minus_n_O %
  72     |#m #Hmj >minus_S_S @Hind @le_S_S_to_le //
  73     ]
  74   ]
  75 qed.
  76
  77 lemma sem_exec_moves: ∀sig,n,i. i < n →
  78   exec_moves sig n i ⊨ R_exec_moves sig n i.
  79 #sig #n #i elim i
  80   [#_ @(Realize_to_Realize … (sem_nop …))
  81    #t1 #t2 #H #a #ls #rs #Ht1 #Hreg #H1 #H2 #H3
  82    %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| %]|//]
  83   |#j #Hind #lttj lapply (lt_to_le … lttj) #ltj
  84    @(sem_seq_app … (Hind ltj) (sem_exec_move_i … ltj)) -Hind
  85    #int #outt * #t1 * #H1 #H2
  86    #a #ls #rs #Hint #H3 #H4 #H5 #H6
  87    lapply (H1 … Hint H3 H4 H5 H6)
  88    * #ls1 * #a1 * #rs1 * * * #H7 #H8 #H9 #H10
  89    lapply (reg_inv … (H8 n) ? H4 H5 H6)
  90     [@H10 [@lt_to_le @ltj |@le_n]]
  91    -H3 -H4 -H5 -H6 * * #H3 #H4 #H5
  92    lapply (H2 … H7 H8 H3 H4 H5)
  93    * #ls2 * #a2 * #rs2 * * * #Houtt #Hregout #Hrboutt #Hrbid
  94    %{ls2} %{a2} %{rs2}
  95    cut (∀i. get_move sig n a i = get_move sig n a1 i)
  96      [@daemon] #aa1
  97    %[%[%[@Houtt|@Hregout]
  98       |whd in ⊢ (??%?); @Vector_eq >(get_moves_cons … ltj)
  99        >tape_moves_def >pmap_vec_cons @eq_f2
 100         [<H10 [>aa1 @Hrboutt |@lt_to_le @ltj |@le_n]
 101         |<tape_moves_def <H9 (* mitico *) @eq_f
 102          @(eq_vec … (niltape ?)) #i #ltij
 103          >(nth_readback … ltij) >(nth_readback … ltij) @Hrbid
 104           [@(transitive_le … ltj) // |@lt_to_not_eq @lt_plus_to_minus //]
 105         ]
 106       ]
 107     |#a #Hja #Han >(Hrbid … Han)
 108       [@(H10 … Han) @lt_to_le @Hja |@sym_not_eq @lt_to_not_eq @Hja ]
 109     ]
 110   ]
 111 qed.
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124
 125