matita/matita/lib/turing/while_multi.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 "basics/star.ma".
  13 include "turing/turing.ma".
  14
  15 (* The following machine implements a while-loop over a body machine $M$.
  16 We just need to extend $M$ adding a single transition leading back from a
  17 distinguished final state $q$ to the initial state. *)
  18
  19 definition while_trans ≝ λsig,n. λM: mTM sig n. λq:states sig n M. λp.
  20   let 〈s,a〉 ≝ p in
  21   if s == q then 〈start ?? M, null_action ??〉
  22   else trans ?? M p.
  23
  24 definition whileTM ≝ λsig,n. λM: mTM sig n. λqacc: states ?? M.
  25   mk_mTM sig n
  26     (states ?? M)
  27     (while_trans sig n M qacc)
  28     (start sig n M)
  29     (λs.halt sig n M s ∧ ¬ s==qacc).
  30
  31 lemma while_trans_false : ∀sig,n,M,q,p.
  32   \fst p ≠ q → trans sig n (whileTM sig n M q) p = trans sig n M p.
  33 #sig #n #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
  34 qed.
  35
  36 lemma loop_lift_acc : ∀A,B,k,lift,f,g,h,hlift,c1,c2,subh.
  37   (∀x.subh x = true → h x = true) →
  38   (∀x.subh x = false → hlift (lift x) = h x) →
  39   (∀x.h x = false → lift (f x) = g (lift x)) →
  40   subh c2 = false →
  41   loop A k f h c1 = Some ? c2 →
  42   loop B k g hlift (lift c1) = Some ? (lift … c2).
  43 #A #B #k #lift #f #g #h #hlift #c1 #c2 #subh #Hsubh #Hlift #Hfg #Hc2
  44 generalize in match c1; elim k
  45 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
  46 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
  47  cases (true_or_false (h c0)) #Hc0 >Hc0
  48    [ normalize #Heq destruct (Heq) >(Hlift … Hc2) >Hc0 //
  49    | normalize >(Hlift c0)
  50      [>Hc0 normalize <(Hfg … Hc0) @IH
  51      |cases (true_or_false (subh c0)) //
  52       #H <Hc0 @sym_eq >H @Hsubh //
  53    ]
  54  ]
  55 qed.
  56
  57 lemma tech1: ∀A.∀R1,R2:relation A.
  58   ∀a,b. (R1 ∘ ((star ? R1) ∘ R2)) a b → ((star ? R1) ∘ R2) a b.
  59 #A #R1 #R2 #a #b #H lapply (sub_assoc_l ?????? H) @sub_comp_l -a -b
  60 #a #b * #c * /2/
  61 qed.
  62
  63 lemma halt_while_acc :
  64   ∀sig,n,M,acc.halt sig n (whileTM sig n M acc) acc = false.
  65 #sig #n #M #acc normalize >(\b ?) // cases (halt sig n M acc) %
  66 qed.
  67
  68 lemma halt_while_not_acc :
  69   ∀sig,n,M,acc,s.s == acc = false →
  70   halt sig n (whileTM sig n M acc) s = halt sig n M s.
  71 #sig #n #M #acc #s #neqs normalize >neqs cases (halt sig n M s) %
  72 qed.
  73
  74 lemma step_while_acc :
  75  ∀sig,n,M,acc,c.cstate ??? c = acc →
  76    step sig n (whileTM sig n M acc) c = initc … (ctapes ??? c).
  77 #sig #n #M #acc * #s #t #Hs whd in match (step ????);
  78 whd in match (trans ????); >(\b Hs)
  79 <(tape_move_null_action ?? t) in ⊢ (???%); //
  80 qed.
  81
  82 theorem sem_while: ∀sig,n,M,acc,Rtrue,Rfalse.
  83   halt sig n M acc = true →
  84   M ⊨ [acc: Rtrue,Rfalse] →
  85     whileTM sig n M acc ⊫ (star ? Rtrue) ∘ Rfalse.
  86 #sig #n #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
  87 generalize in match t;
  88 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
  89 cases (loop_split ?? (λc. halt sig n M (cstate ??? c)) ????? Hloop)
  90   [#k1 * #outc1 * #Hloop1 #Hloop2
  91    cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
  92    cut (outcM = outc1)
  93    [ @(loop_eq … k … Hloop1)
  94      @(loop_lift ?? k (λc.c) ?
  95                 (step ?? (whileTM ?? M acc)) ?
  96                 (λc.halt sig n M (cstate ??? c)) ??
  97                 ?? HloopM)
  98      [ #x %
  99      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
 100        [%
 101        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 102      ]
 103   | #HoutcM1 cases (true_or_false (cstate ??? outc1 == acc)) #Hacc
 104       [@tech1 @(ex_intro … (ctapes ??? outc1)) %
 105         [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
 106         |@(Hind (m-k1))
 107           [ cases m in Hloop;
 108             [normalize #H destruct (H) ]
 109              #m' #_ cases k1 in Hloop1;
 110              [normalize #H destruct (H) ]
 111              #k1' #_ normalize /2/
 112            | <Hloop2 whd in ⊢ (???%);
 113              >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
 114              normalize in match (halt ??? acc);
 115              >step_while_acc // @(\P Hacc)
 116            ]
 117          ]
 118       |@(ex_intro … intape) % //
 119        cut (Some ? outc1 = Some ? outc)
 120        [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
 121          normalize >(loop_Some ?????? Hloop1) >Hacc %
 122        | #Houtc1c destruct @HMfalse @(\Pf Hacc)
 123        ]
 124      ]
 125    ]
 126  | * #s0 #t0 normalize cases (s0 == acc) normalize
 127    [ cases (halt sig n M s0) normalize #Hfalse destruct
 128    | cases (halt sig n M s0) normalize //
 129    ]
 130  ]
 131 qed.
 132
 133 theorem terminate_while: ∀sig,n,M,acc,Rtrue,Rfalse,t.
 134   halt sig n M acc = true →
 135   M ⊨ [acc: Rtrue,Rfalse] →
 136   WF ? (inv … Rtrue) t → whileTM sig n M acc ↓ t.
 137 #sig #n #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF
 138 #t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop
 139 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
 140   [cases (Hind ? (Htrue … (\P Hcase))) #iwhile * #outcfinal
 141    #Hloopwhile @(ex_intro … (i+iwhile))
 142    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
 143     [@(λc.halt sig n M (cstate … c))
 144     |* #s0 #t0 normalize cases (s0 == acc) normalize
 145      [ cases (halt sig n M s0) //
 146      | cases (halt sig n M s0) normalize //
 147      ]
 148     |@(loop_lift ?? i (λc.c) ?
 149                 (step ?? (whileTM ?? M acc)) ?
 150                 (λc.halt sig n M (cstate ??? c)) ??
 151                 ?? Hloop)
 152      [ #x %
 153      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
 154        [%
 155        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 156      ]
 157    |@step_while_acc @(\P Hcase)
 158    |>(\P Hcase) @halt_while_acc
 159    ]
 160  |@(ex_intro … i) @(ex_intro … outc)
 161   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ??? c == acc) ???? Hloop)
 162    [#x #Hx >(\P Hx) //
 163    |#x @halt_while_not_acc
 164    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
 165     % #eqx >eqx in H; >Hacctrue #H destruct
 166    |@Hcase
 167    ]
 168  ]
 169 qed.
 170
 171 theorem terminate_while_guarded: ∀sig,n,M,acc,Pre,Rtrue,Rfalse.
 172   halt sig n M acc = true →
 173   accGRealize sig n M acc Pre Rtrue Rfalse →
 174   (∀t1,t2. Pre t1 → Rtrue t1 t2 → Pre t2) → ∀t.
 175   WF ? (inv … Rtrue) t → Pre t → whileTM sig n M acc ↓ t.
 176 #sig #n #M #acc #Pre #Rtrue #Rfalse #Hacctrue #HM #Hinv #t #HWF elim HWF
 177 #t1 #H #Hind #HPre cases (HM … t1 HPre) #i * #outc * * #Hloop
 178 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
 179   [cases (Hind ? (Htrue … (\P Hcase)) ?)
 180     [2: @(Hinv … HPre) @Htrue @(\P Hcase)]
 181    #iwhile * #outcfinal
 182    #Hloopwhile @(ex_intro … (i+iwhile))
 183    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
 184     [@(λc.halt sig n M (cstate … c))
 185     |* #s0 #t0 normalize cases (s0 == acc) normalize
 186      [ cases (halt sig n M s0) //
 187      | cases (halt sig n M s0) normalize //
 188      ]
 189     |@(loop_lift ?? i (λc.c) ?
 190                 (step ?? (whileTM ?? M acc)) ?
 191                 (λc.halt sig n M (cstate ??? c)) ??
 192                 ?? Hloop)
 193      [ #x %
 194      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
 195        [%
 196        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 197      ]
 198    |@step_while_acc @(\P Hcase)
 199    |>(\P Hcase) @halt_while_acc
 200    ]
 201  |@(ex_intro … i) @(ex_intro … outc)
 202   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ??? c == acc) ???? Hloop)
 203    [#x #Hx >(\P Hx) //
 204    |#x @halt_while_not_acc
 205    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
 206     % #eqx >eqx in H; >Hacctrue #H destruct
 207    |@Hcase
 208    ]
 209  ]
 210 qed.
 211