matita/matita/lib/turing/universal/move_char_l.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
  13 (* MOVE_CHAR (left) MACHINE
  14
  15 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
  16
  17 Input:
  18 (ls,cs,rs can be empty; # is a parameter)
  19
  20   ls # cs x rs
  21         ^
  22         H
  23
  24 Output:
  25   ls # x cs rs
  26        ^
  27        H
  28
  29 Initial state = 〈0,#〉
  30 Final state = 〈4,#〉
  31
  32 *)
  33
  34 include "turing/while_machine.ma".
  35
  36 definition mcl_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
  37
  38 definition mcl_step ≝
  39  λalpha:FinSet.λsep:alpha.
  40  mk_TM alpha (mcl_states alpha)
  41  (λp.let 〈q,a〉 ≝ p in
  42   let 〈q',b〉 ≝ q in
  43   match a with
  44   [ None ⇒ 〈〈4,sep〉,None ?〉
  45   | Some a' ⇒
  46   match q' with
  47   [ O ⇒ (* qinit *)
  48     match a' == sep with
  49     [ true ⇒ 〈〈4,sep〉,None ?〉
  50     | false ⇒ 〈〈1,a'〉,Some ? 〈a',R〉〉 ]
  51   | S q' ⇒ match q' with
  52     [ O ⇒ (* q1 *)
  53       〈〈2,a'〉,Some ? 〈b,L〉〉
  54     | S q' ⇒ match q' with
  55       [ O ⇒ (* q2 *)
  56         〈〈3,sep〉,Some ? 〈b,L〉〉
  57       | S q' ⇒ match q' with
  58         [ O ⇒ (* qacc *)
  59           〈〈3,sep〉,None ?〉
  60         | S q' ⇒ (* qfail *)
  61           〈〈4,sep〉,None ?〉 ] ] ] ] ])
  62   〈0,sep〉
  63   (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
  64
  65 lemma mcc_q0_q1 :
  66   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
  67   a0 == sep = false →
  68   step alpha (mcl_step alpha sep)
  69     (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
  70   mk_config alpha (states ? (mcl_step alpha sep)) 〈1,a0〉
  71     (tape_move_right alpha ls a0 rs).
  72 #alpha #sep #a *
  73 [ #a0 #rs #Ha0 whd in ⊢ (??%?);
  74   normalize in match (trans ???); >Ha0 %
  75 | #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
  76   normalize in match (trans ???); >Ha0 %
  77 ]
  78 qed.
  79
  80 lemma mcl_q1_q2 :
  81   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
  82   step alpha (mcl_step alpha sep)
  83     (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) =
  84   mk_config alpha (states ? (mcl_step alpha sep)) 〈2,a0〉
  85     (tape_move_left alpha ls a rs).
  86 #alpha #sep #a #ls #a0 * //
  87 qed.
  88
  89 lemma mcc_q2_q3 :
  90   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
  91   step alpha (mcl_step alpha sep)
  92     (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) =
  93   mk_config alpha (states ? (mcl_step alpha sep)) 〈3,sep〉
  94     (tape_move_left alpha ls a rs).
  95 #alpha #sep #a #ls #a0 * //
  96 qed.
  97
  98 definition Rmcl_step_true ≝
  99   λalpha,sep,t1,t2.
 100    ∀a,b,ls,rs.
 101     t1 = midtape alpha ls b (a::rs) →
 102     b ≠ sep ∧
 103     t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
 104
 105 definition Rmcl_step_false ≝
 106   λalpha,sep,t1,t2.
 107     right ? t1 ≠ [] →  current alpha t1 ≠ None alpha →
 108       current alpha t1 = Some alpha sep ∧ t2 = t1.
 109
 110 lemma mcl_trans_init_sep:
 111   ∀alpha,sep,x.
 112   trans ? (mcl_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
 113 #alpha #sep #x normalize >(\b ?) //
 114 qed.
 115
 116 lemma mcl_trans_init_not_sep:
 117   ∀alpha,sep,x,y.y == sep = false →
 118   trans ? (mcl_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,R〉〉.
 119 #alpha #sep #x #y #H1 normalize >H1 //
 120 qed.
 121
 122 (*
 123 STOP
 124
 125 lemma sem_mcl_step :
 126   ∀alpha,sep.
 127   accRealize alpha (mcl_step alpha sep)
 128     〈3,sep〉 (Rmcl_step_true alpha sep) (Rmcl_step_false alpha sep).
 129 #alpha #sep *
 130 [@(ex_intro ?? 2)
 131   @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?)))
 132   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
 133 |#l0 #lt0 @(ex_intro ?? 2)
 134   @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? l0 lt0)))
 135   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
 136 |#r0 #rt0 @(ex_intro ?? 2)
 137   @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? r0 rt0)))
 138   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 139 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
 140   [ @(ex_intro ?? 2)
 141     @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
 142     % [ %
 143         [ >(\P Hc) >loop_S_false // >loop_S_true
 144          [ @eq_f whd in ⊢ (??%?); >trans_init_sep %
 145          |>(\P Hc) whd in ⊢(??(???(???%))?); >trans_init_sep % ]
 146         |   #Hfalse destruct ]
 147       |#_ #H1 #H2 % // normalize >(\P Hc) % ]
 148   | @(ex_intro ?? 4) cases lt
 149     [ @ex_intro
 150       [|% [ %
 151             [ >loop_S_false // >mcc_q0_q1 //
 152             | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
 153           | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
 154     | #l0 #lt @ex_intro
 155       [| % [ %
 156              [ >loop_S_false // >mcc_q0_q1 //
 157              | #_ #a #b #ls #rs #Hb destruct %
 158                [ @(\Pf Hc)
 159                | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ]
 160            | normalize in ⊢ (% → ?); * #Hfalse
 161              @False_ind /2/ ]
 162      ]
 163    ]
 164  ]
 165 ]
 166 qed.
 167
 168 (* the move_char (variant c) machine *)
 169 definition move_char_c ≝
 170   λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉.
 171
 172 definition R_move_char_c ≝
 173   λalpha,sep,t1,t2.
 174     ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
 175     (b = sep → t2 = t1) ∧
 176     (∀rs1,rs2.rs = rs1@sep::rs2 →
 177      b ≠ sep → memb ? sep rs1 = false →
 178      t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
 179
 180 lemma sem_while_move_char :
 181   ∀alpha,sep.
 182   WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
 183 #alpha #sep #inc #i #outc #Hloop
 184 lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
 185 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 186 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
 187   %
 188   [ #Hb >Htapea in H1; >Hb normalize in ⊢ (%→?); #H1
 189    cases (H1 ??)
 190    [#_ #H2 >H2 %
 191    |*: % #H2 destruct (H2) ]
 192   | #rs1 #rs2 #Hrs #Hb #Hrs1
 193     >Htapea in H1; normalize in ⊢ (% → ?); #H1
 194     cases (H1 ??)
 195     [ #Hfalse @False_ind @(absurd ?? Hb) destruct %
 196     |*:% #H2 destruct (H2) ]
 197   ]
 198 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 199   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 200   #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
 201   #Ha0 #Htapeb %
 202   [ #Hfalse @False_ind @(absurd ?? Ha0) //
 203   | *
 204     [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize
 205       >Hrs in Htapeb; normalize #Htapeb
 206       cases (IH … Htapeb)
 207       #Houtc #_ >Houtc //
 208     | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
 209       cut (r0 ≠ sep ∧ memb … sep rs0 = false)
 210       [ %
 211          [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
 212          | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
 213            [ destruct
 214            | @Hfalse ]
 215          ]
 216       ] *
 217       #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
 218       normalize in ⊢ (%→?); #Htapeb
 219       cases (IH … Htapeb) -IH #_ #IH
 220       >reverse_cons >associative_append @IH //
 221     ]
 222   ]
 223 qed.
 224 *)