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 mcl0 : initN 5 ≝ mk_Sig ?? 0 (leb_true_to_le 1 5 (refl …)).
  39 definition mcl1 : initN 5 ≝ mk_Sig ?? 1 (leb_true_to_le 2 5 (refl …)).
  40 definition mcl2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)).
  41 definition mcl3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)).
  42 definition mcl4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)).
  43
  44 definition mcl_step ≝
  45  λalpha:FinSet.λsep:alpha.
  46  mk_TM alpha (mcl_states alpha)
  47  (λp.let 〈q,a〉 ≝ p in
  48   let 〈q',b〉 ≝ q in
  49   let q' ≝ pi1 nat (λi.i<5) q' in (* perche' devo passare il predicato ??? *)
  50   match a with
  51   [ None ⇒ 〈〈mcl4,sep〉,None ?〉
  52   | Some a' ⇒
  53   match q' with
  54   [ O ⇒ (* qinit *)
  55     match a' == sep with
  56     [ true ⇒ 〈〈mcl4,sep〉,None ?〉
  57     | false ⇒ 〈〈mcl1,a'〉,Some ? 〈a',R〉〉 ]
  58   | S q' ⇒ match q' with
  59     [ O ⇒ (* q1 *)
  60       〈〈mcl2,a'〉,Some ? 〈b,L〉〉
  61     | S q' ⇒ match q' with
  62       [ O ⇒ (* q2 *)
  63         〈〈mcl3,sep〉,Some ? 〈b,L〉〉
  64       | S q' ⇒ match q' with
  65         [ O ⇒ (* qacc *)
  66           〈〈mcl3,sep〉,None ?〉
  67         | S q' ⇒ (* qfail *)
  68           〈〈mcl4,sep〉,None ?〉 ] ] ] ] ])
  69   〈mcl0,sep〉
  70   (λq.let 〈q',a〉 ≝ q in q' == mcl3 ∨ q' == mcl4).
  71
  72 lemma mcl_q0_q1 :
  73   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
  74   a0 == sep = false →
  75   step alpha (mcl_step alpha sep)
  76     (mk_config ?? 〈mcl0,a〉 (mk_tape … ls (Some ? a0) rs)) =
  77   mk_config alpha (states ? (mcl_step alpha sep)) 〈mcl1,a0〉
  78     (tape_move_right alpha ls a0 rs).
  79 #alpha #sep #a *
  80 [ #a0 #rs #Ha0 whd in ⊢ (??%?);
  81   normalize in match (trans ???); >Ha0 %
  82 | #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
  83   normalize in match (trans ???); >Ha0 %
  84 ]
  85 qed.
  86
  87 lemma mcl_q1_q2 :
  88   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
  89   step alpha (mcl_step alpha sep)
  90     (mk_config ?? 〈mcl1,a〉 (mk_tape … ls (Some ? a0) rs)) =
  91   mk_config alpha (states ? (mcl_step alpha sep)) 〈mcl2,a0〉
  92     (tape_move_left alpha ls a rs).
  93 #alpha #sep #a #ls #a0 * //
  94 qed.
  95
  96 lemma mcl_q2_q3 :
  97   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
  98   step alpha (mcl_step alpha sep)
  99     (mk_config ?? 〈mcl2,a〉 (mk_tape … ls (Some ? a0) rs)) =
 100   mk_config alpha (states ? (mcl_step alpha sep)) 〈mcl3,sep〉
 101     (tape_move_left alpha ls a rs).
 102 #alpha #sep #a #ls #a0 * //
 103 qed.
 104
 105 definition Rmcl_step_true ≝
 106   λalpha,sep,t1,t2.
 107    ∀a,b,ls,rs.
 108     t1 = midtape alpha ls b (a::rs) →
 109     b ≠ sep ∧
 110     t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
 111
 112 definition Rmcl_step_false ≝
 113   λalpha,sep,t1,t2.
 114     right ? t1 ≠ [] →  current alpha t1 ≠ None alpha →
 115       current alpha t1 = Some alpha sep ∧ t2 = t1.
 116
 117 lemma mcl_trans_init_sep:
 118   ∀alpha,sep,x.
 119   trans ? (mcl_step alpha sep) 〈〈mcl0,x〉,Some ? sep〉 = 〈〈mcl4,sep〉,None ?〉.
 120 #alpha #sep #x normalize >(\b ?) //
 121 qed.
 122
 123 lemma mcl_trans_init_not_sep:
 124   ∀alpha,sep,x,y.y == sep = false →
 125   trans ? (mcl_step alpha sep) 〈〈mcl0,x〉,Some ? y〉 = 〈〈mcl1,y〉,Some ? 〈y,R〉〉.
 126 #alpha #sep #x #y #H1 normalize >H1 //
 127 qed.
 128
 129 lemma sem_mcl_step :
 130   ∀alpha,sep.
 131   accRealize alpha (mcl_step alpha sep)
 132     〈mcl3,sep〉 (Rmcl_step_true alpha sep) (Rmcl_step_false alpha sep).
 133 #alpha #sep cut (∀P:Prop.〈mcl4,sep〉=〈mcl3,sep〉→P)
 134   [#P whd in ⊢ ((??(???%?)(???%?))→?); #Hfalse destruct] #Hfalse
 135 *
 136 [@(ex_intro ?? 2)
 137   @(ex_intro … (mk_config ?? 〈mcl4,sep〉 (niltape ?)))
 138   % [% [whd in ⊢ (??%?);% |@Hfalse] |#H1 #H2 @False_ind @(absurd ?? H2) %]
 139 |#l0 #lt0 @(ex_intro ?? 2)
 140   @(ex_intro … (mk_config ?? 〈mcl4,sep〉 (leftof ? l0 lt0)))
 141   % [% [whd in ⊢ (??%?);% |@Hfalse] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 142 |#r0 #rt0 @(ex_intro ?? 2)
 143   @(ex_intro … (mk_config ?? 〈mcl4,sep〉 (rightof ? r0 rt0)))
 144   % [% [whd in ⊢ (??%?);% |@Hfalse] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 145 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
 146   [ @(ex_intro ?? 2)
 147     @(ex_intro ?? (mk_config ?? 〈mcl4,sep〉 (midtape ? lt c rt)))
 148     % [ %
 149         [ >(\P Hc) >loop_S_false // >loop_S_true
 150           [ @eq_f whd in ⊢ (??%?); >mcl_trans_init_sep %
 151           |>(\P Hc) whd in ⊢(??(???(???%))?); >mcl_trans_init_sep % ]
 152         |@Hfalse]
 153       |#_ #H1 #H2 % // normalize >(\P Hc) % ]
 154   |@(ex_intro ?? 4) cases rt
 155     [ @ex_intro
 156       [|% [ %
 157             [ >loop_S_false // >mcl_q0_q1 //
 158             | normalize in ⊢ (%→?); @Hfalse]
 159           | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
 160    | #r0 #rt0 @ex_intro
 161       [| % [ %
 162              [ >loop_S_false // >mcl_q0_q1 //
 163              | #_ #a #b #ls #rs #Hb destruct (Hb) %
 164                [ @(\Pf Hc)
 165                | >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ]
 166            | normalize in ⊢ (% → ?); * #Hfalse
 167              @False_ind /2/ ]
 168      ]
 169    ]
 170  ]
 171 ]
 172 qed.
 173
 174 (* the move_char (variant c) machine *)
 175 definition move_char_l ≝
 176   λalpha,sep.whileTM alpha (mcl_step alpha sep) 〈mcl3,sep〉.
 177
 178 definition R_move_char_l ≝
 179   λalpha,sep,t1,t2.
 180     ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) →
 181     (b = sep → t2 = t1) ∧
 182     (∀ls1,ls2.ls = ls1@sep::ls2 →
 183      b ≠ sep → memb ? sep ls1 = false →
 184      t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
 185
 186 lemma sem_move_char_l :
 187   ∀alpha,sep.
 188   WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
 189 #alpha #sep #inc #i #outc #Hloop
 190 lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
 191 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 192 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
 193   %
 194   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
 195    [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ]
 196   | #rs1 #rs2 #Hrs #Hb #Hrs1
 197     >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??)
 198     [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct %
 199     |*:% normalize #H2 destruct (H2) ]
 200   ]
 201 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 202   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 203   #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
 204   #Ha0 #Htapeb %
 205   [ #Hfalse @False_ind @(absurd ?? Ha0) //
 206   | *
 207     [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_
 208       >Hls in Htapeb; #Htapeb normalize in Htapeb;
 209       cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
 210     | #l0 #ls0 #ls2 #Hls #_ #Hls0
 211       cut (l0 ≠ sep ∧ memb … sep ls0 = false)
 212       [ %
 213          [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
 214          | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
 215            [ destruct
 216            | @Hfalse ]
 217          ]
 218       ] *
 219       #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
 220       normalize in ⊢ (%→?); #Htapeb
 221       cases (IH … Htapeb) -IH #_ #IH
 222       >reverse_cons >associative_append @IH //
 223     ]
 224   ]
 225 qed.
 226
 227 lemma terminate_move_char_l :
 228   ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) →
 229   (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
 230 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
 231 @(terminate_while … (sem_mcl_step alpha sep))
 232   [%
 233   |generalize in match Hsep; -Hsep
 234    generalize in match Ht; -Ht
 235    generalize in match rs; -rs
 236    generalize in match a; -a
 237    generalize in match b; -b
 238    generalize in match t; -t
 239    elim ls
 240     [#t #b #a #rs #Ht #Hsep % #tinit
 241      whd in ⊢ (%→?); #H @False_ind
 242      cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
 243      cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
 244     |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
 245      whd in ⊢ (%→?); #H
 246      cases (H … Ht) #Hbsep #Htinit
 247      @(Hind … Htinit) cases Hsep
 248       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
 249         [#eqsep %1 >(\P eqsep) // | #H %2 //]
 250   ]
 251 qed.