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) (〈None sig,D〉) src)
  51                           (〈None ?,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_mono ? (nth src ? int (niltape ?)) (〈None ?,D〉)) src)
  70             (tape_move_mono ? (nth dst ? int (niltape ?)) (〈None ?,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_mono ? (nth src ? v (niltape ?)) (〈None ?, D〉)) src)
 135        (tape_move_mono ? (nth dst ? v (niltape ?)) (〈None ?, 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 whd in ⊢ (??(????(???%))?);
 143   <(change_vec_same ?? v dst (niltape ?)) in ⊢ (??%?);
 144   >tape_move_multi_def >pmap_change
 145   <(change_vec_same ?? v src (niltape ?)) in ⊢ (??%?);
 146   >pmap_change <tape_move_multi_def >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     | normalize in ⊢ (%→?); #H destruct (H) ]
 163     | #_ % // % %2 // ] ]
 164 | #a #Ha cases (true_or_false (is_sep a)) #Hsep
 165   [ %{2} %
 166     [| % [ %
 167       [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
 168       | normalize in ⊢ (%→?); #H destruct (H) ]
 169       | #_ % // % % %{a} % // ] ]
 170   | lapply (refl ? (current ? (nth dst ? int (niltape ?))))
 171     cases (current ? (nth dst ? int (niltape ?))) in ⊢ (???%→?);
 172     [ #Hcurdst %{2} %
 173       [| % [ %
 174         [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/
 175         | normalize in ⊢ (%→?); #H destruct (H) ]
 176         | #_ % // %2 // ] ]
 177     | #b #Hb %{2} %
 178       [| % [ %
 179         [whd in ⊢  (??%?);  >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
 180         | #_ %{a} %{b} % // % // % // ]
 181         | * #H @False_ind @H % ]
 182 ]]]]
 183 qed.
 184
 185 definition parmove ≝ λsrc,dst,sig,n,D,is_sep.
 186   whileTM … (parmove_step src dst sig n D is_sep) parmove1.
 187
 188 definition R_parmoveL ≝
 189   λsrc,dst,sig,n,is_sep.λint,outt: Vector (tape sig) (S n).
 190   (∀ls,x,xs,rs,sep.
 191     nth src ? int (niltape ?) = midtape sig (xs@sep::ls) x rs →
 192     (∀c.memb ? c (x::xs) = true → is_sep c = false) → is_sep sep = true →
 193     ∀ls0,x0,target,c,rs0.|xs| = |target| →
 194     nth dst ? int (niltape ?) = midtape sig (target@c::ls0) x0 rs0 →
 195     outt = change_vec ??
 196            (change_vec ?? int (midtape sig ls sep (reverse ? xs@x::rs)) src)
 197            (midtape sig ls0 c (reverse ? target@x0::rs0)) dst) ∧
 198   (((∃s.current ? (nth src ? int (niltape ?)) = Some ? s ∧ is_sep s = true) ∨
 199      current ? (nth src ? int (niltape ?)) = None ? ∨
 200      current ? (nth dst ? int (niltape ?)) = None ?) →
 201      outt = int).
 202
 203 lemma wsem_parmoveL : ∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n →
 204   parmove src dst sig n L is_sep ⊫ R_parmoveL src dst sig n is_sep.
 205 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 206 lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) … Hloop) //
 207 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 208 [ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H
 209   [ * [ * #x * #Hx #Hsep #ls #x0 #xs #rs #sep #Hsrctc #Hnosep >Hsrctc in Hx; normalize in ⊢ (%→?);
 210     #Hx0 destruct (Hx0) lapply (Hnosep ? (memb_hd …)) >Hsep
 211     #Hfalse destruct (Hfalse)
 212   | #Hcur_src #ls #x0 #xs #rs #sep #Hsrctc >Hsrctc in Hcur_src;
 213     normalize in ⊢ (%→?); #H destruct (H)]
 214   |#Hcur_dst  #ls #x0 #xs #rs #sep #Hsrctc #Hnosep #Hsep #ls0 #x1 #target
 215    #c #rs0 #Hlen #Hdsttc >Hdsttc in Hcur_dst; normalize in ⊢ (%→?); #H destruct (H)
 216   ]
 217 | #td #te * #c0 * #c1 * * * #Hc0 #Hc1 #Hc0nosep #Hd #Hstar #IH #He
 218   lapply (IH He) -IH * #IH1 #IH2 %
 219   [ #ls #x #xs #rs #sep #Hsrc_tc #Hnosep #Hsep #ls0 #x0 #target
 220     #c #rs0 #Hlen #Hdst_tc
 221    >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
 222    >Hdst_tc in Hd; >Hsrc_tc @(list_cases2 … Hlen)
 223     [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2
 224       [2: %1 %1 %{sep} % // >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
 225       >nth_change_vec //]
 226       >Hd -Hd @(eq_vec … (niltape ?))
 227       #i #Hi cases (decidable_eq_nat i src) #Hisrc
 228       [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 229         >nth_change_vec //
 230       | cases (decidable_eq_nat i dst) #Hidst
 231         [ >Hidst >nth_change_vec //
 232         | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 233           >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] %
 234         ]
 235       ]
 236     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
 237       >(IH1 ls hd1 tl1 (c0::rs) sep ?? Hsep ls0 hd2 tl2 c (x0::rs0))
 238       [ >Hd >(change_vec_commute … ?? td ?? src dst) //
 239        >change_vec_change_vec
 240        >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
 241        >change_vec_change_vec
 242        >reverse_cons >associative_append
 243        >reverse_cons >associative_append %
 244      | >Hd >nth_change_vec //
 245      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
 246      | <Hxs #c1 #Hc1 @Hnosep @memb_cons //
 247      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
 248        >nth_change_vec // ]
 249    ]
 250  | >Hc0 >Hc1 * [* [ * #c * #Hc destruct (Hc) >Hc0nosep]] #Habs destruct (Habs)
 251  ] ]
 252 qed.
 253
 254 lemma terminate_parmoveL :  ∀src,dst,sig,n,is_sep,t.
 255   src ≠ dst → src < S n → dst < S n →
 256   parmove src dst sig n L is_sep ↓ t.
 257 #src #dst #sig #n #is_sep #t #Hneq #Hsrc #Hdst
 258 @(terminate_while … (sem_parmove_step …)) //
 259 <(change_vec_same … t src (niltape ?))
 260 cases (nth src (tape sig) t (niltape ?))
 261 [ % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 262 |2,3: #a0 #al0 % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 263 | #ls lapply t -t elim ls
 264   [#t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?);
 265    #H1 destruct (H1) #Hcurdst #Hxsep >change_vec_change_vec #Ht1 %
 266    #t2 * #y1 * #y2 * * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 267    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 268   |#l0 #ls0 #IH #t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec //
 269    normalize in ⊢ (%→?); #H destruct (H) #Hcurdst #Hxsep
 270    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 271   ]
 272 ]
 273 qed.
 274
 275 lemma sem_parmoveL : ∀src,dst,sig,n,is_sep.
 276   src ≠ dst → src < S n → dst < S n →
 277   parmove src dst sig n L is_sep ⊨ R_parmoveL src dst sig n is_sep.
 278 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst @WRealize_to_Realize
 279 [/2/ | @wsem_parmoveL //]
 280 qed.