matita/matita/lib/turing/multi_universal/moves.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "turing/turing.ma".
  13 include "turing/inject.ma".
  14 include "turing/while_multi.ma".
  15
  16 definition parmove_states ≝ initN 3.
  17
  18 definition parmove0 : parmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  19 definition parmove1 : parmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  20 definition parmove2 : parmove_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  21
  22 (*
  23
  24 src: a b c ... z # ---→ a b c ... z #
  25      ^                              ^
  26
  27 dst: _ _ _ ... _ d ---→ a b c ... z d
  28      ^                              ^
  29
  30 0) (x ≠ sep,_) → (x,x)(R,R) → 1
  31    (sep,d) → None 2
  32 1) (_,_) → None 1
  33 2) (_,_) → None 2
  34
  35 *)
  36
  37 definition trans_parmove_step ≝
  38  λsrc,dst,sig,n,D,is_sep.
  39  λp:parmove_states × (Vector (option sig) (S n)).
  40  let 〈q,a〉 ≝ p in
  41  match pi1 … q with
  42  [ O ⇒ match nth src ? a (None ?) with
  43    [ None ⇒ 〈parmove2,null_action ? n〉
  44    | Some a0 ⇒
  45      if is_sep a0 then 〈parmove2,null_action ? n〉
  46      else match nth dst ? a (None ?) with
  47      [ None ⇒ 〈parmove2,null_action ? n〉
  48      | Some a1 ⇒ 〈parmove1,change_vec ? (S n)
  49                           (change_vec ?(S n)
  50                            (null_action ? n) (Some ? 〈a0,D〉) src)
  51                           (Some ? 〈a1,D〉) dst〉 ] ]
  52  | S q ⇒ match q with
  53    [ O ⇒ (* 1 *) 〈parmove1,null_action ? n〉
  54    | S _ ⇒ (* 2 *) 〈parmove2,null_action ? n〉 ] ].
  55
  56 definition parmove_step ≝
  57   λsrc,dst,sig,n,D,is_sep.
  58   mk_mTM sig n parmove_states (trans_parmove_step src dst sig n D is_sep)
  59     parmove0 (λq.q == parmove1 ∨ q == parmove2).
  60
  61 definition R_parmove_step_true ≝
  62   λsrc,dst,sig,n,D,is_sep.λint,outt: Vector (tape sig) (S n).
  63   ∃x1,x2.
  64    current ? (nth src ? int (niltape ?)) = Some ? x1 ∧
  65    current ? (nth dst ? int (niltape ?)) = Some ? x2 ∧
  66    is_sep x1 = false ∧
  67    outt = change_vec ??
  68             (change_vec ?? int
  69               (tape_move ? (nth src ? int (niltape ?)) (Some ? 〈x1,D〉)) src)
  70             (tape_move ? (nth dst ? int (niltape ?)) (Some ? 〈x2,D〉)) dst.
  71
  72 definition R_parmove_step_false ≝
  73   λsrc,dst:nat.λsig,n,is_sep.λint,outt: Vector (tape sig) (S n).
  74   ((∃x1.
  75    current ? (nth src ? int (niltape ?)) = Some ? x1 ∧
  76    is_sep x1 = true) ∨
  77    current ? (nth src ? int (niltape ?)) = None ?  ∨
  78    current ? (nth dst ? int (niltape ?)) = None ?) ∧
  79    outt = int.
  80
  81 lemma parmove_q0_q2_null_src :
  82   ∀src,dst,sig,n,D,is_sep,v.src < S n → dst < S n →
  83   nth src ? (current_chars ?? v) (None ?) = None ? →
  84   step sig n (parmove_step src dst sig n D is_sep)
  85     (mk_mconfig ??? parmove0 v) =
  86     mk_mconfig ??? parmove2 v.
  87 #src #dst #sig #n #D #is_sep #v #Hsrc #Hdst #Hcurrent
  88 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
  89 @eq_f2
  90 [ whd in ⊢ (??(???%)?); >Hcurrent %
  91 | whd in ⊢ (??(???????(???%))?); >Hcurrent @tape_move_null_action ]
  92 qed.
  93
  94 lemma parmove_q0_q2_sep :
  95   ∀src,dst,sig,n,D,is_sep,v,s.src < S n → dst < S n →
  96   nth src ? (current_chars ?? v) (None ?) = Some ? s → is_sep s = true →
  97   step sig n (parmove_step src dst sig n D is_sep)
  98     (mk_mconfig ??? parmove0 v) =
  99     mk_mconfig ??? parmove2 v.
 100 #src #dst #sig #n #D #is_sep #v #s #Hsrc #Hdst #Hcurrent #Hsep
 101 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 102 @eq_f2
 103 [ whd in ⊢ (??(???%)?); >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
 104 | whd in ⊢ (??(???????(???%))?); >Hcurrent
 105   whd in ⊢ (??(???????(???%))?); >Hsep @tape_move_null_action ]
 106 qed.
 107
 108 lemma parmove_q0_q2_null_dst :
 109   ∀src,dst,sig,n,D,is_sep,v,s.src < S n → dst < S n →
 110   nth src ? (current_chars ?? v) (None ?) = Some ? s → is_sep s = false →
 111   nth dst ? (current_chars ?? v) (None ?) = None ? →
 112   step sig n (parmove_step src dst sig n D is_sep)
 113     (mk_mconfig ??? parmove0 v) =
 114     mk_mconfig ??? parmove2 v.
 115 #src #dst #sig #n #D #is_sep #v #s #Hsrc #Hdst #Hcursrc #Hsep #Hcurdst
 116 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
 117 @eq_f2
 118 [ whd in ⊢ (??(???%)?); >Hcursrc whd in ⊢ (??(???%)?); >Hsep >Hcurdst %
 119 | whd in ⊢ (??(???????(???%))?); >Hcursrc
 120   whd in ⊢ (??(???????(???%))?); >Hsep >Hcurdst @tape_move_null_action ]
 121 qed.
 122
 123 lemma parmove_q0_q1 :
 124   ∀src,dst,sig,n,D,is_sep,v.src ≠ dst → src < S n → dst < S n →
 125   ∀a1,a2.
 126   nth src ? (current_chars ?? v) (None ?) = Some ? a1 →
 127   nth dst ? (current_chars ?? v) (None ?) = Some ? a2 →
 128   is_sep a1 = false →
 129   step sig n (parmove_step src dst sig n D is_sep)
 130     (mk_mconfig ??? parmove0 v) =
 131     mk_mconfig ??? parmove1
 132      (change_vec ? (S n)
 133        (change_vec ?? v
 134          (tape_move ? (nth src ? v (niltape ?)) (Some ? 〈a1,D〉)) src)
 135        (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈a2,D〉)) dst).
 136 #src #dst #sig #n #D #is_sep #v #Hneq #Hsrc #Hdst
 137 #a1 #a2 #Hcursrc #Hcurdst #Hsep
 138 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
 139 [ whd in match (trans ????);
 140   >Hcursrc >Hcurdst whd in ⊢ (??(???%)?); >Hsep //
 141 | whd in match (trans ????);
 142   >Hcursrc >Hcurdst whd in ⊢ (??(???????(???%))?); >Hsep
 143   change with (change_vec ?????) in ⊢ (??(???????%)?);
 144   <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
 145   <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
 146   >pmap_change >pmap_change >tape_move_null_action
 147   @eq_f2 // @eq_f2 // >nth_change_vec_neq //
 148 ]
 149 qed.
 150
 151 lemma sem_parmove_step :
 152   ∀src,dst,sig,n,D,is_sep.src ≠ dst → src < S n → dst < S n →
 153   parmove_step src dst sig n D is_sep ⊨
 154     [ parmove1: R_parmove_step_true src dst sig n D is_sep,
 155              R_parmove_step_false src dst sig n is_sep ].
 156 #src #dst #sig #n #D #is_sep #Hneq #Hsrc #Hdst #int
 157 lapply (refl ? (current ? (nth src ? int (niltape ?))))
 158 cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
 159 [ #Hcursrc %{2} %
 160   [| % [ %
 161     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
 162       <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
 163     | normalize in ⊢ (%→?); #H destruct (H) ]
 164     | #_ % // % %2 // ] ]
 165 | #a #Ha cases (true_or_false (is_sep a)) #Hsep
 166   [ %{2} %
 167     [| % [ %
 168       [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
 169         <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
 170       | normalize in ⊢ (%→?); #H destruct (H) ]
 171       | #_ % // % % %{a} % // ] ]
 172   | lapply (refl ? (current ? (nth dst ? int (niltape ?))))
 173     cases (current ? (nth dst ? int (niltape ?))) in ⊢ (???%→?);
 174     [ #Hcurdst %{2} %
 175       [| % [ %
 176         [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/
 177           [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
 178           | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
 179         | normalize in ⊢ (%→?); #H destruct (H) ]
 180         | #_ % // %2 // ] ]
 181     | #b #Hb %{2} %
 182       [| % [ %
 183         [whd in ⊢  (??%?);  >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
 184           [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
 185           | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
 186         | #_ %{a} %{b} % // % // % // ]
 187         | * #H @False_ind @H % ]
 188 ]]]]
 189 qed.
 190
 191 definition parmove ≝ λsrc,dst,sig,n,D,is_sep.
 192   whileTM … (parmove_step src dst sig n D is_sep) parmove1.
 193
 194 definition R_parmoveL ≝
 195   λsrc,dst,sig,n,is_sep.λint,outt: Vector (tape sig) (S n).
 196   (∀ls,x,xs,rs,sep.
 197     nth src ? int (niltape ?) = midtape sig (xs@sep::ls) x rs →
 198     (∀c.memb ? c (x::xs) = true → is_sep c = false) → is_sep sep = true →
 199     ∀ls0,x0,target,c,rs0.|xs| = |target| →
 200     nth dst ? int (niltape ?) = midtape sig (target@c::ls0) x0 rs0 →
 201     outt = change_vec ??
 202            (change_vec ?? int (midtape sig ls sep (reverse ? xs@x::rs)) src)
 203            (midtape sig ls0 c (reverse ? target@x0::rs0)) dst) ∧
 204   (((∃s.current ? (nth src ? int (niltape ?)) = Some ? s ∧ is_sep s = true) ∨
 205      current ? (nth src ? int (niltape ?)) = None ? ∨
 206      current ? (nth dst ? int (niltape ?)) = None ?) →
 207      outt = int).
 208
 209 lemma wsem_parmoveL : ∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n →
 210   parmove src dst sig n L is_sep ⊫ R_parmoveL src dst sig n is_sep.
 211 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 212 lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) … Hloop) //
 213 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 214 [ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H
 215   [ * [ * #x * #Hx #Hsep #ls #x0 #xs #rs #sep #Hsrctc #Hnosep >Hsrctc in Hx; normalize in ⊢ (%→?);
 216     #Hx0 destruct (Hx0) lapply (Hnosep ? (memb_hd …)) >Hsep
 217     #Hfalse destruct (Hfalse)
 218   | #Hcur_src #ls #x0 #xs #rs #sep #Hsrctc >Hsrctc in Hcur_src;
 219     normalize in ⊢ (%→?); #H destruct (H)]
 220   |#Hcur_dst  #ls #x0 #xs #rs #sep #Hsrctc #Hnosep #Hsep #ls0 #x1 #target
 221    #c #rs0 #Hlen #Hdsttc >Hdsttc in Hcur_dst; normalize in ⊢ (%→?); #H destruct (H)
 222   ]
 223 | #td #te * #c0 * #c1 * * * #Hc0 #Hc1 #Hc0nosep #Hd #Hstar #IH #He
 224   lapply (IH He) -IH * #IH1 #IH2 %
 225   [ #ls #x #xs #rs #sep #Hsrc_tc #Hnosep #Hsep #ls0 #x0 #target
 226     #c #rs0 #Hlen #Hdst_tc
 227    >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
 228    >Hdst_tc in Hd; >Hsrc_tc @(list_cases2 … Hlen)
 229     [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
 230       [2: %1 %1 %{sep} % // >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
 231       >nth_change_vec //]
 232       >Hd -Hd @(eq_vec … (niltape ?))
 233       #i #Hi cases (decidable_eq_nat i src) #Hisrc
 234       [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 235         >nth_change_vec //
 236         >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 237         >nth_change_vec //
 238       | cases (decidable_eq_nat i dst) #Hidst
 239         [ >Hidst >nth_change_vec // >nth_change_vec //
 240           >Hdst_tc in Hc1; >Htargetnil
 241           normalize in ⊢ (%→?); #Hc1 destruct (Hc1) %
 242         | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 243           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
 244           >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 245           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] %
 246         ]
 247       ]
 248     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
 249       >(IH1 ls hd1 tl1 (c0::rs) sep ?? Hsep ls0 hd2 tl2 c (x0::rs0))
 250       [ >Hd >(change_vec_commute … ?? td ?? src dst) //
 251        >change_vec_change_vec
 252        >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
 253        >change_vec_change_vec
 254        >reverse_cons >associative_append
 255        >reverse_cons >associative_append %
 256      | >Hd >nth_change_vec // >Hdst_tc >Htarget >Hdst_tc in Hc1;
 257        normalize in ⊢ (%→?); #H destruct (H) //
 258      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
 259      | <Hxs #c1 #Hc1 @Hnosep @memb_cons //
 260      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
 261        >nth_change_vec // ]
 262    ]
 263  | >Hc0 >Hc1 * [* [ * #c * #Hc destruct (Hc) >Hc0nosep]] #Habs destruct (Habs)
 264  ] ]
 265 qed.
 266
 267 lemma terminate_parmoveL :  ∀src,dst,sig,n,is_sep,t.
 268   src ≠ dst → src < S n → dst < S n →
 269   parmove src dst sig n L is_sep ↓ t.
 270 #src #dst #sig #n #is_sep #t #Hneq #Hsrc #Hdst
 271 @(terminate_while … (sem_parmove_step …)) //
 272 <(change_vec_same … t src (niltape ?))
 273 cases (nth src (tape sig) t (niltape ?))
 274 [ % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 275 |2,3: #a0 #al0 % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 276 | #ls lapply t -t elim ls
 277   [#t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?);
 278    #H1 destruct (H1) #Hcurdst #Hxsep >change_vec_change_vec #Ht1 %
 279    #t2 * #y1 * #y2 * * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 280    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 281   |#l0 #ls0 #IH #t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec //
 282    normalize in ⊢ (%→?); #H destruct (H) #Hcurdst #Hxsep
 283    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 284   ]
 285 ]
 286 qed.
 287
 288 lemma sem_parmoveL : ∀src,dst,sig,n,is_sep.
 289   src ≠ dst → src < S n → dst < S n →
 290   parmove src dst sig n L is_sep ⊨ R_parmoveL src dst sig n is_sep.
 291 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst @WRealize_to_Realize
 292 [/2/ | @wsem_parmoveL //]
 293 qed.