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 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
  16   let 〈s,a〉 ≝ p in
  17   if s == q then 〈start ? M, None ?〉
  18   else trans ? M p.
  19
  20 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
  21   mk_TM sig
  22     (states ? M)
  23     (while_trans sig M qacc)
  24     (start sig M)
  25     (λs.halt sig M s ∧ ¬ s==qacc).
  26
  27 (* axiom daemon : ∀X:Prop.X. *)
  28
  29 lemma while_trans_false : ∀sig,M,q,p.
  30   \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
  31 #sig #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
  32 qed.
  33
  34 lemma loop_lift_acc : ∀A,B,k,lift,f,g,h,hlift,c1,c2,subh.
  35   (∀x.subh x = true → h x = true) →
  36   (∀x.subh x = false → hlift (lift x) = h x) →
  37   (∀x.h x = false → lift (f x) = g (lift x)) →
  38   subh c2 = false →
  39   loop A k f h c1 = Some ? c2 →
  40   loop B k g hlift (lift c1) = Some ? (lift … c2).
  41 #A #B #k #lift #f #g #h #hlift #c1 #c2 #subh #Hsubh #Hlift #Hfg #Hc2
  42 generalize in match c1; elim k
  43 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
  44 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
  45  cases (true_or_false (h c0)) #Hc0 >Hc0
  46    [ normalize #Heq destruct (Heq) >(Hlift … Hc2) >Hc0 //
  47    | normalize >(Hlift c0)
  48      [>Hc0 normalize <(Hfg … Hc0) @IH
  49      |cases (true_or_false (subh c0)) //
  50       #H <Hc0 @sym_eq >H @Hsubh //
  51    ]
  52  ]
  53 qed.
  54
  55 axiom tech1: ∀A.∀R1,R2:relation A.
  56   ∀a,b. (R1 ∘ ((star ? R1) ∘ R2)) a b → ((star ? R1) ∘ R2) a b.
  57
  58 lemma halt_while_acc :
  59   ∀sig,M,acc.halt sig (whileTM sig M acc) acc = false.
  60 #sig #M #acc normalize >(\b ?) //
  61 cases (halt sig M acc) %
  62 qed.
  63
  64 lemma halt_while_not_acc :
  65   ∀sig,M,acc,s.s == acc = false → halt sig (whileTM sig M acc) s = halt sig M s.
  66 #sig #M #acc #s #neqs normalize >neqs
  67 cases (halt sig M s) %
  68 qed.
  69
  70 lemma step_while_acc :
  71  ∀sig,M,acc,c.cstate ?? c = acc →
  72    step sig (whileTM sig M acc) c = initc … (ctape ?? c).
  73 #sig #M #acc * #s #t #Hs normalize >(\b Hs) %
  74 qed.
  75
  76 lemma loop_p_true :
  77   ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a.
  78 #A #k #f #p #a #Ha normalize >Ha %
  79 qed.
  80
  81 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
  82   halt sig M acc = true →
  83   accRealize sig M acc Rtrue Rfalse →
  84     WRealize sig (whileTM sig M acc) ((star ? Rtrue) ∘ Rfalse).
  85 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
  86 generalize in match t;
  87 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
  88 cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
  89   [#k1 * #outc1 * #Hloop1 #Hloop2
  90    cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
  91    cut (outcM = outc1)
  92    [ @(loop_eq … k … Hloop1)
  93      @(loop_lift ?? k (λc.c) ?
  94                 (step ? (whileTM ? M acc)) ?
  95                 (λc.halt sig M (cstate ?? c)) ??
  96                 ?? HloopM)
  97      [ #x %
  98      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
  99        [%
 100        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 101      ]
 102   | #HoutcM1 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
 103       [@tech1 @(ex_intro … (ctape ?? outc1)) %
 104         [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
 105         |@(Hind (m-k1))
 106           [ cases m in Hloop;
 107             [normalize #H destruct (H) ]
 108              #m' #_ cases k1 in Hloop1;
 109              [normalize #H destruct (H) ]
 110              #k1' #_ normalize /2/
 111            | <Hloop2 whd in ⊢ (???%);
 112              >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
 113              normalize in match (halt ?? acc);
 114              >step_while_acc // @(\P Hacc)
 115            ]
 116          ]
 117       |@(ex_intro … intape) % //
 118        cut (Some ? outc1 = Some ? outc)
 119        [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
 120          normalize >(loop_Some ?????? Hloop1) >Hacc %
 121        | #Houtc1c destruct @HMfalse @(\Pf Hacc)
 122        ]
 123      ]
 124    ]
 125  | * #s0 #t0 normalize cases (s0 == acc) normalize
 126    [ cases (halt sig M s0) normalize #Hfalse destruct
 127    | cases (halt sig M s0) normalize //
 128    ]
 129  ]
 130 qed.
 131
 132 theorem terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t.
 133   halt sig M acc = true →
 134   accRealize sig M acc Rtrue Rfalse →
 135   WF ? (inv … Rtrue) t → Terminate sig (whileTM sig M acc) t.
 136 #sig #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF
 137 #t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop
 138 #Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
 139   [cases (Hind ? (Htrue … (\P Hcase))) #iwhile * #outcfinal
 140    #Hloopwhile @(ex_intro … (i+iwhile))
 141    @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
 142     [@(λc.halt sig M (cstate … c))
 143     |* #s0 #t0 normalize cases (s0 == acc) normalize
 144      [ cases (halt sig M s0) //
 145      | cases (halt sig M s0) normalize //
 146      ]
 147     |@(loop_lift ?? i (λc.c) ?
 148                 (step ? (whileTM ? M acc)) ?
 149                 (λc.halt sig M (cstate ?? c)) ??
 150                 ?? Hloop)
 151      [ #x %
 152      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
 153        [%
 154        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
 155      ]
 156    |@step_while_acc @(\P Hcase)
 157    |>(\P Hcase) @halt_while_acc
 158    ]
 159  |@(ex_intro … i) @(ex_intro … outc)
 160   @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ?? c == acc) ???? Hloop)
 161    [#x #Hx >(\P Hx) //
 162    |#x @halt_while_not_acc
 163    |#x #H whd in ⊢ (??%%); >while_trans_false [%]
 164     % #eqx >eqx in H; >Hacctrue #H destruct
 165    |@Hcase
 166    ]
 167  ]
 168 qed.
 169
 170 (*
 171 axiom terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t.
 172   halt sig M acc = true →
 173   accRealize sig M acc Rtrue Rfalse →
 174   ∃t1. Rfalse t t1 → Terminate sig (whileTM sig M acc) t.
 175 *)
 176
 177 (* (*
 178
 179 (* We do not distinuish an input tape *)
 180
 181 record TM (sig:FinSet): Type[1] ≝
 182 { states : FinSet;
 183   trans : states × (option sig) → states × (option (sig × move));
 184   start: states;
 185   halt : states → bool
 186 }.
 187
 188 record config (sig:FinSet) (M:TM sig): Type[0] ≝
 189 { cstate : states sig M;
 190   ctape: tape sig
 191 }.
 192
 193 definition option_hd ≝ λA.λl:list A.
 194   match l with
 195   [nil ⇒ None ?
 196   |cons a _ ⇒ Some ? a
 197   ].
 198
 199 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
 200   match m with
 201   [ None ⇒ t
 202   | Some m1 ⇒
 203     match \snd m1 with
 204     [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
 205     | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
 206     ]
 207   ].
 208
 209 definition step ≝ λsig.λM:TM sig.λc:config sig M.
 210   let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
 211   let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
 212   mk_config ?? news (tape_move sig (ctape ?? c) mv).
 213
 214 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 215   match n with
 216   [ O ⇒ None ?
 217   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 218   ].
 219
 220 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
 221   loop A k1 f p a1 = Some ? a2 →
 222     loop A (k2+k1) f p a1 = Some ? a2.
 223 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
 224 [normalize #a0 #Hfalse destruct
 225 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
 226  cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
 227 ]
 228 qed.
 229
 230 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 231  ∀k1,k2,a1,a2,a3,a4.
 232    loop A k1 f p a1 = Some ? a2 →
 233      f a2 = a3 → q a2 = false →
 234        loop A k2 f q a3 = Some ? a4 →
 235          loop A (k1+k2) f q a1 = Some ? a4.
 236 #Sig #f #p #q #Hpq #k1 elim k1
 237   [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
 238   |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
 239    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 240    [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
 241     whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
 242     whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
 243    |normalize >(Hpq … pa1) normalize
 244     #H1 #H2 #H3 @(Hind … H2) //
 245    ]
 246  ]
 247 qed.
 248
 249 (*
 250 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 251  ∀k1,k2,a1,a2,a3.
 252    loop A k1 f p a1 = Some ? a2 →
 253      loop A k2 f q a2 = Some ? a3 →
 254        loop A (k1+k2) f q a1 = Some ? a3.
 255 #Sig #f #p #q #Hpq #k1 elim k1
 256   [normalize #k2 #a1 #a2 #a3 #H destruct
 257   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
 258    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 259    [#eqa1a2 destruct #H @loop_incr //
 260    |normalize >(Hpq … pa1) normalize
 261     #H1 #H2 @(Hind … H2) //
 262    ]
 263  ]
 264 qed.
 265 *)
 266
 267 definition initc ≝ λsig.λM:TM sig.λt.
 268   mk_config sig M (start sig M) t.
 269
 270 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 271 ∀t.∃i.∃outc.
 272   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
 273   R t (ctape ?? outc).
 274
 275 (* Compositions *)
 276
 277 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 278 λp. let 〈s,a〉 ≝ p in
 279   match s with
 280   [ inl s1 ⇒
 281       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 282       else
 283       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 284       〈inl … news1,m〉
 285   | inr s2 ⇒
 286       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 287       〈inr … news2,m〉
 288   ].
 289
 290 definition seq ≝ λsig. λM1,M2 : TM sig.
 291   mk_TM sig
 292     (FinSum (states sig M1) (states sig M2))
 293     (seq_trans sig M1 M2)
 294     (inl … (start sig M1))
 295     (λs.match s with
 296       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 297
 298 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 299   ∃am.R1 a1 am ∧ R2 am a2.
 300
 301 (*
 302 definition injectRl ≝ λsig.λM1.λM2.λR.
 303    λc1,c2. ∃c11,c12.
 304      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 305      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 306      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 307      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 308      R c11 c12.
 309
 310 definition injectRr ≝ λsig.λM1.λM2.λR.
 311    λc1,c2. ∃c21,c22.
 312      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 313      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 314      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 315      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 316      R c21 c22.
 317
 318 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 319   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 320   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 321   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 322
 323 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 324
 325 definition lift_confL ≝
 326   λsig,M1,M2,c.match c with
 327   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 328 definition lift_confR ≝
 329   λsig,M1,M2,c.match c with
 330   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 331
 332 definition halt_liftL ≝
 333   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 334   match s with
 335   [ inl s1 ⇒ halt sig M1 s1
 336   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 337
 338 definition halt_liftR ≝
 339   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 340   match s with
 341   [ inl _ ⇒ false
 342   | inr s2 ⇒ halt sig M2 s2 ].
 343
 344 lemma p_halt_liftL : ∀sig,M1,M2,c.
 345   halt sig M1 (cstate … c) =
 346      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 347 #sig #M1 #M2 #c cases c #s #t %
 348 qed.
 349
 350 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 351   halt ? M1 s = false →
 352   trans sig M1 〈s,a〉 = 〈news,move〉 →
 353   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 354 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 355 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 356 qed.
 357
 358 lemma config_eq :
 359   ∀sig,M,c1,c2.
 360   cstate sig M c1 = cstate sig M c2 →
 361   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 362 #sig #M1 * #s1 #t1 * #s2 #t2 //
 363 qed.
 364
 365 lemma step_lift_confL : ∀sig,M1,M2,c0.
 366  halt ? M1 (cstate ?? c0) = false →
 367  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 368  lift_confL sig M1 M2 (step sig M1 c0).
 369 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
 370 #rs #Hhalt
 371 whd in ⊢ (???(????%));whd in ⊢ (???%);
 372 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
 373 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
 374 #s0 #m0 #Heq whd in ⊢ (???%);
 375 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 376 >(trans_liftL … Heq)
 377 [% | //]
 378 qed.
 379
 380 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 381   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 382     loop ? k (step sig (seq sig M1 M2))
 383       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 384     Some ? (lift_confL … c2).
 385 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 386 elim k
 387 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 388 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 389  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 390  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 391  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 392    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 393    | // ]
 394  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 395    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 396     @step_lift_confL //
 397    | // ]
 398 qed.
 399
 400 STOP!
 401
 402 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
 403   loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
 404     loop ? k (step sig (seq sig M1 M2))
 405       (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
 406     Some ? (lift_confR … c2).
 407 #sig #k #M1 #M2 #c1 #c2
 408 elim k
 409 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 410 |#k0 #IH whd in ⊢ (??%? → ??%?);
 411  lapply (refl ? (halt ?? (cstate sig M2 c1)))
 412  cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
 413  [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
 414    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
 415    | (* ... *) ]
 416  | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
 417    [whd in ⊢ (??%? → ??%?); #Hc2 <IH
 418      [@eq_f (* @step_lift_confR // *)
 419      |
 420    | // ]
 421 qed. *)
 422
 423 lemma loop_Some :
 424   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 425 #A #k #f #p #a #b elim k
 426 [normalize #Hfalse destruct
 427 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
 428  [ normalize #H1 destruct
 429
 430 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 431   halt ? M1 s = true →
 432   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 433 #sig #M1 #M2 #s #a
 434 #Hhalt whd in ⊢ (??%?); >Hhalt %
 435 qed.
 436
 437 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
 438   ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
 439 #sig #M1 #M2 #outc cases outc #s #t %
 440 qed.
 441
 442 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
 443   ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
 444 #sig #M1 #M2 #outc cases outc #s #t %
 445 qed.
 446
 447 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 448   Realize sig M1 R1 → Realize sig M2 R2 →
 449     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 450 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 451 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 452 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 453 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 454 %
 455 [@(loop_split ??????????? (loop_liftL … Hloop1))
 456  [* *
 457    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 458    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 459  ||4:cases outc1 #s1 #t1 %
 460  |5:@(loop_liftR … Hloop2)
 461  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 462   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 463   >(trans_liftL_true sig M1 M2 ??)
 464   [ whd in ⊢ (??%?); whd in ⊢ (???%);
 465     @config_eq //
 466   | @(loop_Some ?????? Hloop10) ]
 467  ]
 468 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 469   % //
 470 ]
 471 qed.
 472
 473 (* boolean machines: machines with two distinguished halting states *)
 474
 475
 476
 477 (* old stuff *)
 478 definition empty_tapes ≝ λsig.λn.
 479 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 480 elim n // normalize //
 481 qed.
 482
 483 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 484   mk_config ??
 485     (start sig M)
 486     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 487     [ ].
 488
 489 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 490   halt sig M (state sig M c).
 491
 492 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 493   match n with
 494   [ O ⇒ None ?
 495   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 496   ].
 497
 498 (* Compute ? M f states that f is computed by M *)
 499 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 500 ∀l.∃i.∃c.
 501   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 502   out ?? c = f l.
 503
 504 (* for decision problems, we accept a string if on termination
 505 output is not empty *)
 506
 507 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 508 ∀l.∃i.∃c.
 509   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 510   (isnilb ? (out ?? c) = false).
 511
 512 (* alternative approach.
 513 We define the notion of computation. The notion must be constructive,
 514 since we want to define functions over it, like lenght and size
 515
 516 Perche' serve Type[2] se sposto a e b a destra? *)
 517
 518 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 519   mk_move: p a = false → b = f a → cmove A f p a b.
 520
 521 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 522 | empty : ∀a. cstar A M a a
 523 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 524
 525 definition computation ≝ λsig.λM:TM sig.
 526   cstar ? (cmove ? (step sig M) (stop sig M)).
 527
 528 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 529   ∀l.∃c.computation sig M (init sig M l) c →
 530    (stop sig M c = true) ∧ out ?? c = f l.
 531
 532 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 533   ∀l.∃c.computation sig M (init sig M l) c →
 534    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
 535 *)