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