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