matita/matita/lib/turing/simple_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/multi_universal/match.ma".
  13
  14 (********************** look_ahead test *************************)
  15
  16 definition mtestR ≝ λsig,i,n,test.
  17   (mmove i sig n R) ·
  18     (ifTM ?? (inject_TM ? (test_char ? test) n i)
  19     (single_finalTM ?? (mmove i sig n L))
  20     (mmove i sig n L) tc_true).
  21
  22
  23 (* underspecified *)
  24 definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
  25   ∀ls,c,c1,rs.
  26     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
  27     t1 = t2 ∧ (test c1 = true).
  28
  29 definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
  30   ∀ls,c,c1,rs.
  31     nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
  32     t1 = t2 ∧ (test c1 = false).
  33
  34 definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
  35 #sig #i #n #test @inr @inr @inl @inr @start_nop
  36 qed.
  37
  38 lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
  39   mtestR sig i n test ⊨
  40     [mtestR_acc sig i n test:
  41        RmtestR_true sig  i (S n) test, RmtestR_false sig i (S n) test].
  42 #sig #i #n #test #Hlein
  43 @(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
  44    (acc_sem_if sig n ????????
  45      (sem_test_char_multi sig test n i Hlein)
  46      (sem_move_multi … L Hlein)
  47      (sem_move_multi … L Hlein)))
  48   [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); * *
  49    #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
  50    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
  51    >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
  52    #Hsome destruct (Hsome) #Htest % [2:@Htest]
  53    >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
  54    #j #lejn cases (true_or_false (eqb i j)) #Hij
  55     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
  56      >Ht3 >nth_change_vec >Ht1 //
  57     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
  58      >Ht3 >nth_change_vec_neq //
  59     ]
  60   |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in  ⊢ (%→?); *
  61    #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
  62    >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
  63    >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
  64    #Htest % // @(eq_vec … (niltape ?))
  65    #j #lejn cases (true_or_false (eqb i j)) #Hij
  66     [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
  67      >Heqtx >Ht3 >nth_change_vec >Ht1 //
  68     |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
  69      >Heqtx >Ht3 >nth_change_vec_neq //
  70     ]
  71   ]
  72 qed.
  73