matita/matita/lib/turing/auxiliary_machines.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 include "turing/basic_machines.ma".
  13 include "turing/if_machine.ma".
  14
  15 (* while {
  16      if current != null
  17         then move_r
  18         else nop
  19      }
  20  *)
  21
  22 definition mte_step ≝ λalpha,D.
  23 ifTM ? (test_null alpha) (single_finalTM ? (move alpha D)) (nop ?) tc_true.
  24
  25 definition R_mte_step_true ≝ λalpha,D,t1,t2.
  26   ∃ls,c,rs.
  27     t1 = midtape alpha ls c rs ∧ t2 = tape_move ? t1 D.
  28
  29 definition R_mte_step_false ≝ λalpha.λt1,t2:tape alpha.
  30   current ? t1 = None ? ∧ t1 = t2.
  31
  32 definition mte_acc : ∀alpha,D.states ? (mte_step alpha D) ≝
  33 λalpha,D.(inr … (inl … (inr … start_nop))).
  34
  35 lemma sem_mte_step :
  36   ∀alpha,D.mte_step alpha D ⊨
  37    [ mte_acc … : R_mte_step_true alpha D, R_mte_step_false alpha ] .
  38 #alpha #D #ta
  39 @(acc_sem_if_app ??????????? (sem_test_null …)
  40   (sem_move_single …) (sem_nop alpha) ??)
  41 [ #tb #tc #td * #Hcurtb
  42   lapply (refl ? (current ? tb)) cases (current ? tb) in ⊢ (???%→?);
  43   [ #H @False_ind >H in Hcurtb; * /2/ ]
  44   -Hcurtb #c #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd
  45   cases (current_to_midtape … Hcurtb) #ls * #rs #Hmidtb
  46   %{ls} %{c} %{rs} % //
  47 | #tb #tc #td * #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd % // ]
  48 qed.
  49
  50 definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) (mte_acc …).
  51
  52 definition R_move_to_end_r ≝
  53   λsig,int,outt.
  54   (current ? int = None ? → outt = int) ∧
  55   ∀ls,c,rs.int = midtape sig ls c rs → outt = mk_tape ? (reverse ? rs@c::ls) (None ?) [ ].
  56
  57 lemma wsem_move_to_end_r : ∀sig. move_to_end sig R ⊫ R_move_to_end_r sig.
  58 #sig #ta #k #outc #Hloop
  59 lapply (sem_while … (sem_mte_step sig R) … Hloop) //
  60 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
  61 [ * #Hcurtb #Houtc % /2/ #ls #c #rs #Htb >Htb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
  62 | #tc #td * #ls * #c * #rs * #Htc >Htc cases rs
  63   [ normalize in ⊢ (%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
  64     lapply (IH Hfalse) -IH * #Htd1 #_ %
  65     [ normalize in ⊢ (%→?); #H destruct (H)
  66     | #ls0 #c0 #rs0 #H destruct (H) >Htd1 // ]
  67   | #r0 #rs0 whd in ⊢ (???%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
  68     lapply (IH Hfalse) -IH * #_ #IH %
  69     [ normalize in ⊢ (%→?); #H destruct (H)
  70     | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ]
  71 qed.
  72
  73 lemma terminate_move_to_end_r :  ∀sig,t.move_to_end sig R ↓ t.
  74 #sig #t @(terminate_while … (sem_mte_step sig R …)) //
  75 cases t
  76 [ % #t1 * #ls * #c * #rs * #H destruct
  77 |2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct
  78 | #ls #c #rs lapply c -c lapply ls -ls elim rs
  79   [ #ls #c % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct %
  80     #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct
  81   | #r0 #rs0 #IH #ls #c % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH
  82   ]
  83 ]
  84 qed.
  85
  86 lemma sem_move_to_end_r : ∀sig. move_to_end sig R ⊨ R_move_to_end_r sig.
  87 #sig @WRealize_to_Realize //
  88 qed.
  89
  90 definition R_move_to_end_l ≝
  91   λsig,int,outt.
  92   (current ? int = None ? → outt = int) ∧
  93   ∀ls,c,rs.int = midtape sig ls c rs → outt = mk_tape ? [ ] (None ?) (reverse ? ls@c::rs).
  94
  95 lemma wsem_move_to_end_l : ∀sig. move_to_end sig L ⊫ R_move_to_end_l sig.
  96 #sig #ta #k #outc #Hloop
  97 lapply (sem_while … (sem_mte_step sig L) … Hloop) //
  98 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
  99 [ * #Hcurtb #Houtc % /2/ #ls #c #rs #Htb >Htb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
 100 | #tc #td * #ls * #c * #rs * #Htc >Htc cases ls
 101   [ normalize in ⊢ (%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
 102     lapply (IH Hfalse) -IH * #Htd1 #_ %
 103     [ normalize in ⊢ (%→?); #H destruct (H)
 104     | #ls0 #c0 #rs0 #H destruct (H) >Htd1 // ]
 105   | #l0 #ls0 whd in ⊢ (???%→?); #Htd >Htd #Hstar #IH whd in ⊢ (%→?); #Hfalse
 106     lapply (IH Hfalse) -IH * #_ #IH %
 107     [ normalize in ⊢ (%→?); #H destruct (H)
 108     | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ]
 109 qed.
 110
 111 lemma terminate_move_to_end_l :  ∀sig,t.move_to_end sig L ↓ t.
 112 #sig #t @(terminate_while … (sem_mte_step sig L …)) //
 113 cases t
 114 [ % #t1 * #ls * #c * #rs * #H destruct
 115 |2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct
 116 | #ls elim ls
 117   [ #c #rs % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct %
 118     #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct
 119   | #l0 #ls0 #IH #c #rs % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH
 120   ]
 121 ]
 122 qed.
 123
 124 lemma sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
 125 #sig @WRealize_to_Realize //
 126 qed.
 127