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 lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
  63   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
  64     (∀t1,t2,t3. (Rtrue t1 t3 ∧ R2 t3 t2) ∨ (Rfalse t1 t3 ∧ R3 t3 t2) → R4 t1 t2) →
  65     Realize sig
  66      (ifTM sig M1 M2 M3 acc) R4.
  67 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #acc
  68 #HRacc #HRtrue #HRfalse #Hsub
  69 #t cases (sem_if … HRacc HRtrue HRfalse t)
  70 #k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
  71 % [@Hloop] cases Houtc
  72   [* #t3 * #Hleft #Hright @(Hsub … t3) %1 /2/
  73   |* #t3 * #Hleft #Hright @(Hsub … t3) %2 /2/ ]
  74 qed.
  75
  76 axiom acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
  77   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
  78     accRealize sig
  79      (ifTM sig M1 (single_finalTM … M2) M3 acc)
  80      (inr … (inl … (inr … start_nop)))
  81      (Rtrue ∘ R2)
  82      (Rfalse ∘ R3).
  83
  84 lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc.
  85   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
  86     (∀t1,t2,t3. Rtrue t1 t3 → R2 t3 t2 → R4 t1 t2) →
  87     (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) →
  88     accRealize sig
  89      (ifTM sig M1 (single_finalTM … M2) M3 acc)
  90      (inr … (inl … (inr … start_nop)))
  91      R4 R5.
  92 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc
  93 #HRacc #HRtrue #HRfalse #Hsub1 #Hsub2
  94 #t cases (acc_sem_if … HRacc HRtrue HRfalse t)
  95 #k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc)
  96 % [% [@Hloop
  97      |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
  98   |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
  99 qed.
 100
 101 (*
 102 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
 103 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
 104 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
 105   [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
 106    @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
 107    %
 108    [@(loop_merge ???????????
 109     (loop_lift ???
 110       (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
 111       (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
 112       (λc.halt sig M1 (cstate … c))
 113       (λc.halt_liftL ?? (halt sig M1) (cstate … c))
 114       … Hloop1))
 115      [* *
 116        [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 117        | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 118      || #c0 #Hhalt @daemon  (* <step_lift_confL // *)
 119      | #x <p_halt_liftL %
 120      |6:cases outc1 #s1 #t1 %
 121      |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
 122        [ * #s2 #t2 %
 123        | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
 124      |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 125       generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 126       >(trans_liftL_true sig M1 M2 ??)
 127        [ whd in ⊢ (??%?); whd in ⊢ (???%);
 128          @daemon
 129 (*         @config_eq whd in ⊢ (???%); // *)
 130        | @(loop_Some ?????? Hloop10)
 131        | @tdaemon
 132        | skip ]
 133       ]
 134      |
 135      |4:cases outc1 #s1 #t1 %
 136      |5:
 137
 138          @(loop_liftR … Hloop2)
 139          |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 140           generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 141           >(trans_liftL_true sig M1 M2 ??)
 142            [ whd in ⊢ (??%?); whd in ⊢ (???%);
 143              @config_eq //
 144            | @(loop_Some ?????? Hloop10) ]
 145            ]
 146 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 147   % //
 148 ]
 149 qed.
 150 *)