matita/matita/lib/turing/basic_machines.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/while_machine.ma".
  13
  14 (******************* write a given symbol under the head **********************)
  15 definition write_states ≝ initN 2.
  16
  17 definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  18 definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  19
  20 definition write ≝ λalpha,c.
  21   mk_TM alpha write_states
  22   (λp.let 〈q,a〉 ≝ p in
  23     match pi1 … q with
  24     [ O ⇒ 〈wr1,Some ? c,N〉
  25     | S _ ⇒ 〈wr1,None ?,N〉 ])
  26   wr0 (λx.x == wr1).
  27
  28 definition R_write ≝ λalpha,c,t1,t2.
  29   ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
  30
  31 lemma sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
  32 #alpha #c #t @(ex_intro … 2) @ex_intro
  33   [|% [% |#ls #c #rs #Ht >Ht % ] ]
  34 qed.
  35
  36 (******************** moves the head one step to the right ********************)
  37
  38 definition move_states ≝ initN 2.
  39 definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
  40 definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
  41
  42 definition move_r ≝
  43   λalpha:FinSet.mk_TM alpha move_states
  44   (λp.let 〈q,a〉 ≝ p in
  45     match a with
  46     [ None ⇒ 〈move1,None ?,N〉
  47     | Some a' ⇒ match (pi1 … q) with
  48       [ O ⇒ 〈move1,Some ? a',R〉
  49       | S q ⇒ 〈move1,None ?,N〉 ] ])
  50   move0 (λq.q == move1).
  51
  52 definition R_move_r ≝ λalpha,t1,t2.
  53   (current ? t1 = None ? → t1 = t2) ∧
  54   ∀ls,c,rs.
  55     t1 = midtape alpha ls c rs →
  56     t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
  57 (*
  58   (current ? t1 = None ? ∧ t1 = t2) ∨
  59   ∃ls,c,rs.
  60   t1 = midtape alpha ls c rs ∧
  61   t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).*)
  62
  63 lemma sem_move_r :
  64   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
  65 #alpha #intape @(ex_intro ?? 2) cases intape
  66 [ @ex_intro
  67   [| % [ % | % // #ls #c #rs #H destruct ] ]
  68 |#a #al @ex_intro
  69   [| % [ % | % // #ls #c #rs #H destruct ] ]
  70 |#a #al @ex_intro
  71   [| % [ % | % // #ls #c #rs #H destruct ] ]
  72 | #ls #c #rs
  73   @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
  74   #ls1 #c1 #rs1 #H destruct cases rs1 // ] ] ]
  75 qed.
  76
  77 (******************** moves the head one step to the left *********************)
  78
  79 definition move_l ≝
  80   λalpha:FinSet.mk_TM alpha move_states
  81   (λp.let 〈q,a〉 ≝ p in
  82     match a with
  83     [ None ⇒ 〈move1,None ?,N〉
  84     | Some a' ⇒ match pi1 … q with
  85       [ O ⇒ 〈move1,Some ? a',L〉
  86       | S q ⇒ 〈move1,None ?,N〉 ] ])
  87   move0 (λq.q == move1).
  88
  89 definition R_move_l ≝ λalpha,t1,t2.
  90   (current ? t1 = None ? → t1 = t2) ∧
  91   ∀ls,c,rs.
  92     t1 = midtape alpha ls c rs →
  93     t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
  94
  95 lemma sem_move_l :
  96   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
  97 #alpha #intape @(ex_intro ?? 2) cases intape
  98 [ @ex_intro
  99   [| % [ % | % // #ls #c #rs #H destruct ] ]
 100 |#a #al @ex_intro
 101   [| % [ % | % // #ls #c #rs #H destruct ] ]
 102 |#a #al @ex_intro
 103   [| % [ % | % // #ls #c #rs #H destruct ] ]
 104 | #ls #c #rs
 105   @ex_intro [| % [ % | % [whd in ⊢ ((??%?)→?); #H destruct]
 106   #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 107 qed.
 108
 109 (********************************* test char **********************************)
 110
 111 (* the test_char machine ends up in two different states q1 and q2 wether or not
 112 the current character satisfies a boolean test function passed as a parameter to
 113 the machine.
 114 The machine ends up in q1 also in case there is no current character.
 115 *)
 116
 117 definition tc_states ≝ initN 3.
 118
 119 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 120 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 121 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 122
 123 definition test_char ≝
 124   λalpha:FinSet.λtest:alpha→bool.
 125   mk_TM alpha tc_states
 126   (λp.let 〈q,a〉 ≝ p in
 127    match a with
 128    [ None ⇒ 〈tc_false, None ?,N〉
 129    | Some a' ⇒
 130      match test a' with
 131      [ true ⇒ 〈tc_true,None ?,N〉
 132      | false ⇒ 〈tc_false,None ?,N〉 ]])
 133   tc_start (λx.notb (x == tc_start)).
 134
 135 definition Rtc_true ≝
 136   λalpha,test,t1,t2.
 137    (∃c. current alpha t1 = Some ? c ∧ test c = true) ∧ t2 = t1.
 138
 139 definition Rtc_false ≝
 140   λalpha,test,t1,t2.
 141     (∀c. current alpha t1 = Some ? c → test c = false) ∧ t2 = t1.
 142
 143 lemma tc_q0_q1 :
 144   ∀alpha,test,ls,a0,rs. test a0 = true →
 145   step alpha (test_char alpha test)
 146     (mk_config ?? tc_start (midtape … ls a0 rs)) =
 147   mk_config alpha (states ? (test_char alpha test)) tc_true
 148     (midtape … ls a0 rs).
 149 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 150 whd in match (trans … 〈?,?〉); >Htest %
 151 qed.
 152
 153 lemma tc_q0_q2 :
 154   ∀alpha,test,ls,a0,rs. test a0 = false →
 155   step alpha (test_char alpha test)
 156     (mk_config ?? tc_start (midtape … ls a0 rs)) =
 157   mk_config alpha (states ? (test_char alpha test)) tc_false
 158     (midtape … ls a0 rs).
 159 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 160 whd in match (trans … 〈?,?〉); >Htest %
 161 qed.
 162
 163 lemma sem_test_char :
 164   ∀alpha,test.
 165   accRealize alpha (test_char alpha test)
 166     tc_true (Rtc_true alpha test) (Rtc_false alpha test).
 167 #alpha #test *
 168 [ @(ex_intro ?? 2)
 169   @(ex_intro ?? (mk_config ?? tc_false (niltape ?))) %
 170   [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 171 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (leftof ? a al)))
 172   % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 173 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_false (rightof ? a al)))
 174   % [ % // normalize #Hfalse destruct | #_ normalize % // #c #Hfalse destruct (Hfalse) ]
 175 | #ls #c #rs @(ex_intro ?? 2)
 176   cases (true_or_false (test c)) #Htest
 177   [ @(ex_intro ?? (mk_config ?? tc_true ?))
 178     [| %
 179       [ %
 180         [ whd in ⊢ (??%?); >tc_q0_q1 //
 181         | #_ % // @(ex_intro … c) /2/]
 182       | * #Hfalse @False_ind @Hfalse % ]
 183     ]
 184   | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
 185     %
 186     [ %
 187       [ whd in ⊢ (??%?); >tc_q0_q2 //
 188       | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
 189     | #_ % // #c0 whd in ⊢ ((??%?)→?); #Hc0 destruct (Hc0) //
 190     ]
 191   ]
 192 ]
 193 qed.
 194
 195 lemma test_char_inv :
 196   ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
 197 #sig #P #f #t #t0 #HPt * #_ //
 198 qed.
 199
 200 definition test_null ≝ λalpha.test_char alpha (λ_.true).
 201
 202 definition R_test_null_true ≝ λalpha,t1,t2.
 203   current alpha t1 ≠ None ? ∧ t1 = t2.
 204
 205 definition R_test_null_false ≝ λalpha,t1,t2.
 206   current alpha t1 = None ? ∧ t1 = t2.
 207
 208 lemma sem_test_null : ∀alpha.
 209   test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
 210 #alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
 211 #Hfalse %{k} %{outc} % [ %
 212 [ @Hloop
 213 | #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
 214   [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
 215 | #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
 216   [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd
 217     lapply (Habsurd ? (refl ??)) #H destruct (H)
 218   | <Houtc % ] ]
 219 qed.
 220
 221 (************************************* swap ***********************************)
 222 definition swap_states : FinSet → FinSet ≝
 223   λalpha:FinSet.FinProd (initN 4) alpha.
 224
 225 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
 226 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
 227 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
 228 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
 229
 230 definition swap_r ≝
 231  λalpha:FinSet.λfoo:alpha.
 232  mk_TM alpha (swap_states alpha)
 233  (λp.let 〈q,a〉 ≝ p in
 234   let 〈q',b〉 ≝ q in
 235   let q' ≝ pi1 nat (λi.i<4) q' in
 236   match a with
 237   [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
 238   | Some a' ⇒
 239   match q' with
 240   [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉  (* save in register and move R *)
 241   | S q' ⇒ match q' with
 242     [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
 243     | S q' ⇒ match q' with
 244       [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
 245       | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
 246       ]
 247     ]
 248   ]])
 249   〈swap0,foo〉
 250   (λq.\fst q == swap3).
 251
 252 definition Rswap_r ≝
 253   λalpha,t1,t2.
 254     (∀b,ls.
 255       t1 = midtape alpha ls b [ ] →
 256       t2 = rightof ? b ls) ∧
 257     (∀a,b,ls,rs.
 258       t1 = midtape alpha ls b (a::rs) →
 259       t2 = midtape alpha ls a (b::rs)).
 260
 261 lemma sem_swap_r : ∀alpha,foo.
 262   swap_r alpha foo ⊨ Rswap_r alpha.
 263 #alpha #foo *
 264   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
 265    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 266   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
 267    % [% | % [#b #ls | #a #b #ls #rs] #H destruct]
 268   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
 269    % [% |% [#b #ls | #a #b #ls #rs] #H destruct]
 270   | #lt #c #rt @(ex_intro ?? 4) cases rt
 271     [@ex_intro [|% [ % | %
 272       [#b #ls #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 273     |#r0 #rt0 @ex_intro [| % [ % | %
 274       [#b #ls #H destruct | #a #b #ls #rs #H destruct normalize //
 275     ]
 276   ]
 277 qed.
 278
 279 definition swap_l ≝
 280  λalpha:FinSet.λfoo:alpha.
 281  mk_TM alpha (swap_states alpha)
 282  (λp.let 〈q,a〉 ≝ p in
 283   let 〈q',b〉 ≝ q in
 284   let q' ≝ pi1 nat (λi.i<4) q' in
 285   match a with
 286   [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
 287   | Some a' ⇒
 288   match q' with
 289   [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉  (* save in register and move L *)
 290   | S q' ⇒ match q' with
 291     [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
 292     | S q' ⇒ match q' with
 293       [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
 294       | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
 295       ]
 296     ]
 297   ]])
 298   〈swap0,foo〉
 299   (λq.\fst q == swap3).
 300
 301 definition Rswap_l ≝
 302   λalpha,t1,t2.
 303    (∀b,rs.
 304      t1 = midtape alpha [ ] b rs →
 305      t2 = leftof ? b rs) ∧
 306    (∀a,b,ls,rs.
 307       t1 = midtape alpha (a::ls) b rs →
 308       t2 = midtape alpha (b::ls) a rs).
 309
 310 lemma sem_swap_l : ∀alpha,foo.
 311   swap_l alpha foo ⊨ Rswap_l alpha.
 312 #alpha #foo *
 313   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
 314    % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
 315   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
 316    % [% | % [#b #rs | #a #b #ls #rs] #H destruct]
 317   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
 318    % [% |% [#b #rs | #a #b #ls #rs] #H destruct]
 319   | #lt #c #rt @(ex_intro ?? 4) cases lt
 320     [@ex_intro [|% [ % | %
 321       [#b #rs #H destruct normalize // |#a #b #ls #rs #H destruct]]]
 322     |#r0 #rt0 @ex_intro [| % [ % | %
 323       [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
 324     ]
 325   ]
 326 qed.