matita/matita/lib/turing/while_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 "basics/star.ma".
  13 include "turing/mono.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. λM : TM sig. λq:states sig M. λp.
  20   let 〈s,a〉 ≝ p in
  21   if s == q then 〈start ? M, None ?,N〉
  22   else trans ? M p.
  23
  24 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
  25   mk_TM sig
  26     (states ? M)
  27     (while_trans sig M qacc)
  28     (start sig M)
  29     (λs.halt sig M s ∧ ¬ s==qacc).
  30
  31 lemma while_trans_false : ∀sig,M,q,p.
  32   \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
  33 #sig #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,M,acc.halt sig (whileTM sig M acc) acc = false.
  65 #sig #M #acc normalize >(\b ?) // cases (halt sig M acc) %
  66 qed.
  67
  68 lemma halt_while_not_acc :
  69   ∀sig,M,acc,s.s == acc = false → halt sig (whileTM sig M acc) s = halt sig M s.
  70 #sig #M #acc #s #neqs normalize >neqs cases (halt sig M s) %
  71 qed.
  72
  73 lemma step_while_acc :
  74  ∀sig,M,acc,c.cstate ?? c = acc →
  75    step sig (whileTM sig M acc) c = initc … (ctape ?? c).
  76 #sig #M #acc * #s #t #Hs normalize >(\b Hs) %
  77 qed.
  78
  79 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
  80   halt sig M acc = true →
  81   M ⊨ [acc: Rtrue,Rfalse] →
  82     whileTM sig M acc ⊫ (star ? Rtrue) ∘ Rfalse.
  83 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
  84 generalize in match t;
  85 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
  86 cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
  87   [#k1 * #outc1 * #Hloop1 #Hloop2
  88    cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
  89    cut (outcM = outc1)
  90    [ @(loop_eq … k … Hloop1)
  91      @(loop_lift ?? k (λc.c) ?
  92                 (step ? (whileTM ? M acc)) ?
  93                 (λc.halt sig M (cstate ?? c)) ??
  94                 ?? HloopM)
  95      [ #x %
  96      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
  97        [%
  98        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
  99      ]
 100   | #HoutcM1 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
 101       [@tech1 @(ex_intro … (ctape ?? outc1)) %
 102         [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
 103         |@(Hind (m-k1))
 104           [ cases m in Hloop;
 105             [normalize #H destruct (H) ]
 106              #m' #_ cases k1 in Hloop1;
 107              [normalize #H destruct (H) ]
 108              #k1' #_ normalize /2/
 109            | <Hloop2 whd in ⊢ (???%);
 110              >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
 111              normalize in match (halt ?? acc);
 112              >step_while_acc // @(\P Hacc)
 113            ]
 114          ]
 115       |@(ex_intro … intape) % //
 116        cut (Some ? outc1 = Some ? outc)
 117        [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
 118          normalize >(loop_Some ?????? Hloop1) >Hacc %
 119        | #Houtc1c destruct @HMfalse @(\Pf Hacc)
 120        ]
 121      ]
 122    ]
 123  | * #s0 #t0 normalize cases (s0 == acc) normalize
 124    [ cases (halt sig M s0) normalize #Hfalse destruct
 125    | cases (halt sig M s0) normalize //
 126    ]
 127  ]
 128 qed.
 129
 130 theorem terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t.
 131   halt sig M acc = true →
 132   M ⊨ [acc: Rtrue,Rfalse] →
 133   WF ? (inv … Rtrue) t → whileTM sig M acc ↓ t.
 134 #sig #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF
 135 #t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop
 136 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
 137   [cases (Hind ? (Htrue … (\P Hcase))) #iwhile * #outcfinal
 138    #Hloopwhile @(ex_intro … (i+iwhile))
 139    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
 140     [@(λc.halt sig M (cstate … c))
 141     |* #s0 #t0 normalize cases (s0 == acc) normalize
 142      [ cases (halt sig M s0) //
 143      | cases (halt sig M s0) normalize //
 144      ]
 145     |@(loop_lift ?? i (λc.c) ?
 146                 (step ? (whileTM ? M acc)) ?
 147                 (λc.halt sig M (cstate ?? c)) ??
 148                 ?? Hloop)
 149      [ #x %
 150      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
 151        [%
 152        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 153      ]
 154    |@step_while_acc @(\P Hcase)
 155    |>(\P Hcase) @halt_while_acc
 156    ]
 157  |@(ex_intro … i) @(ex_intro … outc)
 158   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ?? c == acc) ???? Hloop)
 159    [#x #Hx >(\P Hx) //
 160    |#x @halt_while_not_acc
 161    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
 162     % #eqx >eqx in H; >Hacctrue #H destruct
 163    |@Hcase
 164    ]
 165  ]
 166 qed.
 167
 168 theorem terminate_while_guarded: ∀sig,M,acc,Pre,Rtrue,Rfalse.
 169   halt sig M acc = true →
 170   accGRealize sig M acc Pre Rtrue Rfalse →
 171   (∀t1,t2. Pre t1 → Rtrue t1 t2 → Pre t2) → ∀t.
 172   WF ? (inv … Rtrue) t → Pre t → whileTM sig M acc ↓ t.
 173 #sig #M #acc #Pre #Rtrue #Rfalse #Hacctrue #HM #Hinv #t #HWF elim HWF
 174 #t1 #H #Hind #HPre cases (HM … t1 HPre) #i * #outc * * #Hloop
 175 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
 176   [cases (Hind ? (Htrue … (\P Hcase)) ?)
 177     [2: @(Hinv … HPre) @Htrue @(\P Hcase)]
 178    #iwhile * #outcfinal
 179    #Hloopwhile @(ex_intro … (i+iwhile))
 180    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
 181     [@(λc.halt sig M (cstate … c))
 182     |* #s0 #t0 normalize cases (s0 == acc) normalize
 183      [ cases (halt sig M s0) //
 184      | cases (halt sig M s0) normalize //
 185      ]
 186     |@(loop_lift ?? i (λc.c) ?
 187                 (step ? (whileTM ? M acc)) ?
 188                 (λc.halt sig M (cstate ?? c)) ??
 189                 ?? Hloop)
 190      [ #x %
 191      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
 192        [%
 193        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 194      ]
 195    |@step_while_acc @(\P Hcase)
 196    |>(\P Hcase) @halt_while_acc
 197    ]
 198  |@(ex_intro … i) @(ex_intro … outc)
 199   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ?? c == acc) ???? Hloop)
 200    [#x #Hx >(\P Hx) //
 201    |#x @halt_while_not_acc
 202    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
 203     % #eqx >eqx in H; >Hacctrue #H destruct
 204    |@Hcase
 205    ]
 206  ]
 207 qed.
 208