matita/matita/lib/turing/multi_universal/copy.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "turing/turing.ma".
  16 include "turing/inject.ma".
  17
  18 definition copy_states ≝ initN 3.
  19
  20 definition copy0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  21 definition copy1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  22 definition copy2 : copy_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  23
  24 (*
  25
  26 src: a b c ... z # ---→ a b c ... z #
  27      ^                              ^
  28
  29 dst: _ _ _ ... _ d ---→ a b c ... z d
  30      ^                              ^
  31
  32 0) (x ≠ sep,_) → (x,x)(R,R) → 1
  33    (sep,d) → None 2
  34 1) (_,_) → None 1
  35 2) (_,_) → None 2
  36
  37 *)
  38
  39 definition trans_copy_step ≝
  40  λsrc,dst,sig,n,is_sep.
  41  λp:copy_states × (Vector (option sig) (S n)).
  42  let 〈q,a〉 ≝ p in
  43  match pi1 … q with
  44  [ O ⇒ match nth src ? a (None ?) with
  45    [ None ⇒ 〈copy2,null_action ? n〉
  46    | Some a0 ⇒ if is_sep a0 then 〈copy2,null_action ? n〉
  47                   else 〈copy1,change_vec ? (S n)
  48                           (change_vec ?(S n)
  49                            (null_action ? n) (Some ? 〈a0,R〉) src)
  50                           (Some ? 〈a0,R〉) dst〉 ]
  51  | S q ⇒ match q with
  52    [ O ⇒ (* 1 *) 〈copy1,null_action ? n〉
  53    | S _ ⇒ (* 2 *) 〈copy2,null_action ? n〉 ] ].
  54
  55 definition copy_step ≝
  56   λsrc,dst,sig,n,is_sep.
  57   mk_mTM sig n copy_states (trans_copy_step src dst sig n is_sep)
  58     copy0 (λq.q == copy1 ∨ q == copy2).
  59
  60 definition R_copy_step ≝
  61   λsrc,dst,sig,n,is_sep.λint,outt: Vector (tape sig) (S n).
  62   (∀x1,x2,xls,xrs.
  63    nth src ? int (niltape ?) = midtape sig xls x1 (x2::xrs) →
  64    (is_sep x1 = true ∧ outt = int) ∨
  65    (is_sep x1 = false ∧
  66     outt = change_vec ??
  67             (change_vec ?? int (midtape sig (x1::xls) x2 xrs) src)
  68             (tape_move ? (nth dst ? int (niltape ?)) (Some ? 〈x1,R〉)) dst)) ∧
  69   (current ? (nth src ? int (niltape ?)) = None ? →
  70    outt = int).
  71
  72 lemma copy_q0_q2_null :
  73   ∀src,dst,sig,n,is_sep,v,t.src < S n → dst < S n →
  74   current ? t = None ? →
  75   step sig n (copy_step src dst sig n is_sep)
  76     (mk_mconfig ??? copy0 (change_vec ? (S n) v t src)) =
  77     mk_mconfig ??? copy2 (change_vec ? (S n) v t src).
  78 #src #dst #sig #n #is_sep #v #t #Hsrc #Hdst #Hcurrent
  79 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
  80 [ >current_chars_change_vec // whd in match (trans ????);
  81   >nth_change_vec // >Hcurrent %
  82 | >current_chars_change_vec // whd in match (trans ????);
  83   >nth_change_vec // >Hcurrent @tape_move_null_action
  84 ]
  85 qed.
  86
  87 lemma copy_q0_q2_sep :
  88   ∀src,dst,sig,n,is_sep,v,t.src < S n → dst < S n →
  89   ∀s.current ? t = Some ? s → is_sep s = true →
  90   step sig n (copy_step src dst sig n is_sep)
  91     (mk_mconfig ??? copy0 (change_vec ? (S n) v t src)) =
  92     mk_mconfig ??? copy2 (change_vec ? (S n) v t src).
  93 #src #dst #sig #n #is_sep #v #t #Hsrc #Hdst #s #Hcurrent #Hsep
  94 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
  95 [ >current_chars_change_vec // whd in match (trans ????);
  96   >nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
  97 | >current_chars_change_vec // whd in match (trans ????);
  98   >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?);
  99   >Hsep @tape_move_null_action
 100 ]
 101 qed.
 102
 103 lemma copy_q0_q1 :
 104   ∀src,dst,sig,n,is_sep,v,t.src < S n → dst < S n →
 105   ∀s.current ? t = Some ? s → is_sep s = false →
 106   step sig n (copy_step src dst sig n is_sep)
 107     (mk_mconfig ??? copy0 (change_vec ? (S n) v t src)) =
 108     mk_mconfig ??? copy1
 109      (change_vec ? (S n)
 110        (change_vec ?? v
 111          (tape_move ? (nth src ? v (niltape ?)) (Some ? 〈s,R〉)) src)
 112        (tape_move ? (nth dst ? v (niltape ?)) (Some ? 〈s,R〉)) dst).
 113 #src #dst #sig #n #is_sep #v #t #Hsrc #Hdst #s #Hcurrent #Hsep
 114 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
 115 [ >current_chars_change_vec // whd in match (trans ????);
 116   >nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
 117 | >current_chars_change_vec // whd in match (trans ????);
 118   >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?);
 119   >Hsep whd in ⊢ (??(???????(???%))?); >pmap_change
 120   (* le due change commutano *)
 121 ]
 122
 123 lemma sem_copy_step :
 124   ∀src,dst,sig,n,is_sep.src < S n → dst < S n →
 125   copy_step src dst sig n is_sep ⊨ R_copy_step src dst sig n is_sep.
 126 #src #dst #sig #n #is_sep #Hsrc #Hdst #int
 127 <(change_vec_same ?? int src (niltape ?)) cases (nth src ? int (niltape ?))
 128 [ %{2} % [| %
 129   [ whd in ⊢ (??%?); >copy_q0_q2 //
 130   | % // #x1 #x2 #xls #xrs >nth_change_vec // #Hfalse destruct ] ]
 131 | #a #al %{2} % [| %
 132   [ whd in ⊢ (??%?); >copy_q0_q2 //
 133   | % // #x1 #x2 #xls #xrs >nth_change_vec // #Hfalse destruct ] ]
 134 | #a #al %{2} % [| %
 135   [ whd in ⊢ (??%?); >copy_q0_q2 //
 136   | % // #x1 #x2 #xls #xrs >nth_change_vec // #Hfalse destruct ] ]
 137 | #ls #c #rs %{2} % [| %
 138   [