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 (**************************** Vector Operations *******************************)
   7
   8 let rec resize A (l:list A) i d on i ≝
   9   match i with
  10   [ O ⇒ [ ]
  11   | S j ⇒ (hd ? l d)::resize A (tail ? l) j d
  12   ].
  13
  14 lemma length_resize : ∀A,l,i,d. |resize A l i d| = i.
  15 #A #l #i lapply l -l elim i
  16   [#l #d %
  17   |#m #Hind #l cases l
  18     [#d normalize @eq_f @Hind
  19     |#a #tl #d normalize @eq_f @Hind
  20     ]
  21   ]
  22 qed.
  23
  24 lemma resize_id : ∀A,n,l,d. |l| = n →
  25   resize A l n d = l.
  26 #A #n elim n
  27   [#l #d #H >(lenght_to_nil … H) //
  28   |#m #Hind * #d normalize
  29     [#H destruct |#a #tl #H @eq_f @Hind @injective_S // ]
  30   ]
  31 qed.
  32
  33 definition resize_vec :∀A,n.Vector A n → ∀i.A→Vector A i.
  34 #A #n #a #i #d @(mk_Vector A i (resize A a i d) ) @length_resize
  35 qed.
  36
  37 axiom nth_resize_vec :∀A,n.∀v:Vector A n.∀d,i,j. i < j →i < n →
  38   nth i ? (resize_vec A n v j d) d = nth i ? v d.
  39
  40 lemma resize_vec_id : ∀A,n.∀v:Vector A n.∀d.
  41   resize_vec A n v n d = v.
  42 #A #n #v #d @(eq_vec … d) #i #ltin @nth_resize_vec //
  43 qed.
  44
  45 definition vec_single: ∀A,a. Vector A 1 ≝ λA,a.
  46   mk_Vector A 1 [a] (refl ??).
  47
  48 definition vec_cons_right : ∀A.∀a:A.∀n. Vector A n → Vector A (S n).
  49 #A #a #n #v >(plus_n_O n) >plus_n_Sm @(vec_append … v (vec_single A a))
  50 >length_append >(len A n v) //
  51 qed.
  52
  53 lemma eq_cons_right : ∀A,a1,a2.∀n.∀v1,v2:Vector A n.
  54   a1 = a2 → v1 = v2 → vec_cons_right A a1 n v1 = vec_cons_right A a2 n v2.
  55 // qed.
  56
  57 axiom nth_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
  58   nth n ? (vec_cons_right A a n v) d = a.
  59 (*
  60 #A #a #n elim n
  61   [#v #d >(vector_nil … v) //
  62   |#m #Hind #v #d >(vec_expand … v) whd in ⊢ (??%?);
  63    whd in match (vec_cons_right ????);
  64 *)
  65
  66 lemma get_moves_cons_right: ∀Q,sig,n,q,moves,a.
  67   get_moves Q sig (S n)
  68     (vec_cons_right ? (Some ? (inl ?? 〈q,moves〉)) (S n) a) = moves.
  69 #Q #sig #n #q #moves #a whd in ⊢(??%?); >nth_cons_right //
  70 qed.
  71
  72 axiom resize_cons_right: ∀A.∀a:A.∀n.∀v:Vector A n.∀d.
  73   resize_vec ? (S n) (vec_cons_right A a n v) n d = v.
  74
  75 let rec exec_moves Q sig n i on i : TM (MTA (HC Q n) sig (S n)) ≝
  76   match i with
  77   [ O ⇒ nop ? (* exec_move_i sig n 0 *)
  78   | S j ⇒ seq ? (exec_moves Q sig n j) (exec_move_i Q sig n j)
  79   ].
  80
  81 definition a_moves ≝
  82   λsig,n.λactions: Vector ((option sig) × move) n.
  83   vec_map ?? (snd ??) n actions.
  84
  85 definition a_chars ≝
  86   λsig,n.λactions: Vector ((option sig) × move) n.
  87   vec_map ?? (fst ??) n actions.
  88
  89 definition tape_moves ≝
  90   λsig,n,ts,mvs.
  91   pmap_vec ??? (tape_move sig) n ts mvs.
  92
  93 lemma tape_moves_def : ∀sig,n,ts,mvs.
  94   tape_moves sig n ts mvs = pmap_vec ??? (tape_move sig) n ts mvs.
  95 // qed.
  96
  97 definition tape_writem ≝
  98   λsig,n,ts,chars.
  99   pmap_vec ??? (tape_write sig) n ts chars.
 100
 101 (*
 102 let rec i_moves a i on i : Vector move i ≝
 103   match i with
 104   [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
 105   | S j ⇒ vec_cons ? (nth j ? a N) j (i_moves a j)
 106   ]. *)
 107
 108 definition vec_moves ≝ λQ,sig,n,a,i.
 109   resize_vec … (get_moves Q sig n a) i N.
 110
 111 axiom vec_moves_cons: ∀Q,sig,n,a,j.j < n →
 112  vec_moves Q sig n a (S j) =
 113  vec_cons ? (get_move Q ? n a j) j (vec_moves Q sig n a j).
 114
 115 (*
 116 axiom actions_commute : ∀sig,n,ts,actions.
 117   tape_moves sig n (tape_writem ?? ts (a_chars … actions)) (a_moves … actions) =
 118     tape_move_multi ?? ts actions. *)
 119
 120 (* devo rafforzare la semantica, dicendo che i tape non toccati
 121 dalle moves non cambiano *)
 122
 123
 124 definition R_exec_moves ≝ λQ,sig,n,i,t1,t2.
 125 ∀a,ls,rs.
 126   t1 = midtape ? ls a rs →
 127   (∀i.regular_trace (TA (HC Q n) sig) (S n) a ls rs i) →
 128   is_head ?? (nth n ? (vec … a) (blank ?)) = true →
 129   no_head_in … ls →
 130   no_head_in … rs →
 131   ∃ls1,a1,rs1.
 132    t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
 133    (∀i.regular_trace (TA (HC Q n) sig) (S n) a1 ls1 rs1 i) ∧
 134    readback ? (S n) ls1 (vec … a1) rs1 i =
 135      tape_moves ?? (readback ? (S n) ls (vec … a) rs i) (vec_moves Q sig n a i) ∧
 136    (∀j. i ≤ j → j ≤ n →
 137     rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
 138       rb_trace_i ? (S n) ls (vec … a) rs j).
 139
 140 (* alias id "Realize_to_Realize" =
 141   "cic:/matita/turing/mono/Realize_to_Realize.def(13)". *)
 142
 143 lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j →
 144  nth i ? (readback sig n ls a rs j) (niltape ?) =
 145    rb_trace_i sig n ls a rs (j - S i).
 146 #sig #n #ls #a #rs #j elim j
 147   [#i #lti0 @False_ind /2/
 148   |-j #j #Hind *
 149     [#_ >minus_S_S <minus_n_O %
 150     |#m #Hmj >minus_S_S @Hind @le_S_S_to_le //
 151     ]
 152   ]
 153 qed.
 154
 155 lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n →
 156   exec_moves Q sig n i ⊨ R_exec_moves Q sig n i.
 157 #Q #sig #n #i elim i
 158   [#_ @(Realize_to_Realize … (sem_nop …))
 159    #t1 #t2 #H #a #ls #rs #Ht1 #Hreg #H1 #H2 #H3
 160    %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| %]|//]
 161   |#j #Hind #lttj lapply (lt_to_le … lttj) #ltj
 162    @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind
 163    #int #outt * #t1 * #H1 #H2
 164    #a #ls #rs #Hint #H3 #H4 #H5 #H6
 165    lapply (H1 … Hint H3 H4 H5 H6)
 166    * #ls1 * #a1 * #rs1 * * * #H7 #H8 #H9 #H10
 167    lapply (reg_inv … (H8 n) ? H4 H5 H6)
 168     [@H10 [@ltj |@le_n]]
 169    -H3 -H4 -H5 -H6 * * #H3 #H4 #H5
 170    lapply (H2 … H7 H8 H3 H4 H5)
 171    * #ls2 * #a2 * #rs2 * * * #Houtt #Hregout #Hrboutt #Hrbid
 172    %{ls2} %{a2} %{rs2}
 173    cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i)
 174      [@daemon] #aa1
 175    %[%[%[@Houtt|@Hregout]
 176       |whd in ⊢ (??%?); @Vector_eq >(vec_moves_cons … lttj)
 177        >tape_moves_def >pmap_vec_cons @eq_f2
 178         [<H10 [>aa1 @Hrboutt |@ltj |@le_n]
 179         |<tape_moves_def <H9 (* mitico *) @eq_f
 180          @(eq_vec … (niltape ?)) #i #ltij
 181          >(nth_readback … ltij) >(nth_readback … ltij) @Hrbid
 182           [@(transitive_le … ltj) // |@lt_to_not_eq @lt_plus_to_minus //]
 183         ]
 184       ]
 185     |#a #Hja #Han >(Hrbid … Han)
 186       [@(H10 … Han) @lt_to_le @Hja |@sym_not_eq @lt_to_not_eq @Hja ]
 187     ]
 188   ]
 189 qed.
 190
 191
 192
 193
 194
 195
 196
 197
 198
 199
 200
 201
 202
 203