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 step_while_acc :
  65  ∀sig,M,acc,c.cstate ?? c = acc →
  66    step sig (whileTM sig M acc) c = initc … (ctape ?? c).
  67 #sig #M #acc * #s #t #Hs normalize >(\b Hs) %
  68 qed.
  69
  70 lemma loop_p_true :
  71   ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a.
  72 #A #k #f #p #a #Ha normalize >Ha %
  73 qed.
  74
  75 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
  76   halt sig M acc = true →
  77   accRealize sig M acc Rtrue Rfalse →
  78     WRealize sig (whileTM sig M acc) ((star ? Rtrue) ∘ Rfalse).
  79 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
  80 generalize in match t;
  81 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
  82 cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
  83   [#k1 * #outc1 * #Hloop1 #Hloop2
  84    cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
  85    cut (outcM = outc1)
  86    [ @(loop_eq … k … Hloop1)
  87      @(loop_lift ?? k (λc.c) ?
  88                 (step ? (whileTM ? M acc)) ?
  89                 (λc.halt sig M (cstate ?? c)) ??
  90                 ?? HloopM)
  91      [ #x %
  92      | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
  93        [%
  94        |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
  95      ]
  96   | #HoutcM1 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
  97       [@tech1 @(ex_intro … (ctape ?? outc1)) %
  98         [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
  99         |@(Hind (m-k1))
 100           [ cases m in Hloop;
 101             [normalize #H destruct (H) ]
 102              #m' #_ cases k1 in Hloop1;
 103              [normalize #H destruct (H) ]
 104              #k1' #_ normalize /2/
 105            | <Hloop2 whd in ⊢ (???%);
 106              >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
 107              normalize in match (halt ?? acc);
 108              >step_while_acc // @(\P Hacc)
 109            ]
 110          ]
 111       |@(ex_intro … intape) % //
 112        cut (Some ? outc1 = Some ? outc)
 113        [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
 114          normalize >(loop_Some ?????? Hloop1) >Hacc %
 115        | #Houtc1c destruct @HMfalse @(\Pf Hacc)
 116        ]
 117      ]
 118    ]
 119  | * #s0 #t0 normalize cases (s0 == acc) normalize
 120    [ cases (halt sig M s0) normalize #Hfalse destruct
 121    | cases (halt sig M s0) normalize //
 122    ]
 123  ]
 124 qed.
 125
 126 (* inductive move_states : Type[0] ≝
 127 | start : move_states
 128 | q1 : move_states
 129 | q2 : move_states
 130 | q3 : move_states
 131 | qacc : move_states
 132 | qfail : move_states.
 133
 134 definition
 135 *)
 136
 137 definition mystates : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
 138
 139 definition move_char ≝
 140  λalpha:FinSet.λsep:alpha.
 141  mk_TM alpha (mystates alpha)
 142  (λp.let 〈q,a〉 ≝ p in
 143   let 〈q',b〉 ≝ q in
 144   match a with
 145   [ None ⇒ 〈〈4,sep〉,None ?〉
 146   | Some a' ⇒
 147   match q' with
 148   [ O ⇒ (* qinit *)
 149     match a' == sep with
 150     [ true ⇒ 〈〈4,sep〉,None ?〉
 151     | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ]
 152   | S q' ⇒ match q' with
 153     [ O ⇒ (* q1 *)
 154       〈〈2,a'〉,Some ? 〈b,R〉〉
 155     | S q' ⇒ match q' with
 156       [ O ⇒ (* q2 *)
 157         〈〈3,sep〉,Some ? 〈b,R〉〉
 158       | S q' ⇒ match q' with
 159         [ O ⇒ (* qacc *)
 160           〈〈3,sep〉,None ?〉
 161         | S q' ⇒ (* qfail *)
 162           〈〈4,sep〉,None ?〉 ] ] ] ] ])
 163   〈0,sep〉
 164   (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
 165
 166 definition mk_tape :
 167   ∀sig:FinSet.list sig → option sig → list sig → tape sig ≝
 168   λsig,lt,c,rt.match c with
 169   [ Some c' ⇒ midtape sig lt c' rt
 170   | None ⇒ match lt with
 171     [ nil ⇒ match rt with
 172       [ nil ⇒ niltape ?
 173       | cons r0 rs0 ⇒ leftof ? r0 rs0 ]
 174     | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
 175
 176 lemma cmove_q0_q1 :
 177   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
 178   a0 == sep = false →
 179   step alpha (move_char alpha sep)
 180     (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
 181   mk_config alpha (states ? (move_char alpha sep)) 〈1,a0〉
 182     (tape_move_left alpha ls a0 rs).
 183 #alpha #sep #a *
 184 [ #a0 #rs #Ha0 whd in ⊢ (??%?);
 185   normalize in match (trans ???); >Ha0 %
 186 | #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
 187   normalize in match (trans ???); >Ha0 %
 188 ]
 189 qed.
 190
 191 lemma cmove_q1_q2 :
 192   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
 193   step alpha (move_char alpha sep)
 194     (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) =
 195   mk_config alpha (states ? (move_char alpha sep)) 〈2,a0〉
 196     (tape_move_right alpha ls a rs).
 197 #alpha #sep #a #ls #a0 * //
 198 qed.
 199
 200 lemma cmove_q2_q3 :
 201   ∀alpha:FinSet.∀sep,a,ls,a0,rs.
 202   step alpha (move_char alpha sep)
 203     (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) =
 204   mk_config alpha (states ? (move_char alpha sep)) 〈3,sep〉
 205     (tape_move_right alpha ls a rs).
 206 #alpha #sep #a #ls #a0 * //
 207 qed.
 208
 209 definition option_hd ≝
 210   λA.λl:list A. match l with
 211   [ nil ⇒ None ?
 212   | cons a _ ⇒ Some ? a ].
 213
 214 definition Rmove_char_true ≝
 215   λalpha,sep,t1,t2.
 216    ∀a,b,ls,rs. b ≠ sep →
 217     t1 = midtape alpha (a::ls) b rs →
 218     t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
 219
 220 definition Rmove_char_false ≝
 221   λalpha,sep,t1,t2.
 222     (current alpha t1 = None alpha → t2 = t1) ∧
 223     (current alpha t1 = Some alpha sep → t2 = t1).
 224
 225 lemma loop_S_true :
 226   ∀A,n,f,p,a.  p a = true →
 227   loop A (S n) f p a = Some ? a. /2/
 228 qed.
 229
 230 lemma loop_S_false :
 231   ∀A,n,f,p,a.  p a = false →
 232   loop A (S n) f p a = loop A n f p (f a).
 233 normalize #A #n #f #p #a #Hpa >Hpa %
 234 qed.
 235
 236 notation < "𝐅" non associative with precedence 90
 237  for @{'bigF}.
 238 notation < "𝐃" non associative with precedence 90
 239  for @{'bigD}.
 240
 241 interpretation "FinSet" 'bigF = (mk_FinSet ???).
 242 interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
 243
 244 lemma trans_init_sep:
 245   ∀alpha,sep,x.
 246   trans ? (move_char alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
 247 #alpha #sep #x normalize >(\b ?) //
 248 qed.
 249
 250 lemma trans_init_not_sep:
 251   ∀alpha,sep,x,y.y == sep = false →
 252   trans ? (move_char alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉.
 253 #alpha #sep #x #y #H1 normalize >H1 //
 254 qed.
 255
 256 lemma sem_move_char :
 257   ∀alpha,sep.
 258   accRealize alpha (move_char alpha sep)
 259     〈3,sep〉 (Rmove_char_true alpha sep) (Rmove_char_false alpha sep).
 260 #alpha #sep *
 261 [@(ex_intro ?? 2)
 262   @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?)))
 263   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 whd % #_ % ]
 264 |#l0 #lt0 @(ex_intro ?? 2)
 265   @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0)))
 266   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 whd % #_ % ]
 267 |#r0 #rt0 @(ex_intro ?? 2)
 268   @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0)))
 269   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 whd % #_ % ]
 270 | #lt #c #rt cases (true_or_false (c == sep)) #Hc
 271   [ @(ex_intro ?? 2)
 272     @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
 273     %
 274     [%
 275       [ >(\P Hc) >loop_S_false //
 276        >loop_S_true
 277        [ @eq_f whd in ⊢ (??%?); >trans_init_sep %
 278        |>(\P Hc) whd in ⊢(??(???(???%))?);
 279          >trans_init_sep % ]
 280      | #Hfalse destruct
 281      ]
 282     |#_ % #_ % ]
 283   | @(ex_intro ?? 4)
 284     cases lt
 285     [ @ex_intro
 286       [|%
 287         [ %
 288           [ >loop_S_false //
 289             >cmove_q0_q1 //
 290           | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 291           ]
 292         | normalize in ⊢ (%→?); #_ %
 293           [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 294           | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 295             @False_ind @(absurd ?? (\Pf Hc)) %
 296           ]
 297         ]
 298       ]
 299     | #l0 #lt @ex_intro
 300       [| %
 301        [ %
 302          [ >loop_S_false //
 303            >cmove_q0_q1 //
 304          | #_ #a #b #ls #rs #Hb #Htape
 305            destruct (Htape)
 306            >cmove_q1_q2
 307            >cmove_q2_q3
 308            cases rs normalize //
 309          ]
 310        | normalize in ⊢ (% → ?); * #Hfalse
 311          @False_ind /2/
 312        ]
 313      ]
 314    ]
 315  ]
 316 ]
 317 qed.
 318
 319 definition R_while_cmove :
 320   λalpha,sep,t1,t2.
 321    ∀a,b,ls,rs. b ≠ sep → memb ? sep rs = false →
 322     t1 = midtape alpha (a::ls) b (rs@sep::rs') →
 323     t2 = midtape alpha (a::rev ? rs@b::ls) sep rs'.
 324
 325 (* (*
 326
 327 (* We do not distinuish an input tape *)
 328
 329 record TM (sig:FinSet): Type[1] ≝
 330 { states : FinSet;
 331   trans : states × (option sig) → states × (option (sig × move));
 332   start: states;
 333   halt : states → bool
 334 }.
 335
 336 record config (sig:FinSet) (M:TM sig): Type[0] ≝
 337 { cstate : states sig M;
 338   ctape: tape sig
 339 }.
 340
 341 definition option_hd ≝ λA.λl:list A.
 342   match l with
 343   [nil ⇒ None ?
 344   |cons a _ ⇒ Some ? a
 345   ].
 346
 347 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
 348   match m with
 349   [ None ⇒ t
 350   | Some m1 ⇒
 351     match \snd m1 with
 352     [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
 353     | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
 354     ]
 355   ].
 356
 357 definition step ≝ λsig.λM:TM sig.λc:config sig M.
 358   let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
 359   let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
 360   mk_config ?? news (tape_move sig (ctape ?? c) mv).
 361
 362 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 363   match n with
 364   [ O ⇒ None ?
 365   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 366   ].
 367
 368 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
 369   loop A k1 f p a1 = Some ? a2 →
 370     loop A (k2+k1) f p a1 = Some ? a2.
 371 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
 372 [normalize #a0 #Hfalse destruct
 373 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
 374  cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
 375 ]
 376 qed.
 377
 378 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 379  ∀k1,k2,a1,a2,a3,a4.
 380    loop A k1 f p a1 = Some ? a2 →
 381      f a2 = a3 → q a2 = false →
 382        loop A k2 f q a3 = Some ? a4 →
 383          loop A (k1+k2) f q a1 = Some ? a4.
 384 #Sig #f #p #q #Hpq #k1 elim k1
 385   [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
 386   |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
 387    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 388    [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
 389     whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
 390     whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
 391    |normalize >(Hpq … pa1) normalize
 392     #H1 #H2 #H3 @(Hind … H2) //
 393    ]
 394  ]
 395 qed.
 396
 397 (*
 398 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 399  ∀k1,k2,a1,a2,a3.
 400    loop A k1 f p a1 = Some ? a2 →
 401      loop A k2 f q a2 = Some ? a3 →
 402        loop A (k1+k2) f q a1 = Some ? a3.
 403 #Sig #f #p #q #Hpq #k1 elim k1
 404   [normalize #k2 #a1 #a2 #a3 #H destruct
 405   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
 406    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 407    [#eqa1a2 destruct #H @loop_incr //
 408    |normalize >(Hpq … pa1) normalize
 409     #H1 #H2 @(Hind … H2) //
 410    ]
 411  ]
 412 qed.
 413 *)
 414
 415 definition initc ≝ λsig.λM:TM sig.λt.
 416   mk_config sig M (start sig M) t.
 417
 418 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 419 ∀t.∃i.∃outc.
 420   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
 421   R t (ctape ?? outc).
 422
 423 (* Compositions *)
 424
 425 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 426 λp. let 〈s,a〉 ≝ p in
 427   match s with
 428   [ inl s1 ⇒
 429       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 430       else
 431       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 432       〈inl … news1,m〉
 433   | inr s2 ⇒
 434       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 435       〈inr … news2,m〉
 436   ].
 437
 438 definition seq ≝ λsig. λM1,M2 : TM sig.
 439   mk_TM sig
 440     (FinSum (states sig M1) (states sig M2))
 441     (seq_trans sig M1 M2)
 442     (inl … (start sig M1))
 443     (λs.match s with
 444       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 445
 446 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 447   ∃am.R1 a1 am ∧ R2 am a2.
 448
 449 (*
 450 definition injectRl ≝ λsig.λM1.λM2.λR.
 451    λc1,c2. ∃c11,c12.
 452      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 453      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 454      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 455      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 456      R c11 c12.
 457
 458 definition injectRr ≝ λsig.λM1.λM2.λR.
 459    λc1,c2. ∃c21,c22.
 460      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 461      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 462      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 463      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 464      R c21 c22.
 465
 466 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 467   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 468   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 469   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 470
 471 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 472
 473 definition lift_confL ≝
 474   λsig,M1,M2,c.match c with
 475   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 476 definition lift_confR ≝
 477   λsig,M1,M2,c.match c with
 478   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 479
 480 definition halt_liftL ≝
 481   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 482   match s with
 483   [ inl s1 ⇒ halt sig M1 s1
 484   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 485
 486 definition halt_liftR ≝
 487   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 488   match s with
 489   [ inl _ ⇒ false
 490   | inr s2 ⇒ halt sig M2 s2 ].
 491
 492 lemma p_halt_liftL : ∀sig,M1,M2,c.
 493   halt sig M1 (cstate … c) =
 494      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 495 #sig #M1 #M2 #c cases c #s #t %
 496 qed.
 497
 498 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 499   halt ? M1 s = false →
 500   trans sig M1 〈s,a〉 = 〈news,move〉 →
 501   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 502 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 503 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 504 qed.
 505
 506 lemma config_eq :
 507   ∀sig,M,c1,c2.
 508   cstate sig M c1 = cstate sig M c2 →
 509   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 510 #sig #M1 * #s1 #t1 * #s2 #t2 //
 511 qed.
 512
 513 lemma step_lift_confL : ∀sig,M1,M2,c0.
 514  halt ? M1 (cstate ?? c0) = false →
 515  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 516  lift_confL sig M1 M2 (step sig M1 c0).
 517 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
 518 #rs #Hhalt
 519 whd in ⊢ (???(????%));whd in ⊢ (???%);
 520 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
 521 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
 522 #s0 #m0 #Heq whd in ⊢ (???%);
 523 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 524 >(trans_liftL … Heq)
 525 [% | //]
 526 qed.
 527
 528 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 529   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 530     loop ? k (step sig (seq sig M1 M2))
 531       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 532     Some ? (lift_confL … c2).
 533 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 534 elim k
 535 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 536 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 537  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 538  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 539  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 540    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 541    | // ]
 542  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 543    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 544     @step_lift_confL //
 545    | // ]
 546 qed.
 547
 548 STOP!
 549
 550 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
 551   loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
 552     loop ? k (step sig (seq sig M1 M2))
 553       (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
 554     Some ? (lift_confR … c2).
 555 #sig #k #M1 #M2 #c1 #c2
 556 elim k
 557 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 558 |#k0 #IH whd in ⊢ (??%? → ??%?);
 559  lapply (refl ? (halt ?? (cstate sig M2 c1)))
 560  cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
 561  [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
 562    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
 563    | (* ... *) ]
 564  | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
 565    [whd in ⊢ (??%? → ??%?); #Hc2 <IH
 566      [@eq_f (* @step_lift_confR // *)
 567      |
 568    | // ]
 569 qed. *)
 570
 571 lemma loop_Some :
 572   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 573 #A #k #f #p #a #b elim k
 574 [normalize #Hfalse destruct
 575 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
 576  [ normalize #H1 destruct
 577
 578 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 579   halt ? M1 s = true →
 580   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 581 #sig #M1 #M2 #s #a
 582 #Hhalt whd in ⊢ (??%?); >Hhalt %
 583 qed.
 584
 585 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
 586   ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
 587 #sig #M1 #M2 #outc cases outc #s #t %
 588 qed.
 589
 590 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
 591   ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
 592 #sig #M1 #M2 #outc cases outc #s #t %
 593 qed.
 594
 595 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 596   Realize sig M1 R1 → Realize sig M2 R2 →
 597     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 598 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 599 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 600 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 601 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 602 %
 603 [@(loop_split ??????????? (loop_liftL … Hloop1))
 604  [* *
 605    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 606    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 607  ||4:cases outc1 #s1 #t1 %
 608  |5:@(loop_liftR … Hloop2)
 609  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 610   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 611   >(trans_liftL_true sig M1 M2 ??)
 612   [ whd in ⊢ (??%?); whd in ⊢ (???%);
 613     @config_eq //
 614   | @(loop_Some ?????? Hloop10) ]
 615  ]
 616 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 617   % //
 618 ]
 619 qed.
 620
 621 (* boolean machines: machines with two distinguished halting states *)
 622
 623
 624
 625 (* old stuff *)
 626 definition empty_tapes ≝ λsig.λn.
 627 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 628 elim n // normalize //
 629 qed.
 630
 631 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 632   mk_config ??
 633     (start sig M)
 634     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 635     [ ].
 636
 637 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 638   halt sig M (state sig M c).
 639
 640 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 641   match n with
 642   [ O ⇒ None ?
 643   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 644   ].
 645
 646 (* Compute ? M f states that f is computed by M *)
 647 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 648 ∀l.∃i.∃c.
 649   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 650   out ?? c = f l.
 651
 652 (* for decision problems, we accept a string if on termination
 653 output is not empty *)
 654
 655 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 656 ∀l.∃i.∃c.
 657   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 658   (isnilb ? (out ?? c) = false).
 659
 660 (* alternative approach.
 661 We define the notion of computation. The notion must be constructive,
 662 since we want to define functions over it, like lenght and size
 663
 664 Perche' serve Type[2] se sposto a e b a destra? *)
 665
 666 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 667   mk_move: p a = false → b = f a → cmove A f p a b.
 668
 669 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 670 | empty : ∀a. cstar A M a a
 671 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 672
 673 definition computation ≝ λsig.λM:TM sig.
 674   cstar ? (cmove ? (step sig M) (stop sig M)).
 675
 676 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 677   ∀l.∃c.computation sig M (init sig M l) c →
 678    (stop sig M c = true) ∧ out ?? c = f l.
 679
 680 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 681   ∀l.∃c.computation sig M (init sig M l) c →
 682    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
 683 *)