matita/matita/lib/turing/universal/tests.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/if_machine.ma".
  13
  14 (* TEST CHAR
  15
  16    stato finale diverso a seconda che il carattere
  17    corrente soddisfi un test booleano oppure no
  18
  19    q1 = true or no current char
  20    q2 = false
  21 *)
  22
  23 definition tc_states ≝ initN 3.
  24
  25 definition tc_start : tc_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  26 definition tc_true : tc_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  27 definition tc_false : tc_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  28
  29 definition test_char ≝
  30   λalpha:FinSet.λtest:alpha→bool.
  31   mk_TM alpha tc_states
  32   (λp.let 〈q,a〉 ≝ p in
  33    match a with
  34    [ None ⇒ 〈tc_true, None ?〉
  35    | Some a' ⇒
  36      match test a' with
  37      [ true ⇒ 〈tc_true,None ?〉
  38      | false ⇒ 〈tc_false,None ?〉 ]])
  39   tc_start (λx.notb (x == tc_start)).
  40
  41 definition Rtc_true ≝
  42   λalpha,test,t1,t2.
  43    ∀c. current alpha t1 = Some ? c →
  44    test c = true ∧ t2 = t1.
  45
  46 definition Rtc_false ≝
  47   λalpha,test,t1,t2.
  48     ∀c. current alpha t1 = Some ? c →
  49     test c = false ∧ t2 = t1.
  50
  51 lemma tc_q0_q1 :
  52   ∀alpha,test,ls,a0,rs. test a0 = true →
  53   step alpha (test_char alpha test)
  54     (mk_config ?? tc_start (midtape … ls a0 rs)) =
  55   mk_config alpha (states ? (test_char alpha test)) tc_true
  56     (midtape … ls a0 rs).
  57 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  58 whd in match (trans … 〈?,?〉); >Htest %
  59 qed.
  60
  61 lemma tc_q0_q2 :
  62   ∀alpha,test,ls,a0,rs. test a0 = false →
  63   step alpha (test_char alpha test)
  64     (mk_config ?? tc_start (midtape … ls a0 rs)) =
  65   mk_config alpha (states ? (test_char alpha test)) tc_false
  66     (midtape … ls a0 rs).
  67 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  68 whd in match (trans … 〈?,?〉); >Htest %
  69 qed.
  70
  71 lemma sem_test_char :
  72   ∀alpha,test.
  73   accRealize alpha (test_char alpha test)
  74     tc_true (Rtc_true alpha test) (Rtc_false alpha test).
  75 #alpha #test *
  76 [ @(ex_intro ?? 2)
  77   @(ex_intro ?? (mk_config ?? tc_true (niltape ?))) %
  78   [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
  79 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (leftof ? a al)))
  80   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
  81 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? tc_true (rightof ? a al)))
  82   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
  83 | #ls #c #rs @(ex_intro ?? 2)
  84   cases (true_or_false (test c)) #Htest
  85   [ @(ex_intro ?? (mk_config ?? tc_true ?))
  86     [| %
  87       [ %
  88         [ whd in ⊢ (??%?); >tc_q0_q1 //
  89         | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
  90       | * #Hfalse @False_ind @Hfalse % ]
  91     ]
  92   | @(ex_intro ?? (mk_config ?? tc_false (midtape ? ls c rs)))
  93     %
  94     [ %
  95       [ whd in ⊢ (??%?); >tc_q0_q2 //
  96       | whd in ⊢ ((??%%)→?); #Hfalse destruct (Hfalse) ]
  97     | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
  98     ]
  99   ]
 100 ]
 101 qed.