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    outt = int).
 206
 207 lemma wsem_parmoveL : ∀src,dst,sig,n,is_sep.src ≠ dst → src < S n → dst < S n →
 208   parmove src dst sig n L is_sep ⊫ R_parmoveL src dst sig n is_sep.
 209 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 210 lapply (sem_while … (sem_parmove_step src dst sig n L is_sep Hneq Hsrc Hdst) … Hloop) //
 211 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
 212 [ #tc whd in ⊢ (%→?); * * [ *
 213   [ * #x * #Hx #Hsep #Houtc %
 214     [ #ls #x0 #xs #rs #sep #Hsrctc #Hnosep >Hsrctc in Hx; normalize in ⊢ (%→?);
 215       #Hx0 destruct (Hx0) lapply (Hnosep ? (memb_hd …)) >Hsep
 216       #Hfalse destruct (Hfalse)
 217     | #s #Hs #Hseps @Houtc ]
 218   | #Hcur #Houtc %
 219     [ #ls #x0 #xs #rs #sep #Hsrctc >Hsrctc in Hcur; normalize in ⊢ (%→?);
 220       #Hcur destruct (Hcur)
 221     | >Hcur #s #Hs destruct (Hs) ] ]
 222   | #Hcur #Houtc %
 223     [ #ls #x0 #xs #rs #sep #Hsrctc #Hnosep #Hsep #ls0 #x1 #target #c #rs0 #Hlen
 224       #Hdsttc >Hdsttc in Hcur; normalize in ⊢ (%→?); #Hcur destruct (Hcur)
 225     | #s #Hs #Hseps @Houtc ]
 226   ]
 227 | #tc #td #te * #c0 * #c1 * * * #Hc0 #Hc1 #Hc0nosep #Hd #Hstar #IH #He
 228   lapply (IH He) -IH * #IH1 #IH2 %
 229   [ #ls #x #xs #rs #sep #Hsrc_tc #Hnosep #Hsep #ls0 #x0 #target
 230     #c #rs0 #Hlen #Hdst_tc
 231     >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
 232 (*    <(change_vec_same … tc src (niltape ?)) in Hd:(???(???(???%??)??));
 233       <(change_vec_same … tc dst (niltape ?)) in ⊢(???(???(???%??)??)→?); *)
 234     >Hdst_tc in Hd; >Hsrc_tc
 235 (*    >change_vec_change_vec >change_vec_change_vec
 236       >(change_vec_commute ?? tc ?? dst src) [|@(sym_not_eq … Hneq)]
 237       >change_vec_change_vec *) @(list_cases2 … Hlen)
 238     [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >(IH2 … Hsep)
 239       [ >Hd -Hd @(eq_vec … (niltape ?))
 240         #i #Hi cases (decidable_eq_nat i src) #Hisrc
 241         [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 242           >nth_change_vec //
 243           >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
 244           >nth_change_vec //
 245         | cases (decidable_eq_nat i dst) #Hidst
 246           [ >Hidst >nth_change_vec // >nth_change_vec //
 247             >Hdst_tc in Hc1; >Htargetnil
 248             normalize in ⊢ (%→?); #Hc1 destruct (Hc1) %
 249           | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 250             >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
 251             >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
 252             >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % ]
 253          ]
 254        | >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
 255          >nth_change_vec // ]
 256     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
 257       >(IH1 ls hd1 tl1 (c0::rs) sep ?? Hsep ls0 hd2 tl2 c (x0::rs0))
 258       [ >Hd >(change_vec_commute … ?? tc ?? src dst) //
 259        >change_vec_change_vec
 260        >(change_vec_commute … ?? tc ?? dst src) [|@sym_not_eq //]
 261        >change_vec_change_vec
 262        >reverse_cons >associative_append
 263        >reverse_cons >associative_append %
 264      | >Hd >nth_change_vec // >Hdst_tc >Htarget >Hdst_tc in Hc1;
 265        normalize in ⊢ (%→?); #H destruct (H) //
 266      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
 267      | <Hxs #c1 #Hc1 @Hnosep @memb_cons //
 268      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
 269        >nth_change_vec // ]
 270    ]
 271  | #c #Hc #Hsepc >Hc in Hc0; #Hcc0 destruct (Hcc0) >Hc0nosep in Hsepc;
 272    #H destruct (H)
 273 ] ]
 274 qed.
 275
 276 lemma terminate_parmoveL :  ∀src,dst,sig,n,is_sep,t.
 277   src ≠ dst → src < S n → dst < S n →
 278   parmove src dst sig n L is_sep ↓ t.
 279 #src #dst #sig #n #is_sep #t #Hneq #Hsrc #Hdst
 280 @(terminate_while … (sem_parmove_step …)) //
 281 <(change_vec_same … t src (niltape ?))
 282 cases (nth src (tape sig) t (niltape ?))
 283 [ % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 284 |2,3: #a0 #al0 % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?); #Hx destruct
 285 | #ls lapply t -t elim ls
 286   [#t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec // normalize in ⊢ (%→?);
 287    #H1 destruct (H1) #Hcurdst #Hxsep >change_vec_change_vec #Ht1 %
 288    #t2 * #y1 * #y2 * * * >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
 289    >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H)
 290   |#l0 #ls0 #IH #t #c #rs % #t1 * #x1 * #x2 * * * >nth_change_vec //
 291    normalize in ⊢ (%→?); #H destruct (H) #Hcurdst #Hxsep
 292    >change_vec_change_vec >change_vec_commute // #Ht1 >Ht1 @IH
 293   ]
 294 ]
 295 qed.
 296
 297 lemma sem_parmoveL : ∀src,dst,sig,n,is_sep.
 298   src ≠ dst → src < S n → dst < S n →
 299   parmove src dst sig n L is_sep ⊨ R_parmoveL src dst sig n is_sep.
 300 #src #dst #sig #n #is_sep #Hneq #Hsrc #Hdst @WRealize_to_Realize /2/
 301 qed.