matita/matita/lib/turing/universal/move_char_c.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 (variant c) 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 x cs # rs
  21        ^
  22        H
  23
  24 Output:
  25   ls cs x # rs
  26         ^
  27         H
  28
  29 Initial state = 〈0,#〉
  30 Final state = 〈4,#〉
  31
  32 *)
  33
  34 include "turing/basic_machines.ma".
  35 include "turing/if_machine.ma".
  36
  37 definition mcc_step ≝ λalpha:FinSet.λsep:alpha.
  38   ifTM alpha (test_char ? (λc.¬c==sep))
  39      (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true.
  40
  41 definition Rmcc_step_true ≝
  42   λalpha,sep,t1,t2.
  43    ∀a,b,ls,rs.
  44     t1 = midtape alpha (a::ls) b rs →
  45     b ≠ sep ∧
  46     t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
  47
  48 definition Rmcc_step_false ≝
  49   λalpha,sep,t1,t2.
  50     left ? t1 ≠ [] →  current alpha t1 ≠ None alpha →
  51       current alpha t1 = Some alpha sep ∧ t2 = t1.
  52
  53 lemma sem_mcc_step :
  54   ∀alpha,sep.
  55   mcc_step alpha sep ⊨
  56     [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep].
  57 #alpha #sep
  58   @(acc_sem_if_app …
  59      (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …))
  60   [#intape #outtape #tapea whd in ⊢ (%→%→%);
  61    #Htapea * #tapeb * whd in ⊢ (%→%→?);
  62    #Htapeb #Houttape #a #b #ls #rs #Hintape
  63    >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
  64    #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
  65    @Houttape @Htapeb //
  66   |#intape #outtape #tapea whd in ⊢ (%→%→%);
  67    cases (current alpha intape)
  68     [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
  69     |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
  70      lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
  71     ]
  72   ]
  73 qed.
  74
  75 (* the move_char (variant c) machine *)
  76 definition move_char_c ≝
  77   λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))).
  78
  79 definition R_move_char_c ≝
  80   λalpha,sep,t1,t2.
  81     ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
  82     (b = sep → t2 = t1) ∧
  83     (∀rs1,rs2.rs = rs1@sep::rs2 →
  84      b ≠ sep → memb ? sep rs1 = false →
  85      t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
  86
  87 lemma sem_move_char_c :
  88   ∀alpha,sep.
  89   WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
  90 #alpha #sep #inc #i #outc #Hloop
  91 lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
  92 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
  93 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
  94   %
  95   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
  96     [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
  97   | #rs1 #rs2 #Hrs #Hb #Hrs1
  98     >Htapea in H1; #H1 cases (H1 ??)
  99     [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
 100     |*:% #H2 normalize in H2; destruct (H2) ]
 101   ]
 102 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 103   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 104   #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
 105   #Ha0 #Htapeb %
 106   [ #Hfalse @False_ind @(absurd ?? Ha0) //
 107   | *
 108     [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
 109       >Hrs in Htapeb; #Htapeb normalize in Htapeb;
 110       cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
 111     | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
 112       cut (r0 ≠ sep ∧ memb … sep rs0 = false)
 113       [ %
 114          [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
 115          | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
 116            [ destruct
 117            | @Hfalse ]
 118          ]
 119       ] *
 120       #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
 121       normalize in ⊢ (%→?); #Htapeb
 122       cases (IH … Htapeb) -IH #_ #IH
 123       >reverse_cons >associative_append @IH //
 124     ]
 125   ]
 126 qed.
 127
 128 lemma terminate_move_char_c :
 129   ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
 130   (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_c alpha sep) t.
 131 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
 132 @(terminate_while … (sem_mcc_step alpha sep))
 133   [%
 134   |generalize in match Hsep; -Hsep
 135    generalize in match Ht; -Ht
 136    generalize in match ls; -ls
 137    generalize in match a; -a
 138    generalize in match b; -b
 139    generalize in match t; -t
 140    elim rs
 141     [#t #b #a #ls #Ht #Hsep % #tinit
 142      whd in ⊢ (%→?); #H @False_ind
 143      cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
 144      cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
 145     |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
 146      whd in ⊢ (%→?); #H
 147      cases (H … Ht) #Hbsep #Htinit
 148      @(Hind … Htinit) cases Hsep
 149       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
 150         [#eqsep %1 >(\P eqsep) // | #H %2 //]
 151   ]
 152 qed.
 153
 154 (* NO GOOD: we must stop if current = None too!!! *)
 155
 156 axiom ssem_move_char_c :
 157   ∀alpha,sep.
 158   Realize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).