matita/matita/lib/turing/auxiliary_machines1.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/basic_machines.ma".
  13 include "turing/if_machine.ma".
  14
  15 (* move until test *)
  16 definition mut_step ≝ λalpha,D,test.
  17 ifTM ? (test_char alpha test) (single_finalTM ? (move alpha D)) (nop ?) tc_true.
  18
  19 definition R_mut_step_true ≝ λalpha,D,test,t1,t2.
  20   ∃ls,c,rs.
  21     t1 = midtape alpha ls c rs ∧ test c = true ∧ t2 = tape_move ? t1 D.
  22
  23 definition R_mut_step_false ≝ λalpha,test.λt1,t2:tape alpha.
  24   (∀ls,c,rs.t1 = midtape alpha ls c rs → test c = false)
  25   ∧ t2 = t1.
  26
  27 definition mut_acc : ∀alpha,D,test.states ? (mut_step alpha D test) ≝
  28 λalpha,D,test.(inr … (inl … (inr … start_nop))).
  29
  30 lemma sem_mut_step :
  31   ∀alpha,D,test.mut_step alpha D test ⊨
  32    [ mut_acc … : R_mut_step_true alpha D test, R_mut_step_false alpha test] .
  33 #alpha #D #tets #ta
  34 @(acc_sem_if_app ??????????? (sem_test_char …)
  35   (sem_move_single …) (sem_nop alpha) ??)
  36   [#tb #tc #td * * #c * #Hcurtb #Htrue
  37    cases (current_to_midtape … Hcurtb) #ls * #rs #Hmidtb
  38    #tbtd #Hmove %{ls} %{c} %{rs} % // % //
  39   |#tb #tc #td * #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd % //
  40    lapply (refl ? (current ? tb)) cases (current ? tb) in ⊢ (???%→?);
  41     [#H #ls #c #rs #Htb >Htb in H; normalize #HF destruct (HF)
  42     |#c #H #ls #c0 #rs #Htb @Hcurtb >Htb //
  43     ]
  44   ]
  45 qed.
  46
  47 definition move_until ≝ λsig,D,test.
  48   whileTM sig (mut_step sig D test) (mut_acc …).
  49
  50 definition R_move_l_until ≝
  51   λsig,test,t1,t2.
  52   (current ? t1 = None ? → t2 = t1) ∧
  53   ∀ls,a,rs.t1 = midtape sig ls a rs →
  54     (test a = false ∧ t2 = t1) ∨
  55     ((∃ls1,b,ls2.
  56        ls = ls1@b::ls2 ∧
  57        test b = false ∧
  58         (∀x. mem ? x (a::ls1) → test x = true) ∧
  59         t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)) ∨
  60       (∃b,lss.
  61         (∀x. mem ? x (a::ls) → test x = true) ∧
  62         a::ls = lss@[b] ∧
  63         t2 = leftof ? b ((reverse ? lss)@rs))).
  64
  65 lemma sem_move_L_until:
  66   ∀sig,test.
  67   WRealize sig (move_until sig L test) (R_move_l_until sig test).
  68 #sig #test #inc #j #outc #Hloop
  69 lapply (sem_while … (sem_mut_step sig L test) inc j outc Hloop) [%]
  70 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
  71 [ whd in ⊢ (% → ?); * #H1 #H2 %
  72   [#Htape1 @H2
  73   |#ls #a #rs #Htapea % % [@(H1 … Htapea) |@H2]
  74   ]
  75 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
  76   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
  77   * #IH1 #IH2 %
  78   [#Htapeb cases Hstar1 #ls * #b * #rs * *
  79    #H1 >H1 in Htapeb; whd in ⊢ (??%?→?); #H destruct (H)
  80   |#ls #b0 #rs #Htapeb cases Hstar1
  81    #ls1 * #b * #rs1 * * >Htapeb #H destruct (H)
  82    #Hb cases ls1
  83     [whd in ⊢ (???%→?); #Htapec >Htapec in IH1; #IH1
  84      %2 %2 %{b} %{[ ]} % [% [#x * [//|@False_ind] | //] |@IH1 //]
  85     |#a #ls2 whd in ⊢ (???%→?); #Htapec
  86      %2 cases (IH2 … Htapec)
  87       [* #afalse #Hout %1
  88        %{[ ]} %{a} %{ls2}
  89        %[%[%[//|//] |#x * [#eqxa >eqxa // |@False_ind]]
  90         |>Hout >reverse_single @Htapec
  91         ]
  92       |*
  93         [-IH1 -IH2 #IH
  94          %1 cases IH -IH #ls3 * #b0 * #ls4 * * * #H1 #H2 #H3 #H4
  95          %{(a::ls3)} %{b0} %{ls4}
  96          %[%[%[>H1 //|//]| #x * [#eqxb >eqxb //|@H3]]
  97           |>H4 >reverse_cons in ⊢ (???%); >associative_append //
  98           ]
  99         |-IH1 -IH2 #IH
 100          %2 cases IH -IH #b0 * #ls3 * * #H1 #H2 #H3
 101          %{b0} %{(b::ls3)}
 102          %[%[#x * [#eqxb >eqxb //|@H1]|>H2 //]
 103           |>H3 >reverse_cons in ⊢ (???%); >associative_append //
 104           ]
 105         ]
 106       ]
 107     ]
 108   ]
 109 qed.
 110
 111 definition R_move_R_until ≝
 112   λsig,test,t1,t2.
 113   (current ? t1 = None ? → t2 = t1) ∧
 114   ∀ls,a,rs.t1 = midtape sig ls a rs →
 115     (test a = false ∧ t2 = t1) ∨
 116     ((∃rs1,b,rs2.
 117        rs = rs1@b::rs2 ∧
 118        test b = false ∧
 119         (∀x. mem ? x (a::rs1) → test x = true) ∧
 120         t2 = midtape ? ((reverse ? (a::rs1))@ls) b rs2) ∨
 121       (∃b,rss.
 122         (∀x. mem ? x (a::rs) → test x = true) ∧
 123         a::rs = rss@[b] ∧
 124         t2 = rightof ? b ((reverse ? rss)@ls))).
 125
 126 lemma sem_move_R_until:
 127   ∀sig,test.
 128   WRealize sig (move_until sig R test) (R_move_R_until sig test).
 129 #sig #test #inc #j #outc #Hloop
 130 lapply (sem_while … (sem_mut_step sig R test) inc j outc Hloop) [%]
 131 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 132 [ whd in ⊢ (% → ?); * #H1 #H2 %
 133   [#Htape1 @H2
 134   |#ls #a #rs #Htapea % % [@(H1 … Htapea) |@H2]
 135   ]
 136 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 137   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
 138   * #IH1 #IH2 %
 139   [#Htapeb cases Hstar1 #ls * #b * #rs * *
 140    #H1 >H1 in Htapeb; whd in ⊢ (??%?→?); #H destruct (H)
 141   |#ls #b0 #rs #Htapeb cases Hstar1
 142    #ls1 * #b * #rs1 * * >Htapeb #H destruct (H)
 143    #Hb cases rs1
 144     [whd in ⊢ (???%→?); #Htapec >Htapec in IH1; #IH1
 145      %2 %2 %{b} %{[ ]} % [% [#x * [//|@False_ind] | //] |@IH1 //]
 146     |#a #rs2 whd in ⊢ (???%→?); #Htapec
 147      %2 cases (IH2 … Htapec)
 148       [* #afalse #Hout %1
 149        %{[ ]} %{a} %{rs2}
 150        %[%[%[//|//] |#x * [#eqxa >eqxa // |@False_ind]]
 151         |>Hout >reverse_single @Htapec
 152         ]
 153       |*
 154         [-IH1 -IH2 #IH
 155          %1 cases IH -IH #rs3 * #b0 * #rs4 * * * #H1 #H2 #H3 #H4
 156          %{(a::rs3)} %{b0} %{rs4}
 157          %[%[%[>H1 //|//]| #x * [#eqxb >eqxb //|@H3]]
 158           |>H4 >reverse_cons in ⊢ (???%); >associative_append //
 159           ]
 160         |-IH1 -IH2 #IH
 161          %2 cases IH -IH #b0 * #rs3 * * #H1 #H2 #H3
 162          %{b0} %{(b::rs3)}
 163          %[%[#x * [#eqxb >eqxb //|@H1]|>H2 //]
 164           |>H3 >reverse_cons in ⊢ (???%); >associative_append //
 165           ]
 166         ]
 167       ]
 168     ]
 169   ]
 170 qed.
 171
 172 (* termination *)
 173
 174 lemma WF_mut_niltape:
 175   ∀alpha,D,test. WF ? (inv ? (R_mut_step_true alpha D test)) (niltape alpha).
 176 #alpha #D #test @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * * #H destruct
 177 qed.
 178
 179 lemma WF_mut_rightof:
 180   ∀alpha,D,test,a,ls. WF ? (inv ? (R_mut_step_true alpha D test)) (rightof alpha a ls).
 181 #alpha #D #test #a #ls @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * * #H destruct
 182 qed.
 183
 184 lemma WF_mut_leftof:
 185   ∀alpha,D,test,a,rs. WF ? (inv ? (R_mut_step_true alpha D test)) (leftof alpha a rs).
 186 #alpha #D #test #a #rs @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * * #H destruct
 187 qed.
 188
 189 lemma terminate_move_until_L:
 190   ∀alpha,test.∀t. Terminate alpha (move_until alpha L test) t.
 191 #alpha #test #t @(terminate_while … (sem_mut_step alpha L test)) [%]
 192 cases t // #ls elim ls
 193   [#c1 #l1 @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * *
 194    #_ #_ #Ht1 >Ht1 //
 195   |#a #ls1 #Hind #c1 #l1 @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * *
 196    #_ #_ #Ht1 >Ht1 //
 197   ]
 198 qed.
 199
 200 lemma terminate_move_until_R:
 201   ∀alpha,test.∀t. Terminate alpha (move_until alpha R test) t.
 202 #alpha #test #t @(terminate_while … (sem_mut_step alpha R test)) [%]
 203 cases t // #ls #c #rs lapply c -c lapply ls -ls elim rs
 204   [#c1 #l1 @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * *
 205    #_ #_ #Ht1 >Ht1 //
 206   |#a #ls1 #Hind #c1 #l1 @wf #t1 whd in ⊢ (%→?); * #ls * #b * #rs * *
 207    #_ #_ #Ht1 >Ht1 //
 208   ]
 209 qed.
 210
 211 lemma ssem_move_until_L :
 212   ∀alpha,test.
 213   Realize alpha (move_until alpha L test) (R_move_l_until alpha test).
 214 /2/ qed.
 215
 216 lemma ssem_move_until_R :
 217   ∀alpha,test.
 218   Realize alpha (move_until alpha R test) (R_move_R_until alpha test).
 219 /2/ qed.
 220
 221 (*********************************** extend ***********************************)
 222 (* if current = Null write a character a. Used to dynamically extend the tape *)
 223
 224 definition extend ≝ λalpha,a.
 225   ifTM ? (test_null alpha) (nop ?) (write alpha a) tc_true.
 226
 227 definition R_extend ≝ λalpha,a,t1,t2.
 228   (current ? t1 = None ? → t2 = midtape alpha (left ? t1) a (right ? t1)) ∧
 229   (current ? t1 ≠ None ? → t2 = t1).
 230
 231 lemma sem_extend : ∀alpha,a.
 232   extend alpha a ⊨ R_extend alpha a.
 233 #alpha #a #ta
 234 @(sem_if_app … (sem_test_null …) (sem_nop … ) (sem_write_strong …) ??)
 235 -ta #t1 #t2 #t3 *
 236   [* * #H1 #H2 #H3 %
 237     [#Hcur >Hcur in H1; * #H @False_ind @H //|#_ >H2 @H3]
 238   |* * #H1 #H2 #H3 %
 239     [#_ >H2 @H3 | >H1 * #H @False_ind @H //]
 240   ]
 241 qed.
 242
 243 (********************************** extend1 ***********************************)
 244 (* a slightly different version: we add a to the left of the current position *)
 245
 246 definition extendL ≝ λalpha,a.
 247   (move_l alpha) · (write alpha a) · (move_r alpha).
 248
 249 definition R_extendL ≝ λalpha,a,t1,t2.
 250   (∀b,ls. t1 = leftof ? b ls → t2 = midtape alpha [a] b ls) ∧
 251   (∀b,ls,rs. t1 = midtape ? ls b rs → t2 = midtape alpha (a::(tail ? ls)) b rs).
 252
 253 lemma sem_extendL : ∀alpha,a.
 254   extendL alpha a ⊨ R_extendL alpha a.
 255 #alpha #a
 256 @(sem_seq_app … (sem_move_l …)
 257   (sem_seq … (sem_write_strong … ) (sem_move_r …) …))
 258 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * #Ht2 * #_ #Ht3 %
 259   [#b #ls #Htin >Htin in Ht1a; #Ht1 <(Ht1 … (refl … )) in Ht2;
 260    normalize in ⊢ (%→?); #Ht2 @(Ht3 … Ht2)
 261   |#b #ls #rs #Htin lapply (Ht1b … Htin) #Ht1 >Ht1 in Ht2;
 262    #Ht2 lapply(Ht3 ??? Ht2) cases ls normalize //
 263   ]
 264 qed.