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 ?〉 ])
  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 ?〉
  47     | Some a' ⇒ match (pi1 … q) with
  48       [ O ⇒ 〈move1,Some ? 〈a',R〉〉
  49       | S q ⇒ 〈move1,None ?〉 ] ])
  50   move0 (λq.q == move1).
  51
  52 definition R_move_r ≝ λalpha,t1,t2.
  53   ∀ls,c,rs.
  54   t1 = midtape alpha ls c rs →
  55   t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
  56
  57 lemma sem_move_r :
  58   ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
  59 #alpha #intape @(ex_intro ?? 2) cases intape
  60 [ @ex_intro
  61   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
  62 |#a #al @ex_intro
  63   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
  64 |#a #al @ex_intro
  65   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
  66 | #ls #c #rs
  67   @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
  68   cases rs0 // ] ] ]
  69 qed.
  70
  71 (******************** moves the head one step to the left *********************)
  72
  73 definition move_l ≝
  74   λalpha:FinSet.mk_TM alpha move_states
  75   (λp.let 〈q,a〉 ≝ p in
  76     match a with
  77     [ None ⇒ 〈move1,None ?〉
  78     | Some a' ⇒ match pi1 … q with
  79       [ O ⇒ 〈move1,Some ? 〈a',L〉〉
  80       | S q ⇒ 〈move1,None ?〉 ] ])
  81   move0 (λq.q == move1).
  82
  83 definition R_move_l ≝ λalpha,t1,t2.
  84   ∀ls,c,rs.
  85   t1 = midtape alpha ls c rs →
  86   t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
  87
  88 lemma sem_move_l :
  89   ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
  90 #alpha #intape @(ex_intro ?? 2) cases intape
  91 [ @ex_intro
  92   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
  93 |#a #al @ex_intro
  94   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
  95 |#a #al @ex_intro
  96   [| % [ % | #ls #c #rs #Hfalse destruct ] ]
  97 | #ls #c #rs
  98   @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
  99   cases ls0 // ] ] ]
 100 qed.
 101
 102 (********************************* test char **********************************)
 103
 104 (* the test_char machine ends up in two different states q1 and q2 wether or not
 105 the current character satisfies a boolean test function passed as a parameter to
 106 the machine.
 107 The machine ends up in q1 also in case there is no current character.
 108 *)
 109
 110 definition tc_states ≝ initN 3.
 111
 112 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 113 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 114 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 115
 116 definition test_char ≝
 117   λalpha:FinSet.λtest:alpha→bool.
 118   mk_TM alpha tc_states
 119   (λp.let 〈q,a〉 ≝ p in
 120    match a with
 121    [ None ⇒ 〈tc_true, None ?〉
 122    | Some a' ⇒
 123      match test a' with
 124      [ true ⇒ 〈tc_true,None ?〉
 125      | false ⇒ 〈tc_false,None ?〉 ]])
 126   tc_start (λx.notb (x == tc_start)).
 127
 128 definition Rtc_true ≝
 129   λalpha,test,t1,t2.
 130    ∀c. current alpha t1 = Some ? c → test c = true ∧ t2 = t1.
 131
 132 definition Rtc_false ≝
 133   λalpha,test,t1,t2.
 134     ∀c. current alpha t1 = Some ? c → test c = false ∧ t2 = t1.
 135
 136 lemma tc_q0_q1 :
 137   ∀alpha,test,ls,a0,rs. test a0 = true →
 138   step alpha (test_char alpha test)
 139     (mk_config ?? tc_start (midtape … ls a0 rs)) =
 140   mk_config alpha (states ? (test_char alpha test)) tc_true
 141     (midtape … ls a0 rs).
 142 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 143 whd in match (trans … 〈?,?〉); >Htest %
 144 qed.
 145
 146 lemma tc_q0_q2 :
 147   ∀alpha,test,ls,a0,rs. test a0 = false →
 148   step alpha (test_char alpha test)
 149     (mk_config ?? tc_start (midtape … ls a0 rs)) =
 150   mk_config alpha (states ? (test_char alpha test)) tc_false
 151     (midtape … ls a0 rs).
 152 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
 153 whd in match (trans … 〈?,?〉); >Htest %
 154 qed.
 155
 156 lemma sem_test_char :
 157   ∀alpha,test.
 158   accRealize alpha (test_char alpha test)
 159     tc_true (Rtc_true alpha test) (Rtc_false alpha test).
 160 #alpha #test *
 161 [ @(ex_intro ?? 2)
 162   @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) %
 163   [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 164 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al)))
 165   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 166 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al)))
 167   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 168 | #ls #c #rs @(ex_intro ?? 2)
 169   cases (true_or_false (test c)) #Htest
 170   [ @(ex_intro ?? (mk_config ?? tc_true ?))
 171     [| %
 172       [ %
 173         [ whd in ⊢ (??%?); >tc_q0_q1 //
 174         | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
 175       | * #Hfalse @False_ind @Hfalse % ]
 176     ]
 177   | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
 178     %
 179     [ %
 180       [ whd in ⊢ (??%?); >tc_q0_q2 //
 181       | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
 182     | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
 183     ]
 184   ]
 185 ]
 186 qed.
 187
 188 (************************************* swap ***********************************)
 189 definition swap_states : FinSet → FinSet ≝
 190   λalpha:FinSet.FinProd (initN 4) alpha.
 191
 192 definition swap0 : initN 4 ≝ mk_Sig ?? 0 (leb_true_to_le 1 4 (refl …)).
 193 definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
 194 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
 195 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
 196
 197 definition swap_r ≝
 198  λalpha:FinSet.λfoo:alpha.
 199  mk_TM alpha (swap_states alpha)
 200  (λp.let 〈q,a〉 ≝ p in
 201   let 〈q',b〉 ≝ q in
 202   let q' ≝ pi1 nat (λi.i<4) q' in
 203   match a with
 204   [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
 205   | Some a' ⇒
 206   match q' with
 207   [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',R〉〉  (* save in register and move R *)
 208   | S q' ⇒ match q' with
 209     [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,L〉〉 (* swap with register and move L *)
 210     | S q' ⇒ match q' with
 211       [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
 212       | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
 213       ]
 214     ]
 215   ]])
 216   〈swap0,foo〉
 217   (λq.\fst q == swap3).
 218
 219 definition Rswap ≝
 220   λalpha,t1,t2.
 221    ∀a,b,ls,rs.
 222     t1 = midtape alpha ls b (a::rs) →
 223     t2 = midtape alpha ls a (b::rs).
 224
 225 lemma sem_swap_r : ∀alpha,foo.
 226   swap_r alpha foo ⊨ Rswap alpha.
 227 #alpha #foo *
 228   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
 229    % [% |#a #b #ls #rs #H destruct]
 230   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
 231    % [% |#a #b #ls #rs #H destruct]
 232   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
 233    % [% |#a #b #ls #rs #H destruct]
 234   | #lt #c #rt @(ex_intro ?? 4) cases rt
 235     [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
 236     |#r0 #rt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
 237     ]
 238   ]
 239 qed.
 240
 241 definition swap_l ≝
 242  λalpha:FinSet.λfoo:alpha.
 243  mk_TM alpha (swap_states alpha)
 244  (λp.let 〈q,a〉 ≝ p in
 245   let 〈q',b〉 ≝ q in
 246   let q' ≝ pi1 nat (λi.i<4) q' in
 247   match a with
 248   [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
 249   | Some a' ⇒
 250   match q' with
 251   [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',L〉〉  (* save in register and move L *)
 252   | S q' ⇒ match q' with
 253     [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,R〉〉 (* swap with register and move R *)
 254     | S q' ⇒ match q' with
 255       [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
 256       | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
 257       ]
 258     ]
 259   ]])
 260   〈swap0,foo〉
 261   (λq.\fst q == swap3).
 262
 263 definition Rswap_l ≝
 264   λalpha,t1,t2.
 265    ∀a,b,ls,rs.
 266     t1 = midtape alpha (a::ls) b rs →
 267     t2 = midtape alpha (b::ls) a rs.
 268
 269 lemma sem_swap_l : ∀alpha,foo.
 270   swap_l alpha foo ⊨ Rswap_l alpha.
 271 #alpha #foo *
 272   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
 273    % [% |#a #b #ls #rs #H destruct]
 274   |#l0 #lt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (leftof ? l0 lt0)))
 275    % [% |#a #b #ls #rs #H destruct]
 276   |#r0 #rt0 @(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (rightof ? r0 rt0)))
 277    % [% |#a #b #ls #rs #H destruct]
 278   | #lt #c #rt @(ex_intro ?? 4) cases lt
 279     [@ex_intro [|% [ % | #a #b #ls #rs #H destruct]]
 280     |#l0 #lt0 @ex_intro [| % [ % | #a #b #ls #rs #H destruct //
 281     ]
 282   ]
 283 qed.