matita/matita/lib/turing/if_machine.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/mono.ma".
  13
  14 definition single_finalTM ≝
  15   λsig.λM:TM sig.seq ? M (nop ?).
  16
  17 lemma sem_single_final :
  18   ∀sig,M,R.Realize ? M R → Realize ? (single_finalTM sig M) R.
  19 #sig #M #R #HR #intape
  20 cases (sem_seq ????? HR (sem_nop …) intape)
  21 #k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc
  22 @(ex_intro ?? k) @(ex_intro ?? outc) %  [ @Hloop | >Houtc // ]
  23 qed.
  24
  25 definition if_trans ≝ λsig. λM1,M2,M3 : TM sig. λq:states sig M1.
  26 λp. let 〈s,a〉 ≝ p in
  27   match s with
  28   [ inl s1 ⇒
  29       if halt sig M1 s1 then
  30         if s1==q then 〈inr … (inl … (start sig M2)), None ?〉
  31         else 〈inr … (inr … (start sig M3)), None ?〉
  32       else let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
  33        〈inl … news1,m〉
  34   | inr s' ⇒
  35       match s' with
  36       [ inl s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
  37          〈inr … (inl … news2),m〉
  38       | inr s3 ⇒ let 〈news3,m〉 ≝ trans sig M3 〈s3,a〉 in
  39          〈inr … (inr … news3),m〉
  40       ]
  41   ].
  42
  43 definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
  44   λqacc: states sig condM.
  45   mk_TM sig
  46     (FinSum (states sig condM) (FinSum (states sig thenM) (states sig elseM)))
  47     (if_trans sig condM thenM elseM qacc)
  48     (inl … (start sig condM))
  49     (λs.match s with
  50       [ inl _ ⇒ false
  51       | inr s' ⇒ match s' with
  52         [ inl s2 ⇒ halt sig thenM s2
  53         | inr s3 ⇒ halt sig elseM s3 ]]).
  54
  55 axiom daemon : ∀X:Prop.X.
  56 axiom tdaemon : ∀X:Type[0].X.
  57
  58 axiom sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
  59   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
  60     Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
  61
  62 axiom acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
  63   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
  64     accRealize sig
  65      (ifTM sig M1 (single_finalTM … M2) M3 acc)
  66      (inr … (inl … (inr … 0)))
  67      (Rtrue ∘ R2)
  68      (Rfalse ∘ R3).
  69 (*
  70 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
  71 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
  72 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
  73   [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
  74    @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
  75    %
  76    [@(loop_merge ???????????
  77     (loop_lift ???
  78       (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
  79       (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
  80       (λc.halt sig M1 (cstate … c))
  81       (λc.halt_liftL ?? (halt sig M1) (cstate … c))
  82       … Hloop1))
  83      [* *
  84        [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
  85        | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
  86      || #c0 #Hhalt @daemon  (* <step_lift_confL // *)
  87      | #x <p_halt_liftL %
  88      |6:cases outc1 #s1 #t1 %
  89      |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
  90        [ * #s2 #t2 %
  91        | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
  92      |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
  93       generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
  94       >(trans_liftL_true sig M1 M2 ??)
  95        [ whd in ⊢ (??%?); whd in ⊢ (???%);
  96          @daemon
  97 (*         @config_eq whd in ⊢ (???%); // *)
  98        | @(loop_Some ?????? Hloop10)
  99        | @tdaemon
 100        | skip ]
 101       ]
 102      |
 103      |4:cases outc1 #s1 #t1 %
 104      |5:
 105
 106          @(loop_liftR … Hloop2)
 107          |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 108           generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 109           >(trans_liftL_true sig M1 M2 ??)
 110            [ whd in ⊢ (??%?); whd in ⊢ (???%);
 111              @config_eq //
 112            | @(loop_Some ?????? Hloop10) ]
 113            ]
 114 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 115   % //
 116 ]
 117 qed.
 118 *)