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_step ≝ λalpha:FinSet.λsep:alpha.
  39   ifTM alpha (test_char ? (λc.¬c==sep))
  40      (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true.
  41
  42 definition Rmcl_step_true ≝
  43   λalpha,sep,t1,t2.
  44    ∀a,b,ls,rs.
  45     t1 = midtape alpha ls b (a::rs) →
  46     b ≠ sep ∧
  47     t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
  48
  49 definition Rmcl_step_false ≝
  50   λalpha,sep,t1,t2.
  51     right ? t1 ≠ [] →  current alpha t1 ≠ None alpha →
  52       current alpha t1 = Some alpha sep ∧ t2 = t1.
  53
  54 lemma sem_mcl_step :
  55   ∀alpha,sep.
  56   mcl_step alpha sep ⊨
  57     [inr … (inl … (inr … start_nop)): Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
  58 #alpha #sep
  59   @(acc_sem_if_app …
  60      (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …))
  61   [#intape #outtape #tapea whd in ⊢ (%→%→%);
  62    #Htapea * #tapeb * whd in ⊢ (%→%→?);
  63    #Htapeb #Houttape #a #b #ls #rs #Hintape
  64    >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
  65    #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
  66    @Houttape @Htapeb //
  67   |#intape #outtape #tapea whd in ⊢ (%→%→%);
  68    cases (current alpha intape)
  69     [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
  70     |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
  71      lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
  72     ]
  73   ]
  74 qed.
  75
  76 (* the move_char (variant c) machine *)
  77 definition move_char_l ≝
  78   λalpha,sep.whileTM alpha (mcl_step alpha sep) 〈mcl3,sep〉.
  79
  80 definition R_move_char_l ≝
  81   λalpha,sep,t1,t2.
  82     ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) →
  83     (b = sep → t2 = t1) ∧
  84     (∀ls1,ls2.ls = ls1@sep::ls2 →
  85      b ≠ sep → memb ? sep ls1 = false →
  86      t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
  87
  88 lemma sem_move_char_l :
  89   ∀alpha,sep.
  90   WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
  91 #alpha #sep #inc #i #outc #Hloop
  92 lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
  93 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
  94 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
  95   %
  96   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
  97    [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ]
  98   | #rs1 #rs2 #Hrs #Hb #Hrs1
  99     >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??)
 100     [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct %
 101     |*:% normalize #H2 destruct (H2) ]
 102   ]
 103 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 104   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 105   #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
 106   #Ha0 #Htapeb %
 107   [ #Hfalse @False_ind @(absurd ?? Ha0) //
 108   | *
 109     [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_
 110       >Hls in Htapeb; #Htapeb normalize in Htapeb;
 111       cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
 112     | #l0 #ls0 #ls2 #Hls #_ #Hls0
 113       cut (l0 ≠ sep ∧ memb … sep ls0 = false)
 114       [ %
 115          [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
 116          | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
 117            [ destruct
 118            | @Hfalse ]
 119          ]
 120       ] *
 121       #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
 122       normalize in ⊢ (%→?); #Htapeb
 123       cases (IH … Htapeb) -IH #_ #IH
 124       >reverse_cons >associative_append @IH //
 125     ]
 126   ]
 127 qed.
 128
 129 lemma terminate_move_char_l :
 130   ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) →
 131   (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
 132 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
 133 @(terminate_while … (sem_mcl_step alpha sep))
 134   [%
 135   |generalize in match Hsep; -Hsep
 136    generalize in match Ht; -Ht
 137    generalize in match rs; -rs
 138    generalize in match a; -a
 139    generalize in match b; -b
 140    generalize in match t; -t
 141    elim ls
 142     [#t #b #a #rs #Ht #Hsep % #tinit
 143      whd in ⊢ (%→?); #H @False_ind
 144      cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
 145      cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
 146     |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
 147      whd in ⊢ (%→?); #H
 148      cases (H … Ht) #Hbsep #Htinit
 149      @(Hind … Htinit) cases Hsep
 150       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
 151         [#eqsep %1 >(\P eqsep) // | #H %2 //]
 152   ]
 153 qed.