matita/matita/lib/turing/multi_universal/par_test.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/turing.ma".
  13 include "turing/inject.ma".
  14 include "turing/while_multi.ma".
  15
  16 definition partest_states ≝ initN 3.
  17
  18 definition partest0 : partest_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  19 definition partest1 : partest_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  20 definition partest2 : partest_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  21
  22 definition trans_partest ≝
  23  λsig,n,test.
  24  λp:partest_states × (Vector (option sig) (S n)).
  25  let 〈q,a〉 ≝ p in
  26  if test a then 〈partest1,null_action sig n〉
  27  else 〈partest2,null_action ? n〉.
  28
  29 definition partest ≝
  30   λsig,n,test.
  31   mk_mTM sig n partest_states (trans_partest sig n test)
  32     partest0 (λq.q == partest1 ∨ q == partest2).
  33
  34 definition R_partest_true ≝
  35   λsig,n,test.λint,outt: Vector (tape sig) (S n).
  36   test (current_chars ?? int) = true ∧ outt = int.
  37
  38 definition R_partest_false ≝
  39   λsig,n,test.λint,outt: Vector (tape sig) (S n).
  40   test (current_chars ?? int) = false ∧ outt = int.
  41
  42 lemma partest_q0_q1:
  43   ∀sig,n,test,v.
  44   test (current_chars ?? v) = true →
  45   step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
  46     = mk_mconfig ??? partest1 v.
  47 #sig #n #test #v #Htest
  48 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
  49 @eq_f2
  50 [ whd in ⊢ (??(???%)?); >Htest %
  51 | whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
  52 qed.
  53
  54 lemma partest_q0_q2:
  55   ∀sig,n,test,v.
  56   test (current_chars ?? v) = false →
  57   step sig n (partest sig n test)(mk_mconfig ??? partest0 v)
  58     = mk_mconfig ??? partest2 v.
  59 #sig #n #test #v #Htest
  60 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
  61 @eq_f2
  62 [ whd in ⊢ (??(???%)?); >Htest %
  63 | whd in ⊢ (??(???????(???%))?); >Htest @tape_move_null_action ]
  64 qed.
  65
  66 lemma sem_partest:
  67   ∀sig,n,test.
  68   partest sig n test ⊨
  69     [ partest1: R_partest_true sig n test, R_partest_false sig n test ].
  70 #sig #n #test #int
  71 cases (true_or_false (test (current_chars ?? int))) #Htest
  72 [ %{2} %{(mk_mconfig ? partest_states n partest1 int)} %
  73   [ % [ whd in ⊢ (??%?); >partest_q0_q1 /2/ | #_ % // ]
  74   | * #H @False_ind @H %
  75   ]
  76 | %{2} %{(mk_mconfig ? partest_states n partest2 int)} %
  77   [ % [ whd in ⊢ (??%?); >partest_q0_q2 /2/
  78       | whd in ⊢ (??%%→?); #H destruct (H)]
  79   | #_ % //]
  80 ]
  81 qed.
  82