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     left ? t1 ≠ [] → current alpha t1 ≠ None alpha →
 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 #H2 @False_ind @(absurd ?? H2) %]
 264 |#l0 #lt0 @(ex_intro ?? 2)
 265   @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0)))
 266   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
 267 |#r0 #rt0 @(ex_intro ?? 2)
 268   @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0)))
 269   % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
 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     |#_ #H1 #H2 % // normalize >(\P Hc) % ]
 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 ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) %
 293         ]
 294       ]
 295     | #l0 #lt @ex_intro
 296       [| %
 297        [ %
 298          [ >loop_S_false //
 299            >cmove_q0_q1 //
 300          | #_ #a #b #ls #rs #Hb #Htape
 301            destruct (Htape)
 302            >cmove_q1_q2
 303            >cmove_q2_q3
 304            cases rs normalize //
 305          ]
 306        | normalize in ⊢ (% → ?); * #Hfalse
 307          @False_ind /2/
 308        ]
 309      ]
 310    ]
 311  ]
 312 ]
 313 qed.
 314
 315 definition R_while_cmove ≝
 316   λalpha,sep,t1,t2.
 317    ∀a,b,ls,rs,rs'. b ≠ sep → memb ? sep rs = false →
 318     t1 = midtape alpha (a::ls) b (rs@sep::rs') →
 319     t2 = midtape alpha (a::reverse ? rs@b::ls) sep rs'.
 320
 321 lemma star_cases :
 322   ∀A,R,x,y.star A R x y → x = y ∨ ∃z.R x z ∧ star A R z y.
 323 #A #R #x #y #Hstar elim Hstar
 324 [ #b #c #Hleft #Hright *
 325   [ #H1 %2 @(ex_intro ?? c) % //
 326   | * #x0 * #H1 #H2 %2 @(ex_intro ?? x0) % /2/ ]
 327 | /2/ ]
 328 qed.
 329
 330 axiom star_ind_r :
 331   ∀A:Type[0].∀R:relation A.∀Q:A → A → Prop.
 332   (∀a.Q a a) →
 333   (∀a,b,c.R a b → star A R b c → Q b c → Q a c) →
 334   ∀x,y.star A R x y → Q x y.
 335 (* #A #R #Q #H1 #H2 #x #y #H0 elim H0
 336 [ #b #c #Hleft #Hright #IH
 337   cases (star_cases ???? Hleft)
 338   [ #Hx @H2 //
 339   | * #z * #H3 #H4 @(H2 … H3) /2/
 340 [
 341 |
 342 generalize in match (λb.H2 x b y); elim H0
 343 [#b #c #Hleft #Hright #H2' #H3 @H3
 344  @(H3 b)
 345  elim H0
 346 [ #b #c #Hleft #Hright #IH //
 347 | *)
 348
 349 lemma sem_move_char :
 350   ∀alpha,sep.
 351   WRealize alpha (whileTM alpha (move_char alpha sep) 〈3,sep〉)
 352     (R_while_cmove alpha sep).
 353 #alpha #sep #inc #i #outc #Hloop
 354 lapply (sem_while … (sem_move_char alpha sep) inc i outc Hloop) [%]
 355 * #t1 * #Hstar @(star_ind_r ??????? Hstar)
 356 [ #a whd in ⊢ (% → ?); #H1 #a #b #ls #rs #rs' #Hb #Hrs #Hinc
 357   >Hinc in H1; normalize in ⊢ (% → ?); #H1
 358   cases (H1 ??)
 359   [ #Hfalse @False_ind @(absurd ?? Hb) destruct %
 360   |% #H2 destruct (H2)
 361   |% #H2 destruct ]
 362 | #a #b #c #Hstar1 #HRtrue #IH #HRfalse
 363   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
 364   #a0 #b0 #ls #rs #rs' #Hb0 #Hrs #Ha
 365   whd in Hstar1;
 366   lapply (Hstar1 … Hb0 Ha) #Hb
 367   @(IH … Hb0 Hrs) >Hb whd in HRfalse;
 368   [
 369   inc Rtrue* b Rtrue c Rfalse outc
 370
 371 |
 372 ]
 373 qed.
 374
 375    #H1
 376   #a #b #ls #rs #rs #Hb #Hrs #Hinc
 377   >Hinc in H2;whd in ⊢ ((??%? → ?) → ?);
 378
 379 lapply (H inc i outc Hloop) *
 380
 381
 382 (* (*
 383
 384 (* We do not distinuish an input tape *)
 385
 386 record TM (sig:FinSet): Type[1] ≝
 387 { states : FinSet;
 388   trans : states × (option sig) → states × (option (sig × move));
 389   start: states;
 390   halt : states → bool
 391 }.
 392
 393 record config (sig:FinSet) (M:TM sig): Type[0] ≝
 394 { cstate : states sig M;
 395   ctape: tape sig
 396 }.
 397
 398 definition option_hd ≝ λA.λl:list A.
 399   match l with
 400   [nil ⇒ None ?
 401   |cons a _ ⇒ Some ? a
 402   ].
 403
 404 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
 405   match m with
 406   [ None ⇒ t
 407   | Some m1 ⇒
 408     match \snd m1 with
 409     [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
 410     | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
 411     ]
 412   ].
 413
 414 definition step ≝ λsig.λM:TM sig.λc:config sig M.
 415   let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
 416   let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
 417   mk_config ?? news (tape_move sig (ctape ?? c) mv).
 418
 419 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 420   match n with
 421   [ O ⇒ None ?
 422   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 423   ].
 424
 425 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
 426   loop A k1 f p a1 = Some ? a2 →
 427     loop A (k2+k1) f p a1 = Some ? a2.
 428 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
 429 [normalize #a0 #Hfalse destruct
 430 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
 431  cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
 432 ]
 433 qed.
 434
 435 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 436  ∀k1,k2,a1,a2,a3,a4.
 437    loop A k1 f p a1 = Some ? a2 →
 438      f a2 = a3 → q a2 = false →
 439        loop A k2 f q a3 = Some ? a4 →
 440          loop A (k1+k2) f q a1 = Some ? a4.
 441 #Sig #f #p #q #Hpq #k1 elim k1
 442   [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
 443   |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
 444    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 445    [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
 446     whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
 447     whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
 448    |normalize >(Hpq … pa1) normalize
 449     #H1 #H2 #H3 @(Hind … H2) //
 450    ]
 451  ]
 452 qed.
 453
 454 (*
 455 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 456  ∀k1,k2,a1,a2,a3.
 457    loop A k1 f p a1 = Some ? a2 →
 458      loop A k2 f q a2 = Some ? a3 →
 459        loop A (k1+k2) f q a1 = Some ? a3.
 460 #Sig #f #p #q #Hpq #k1 elim k1
 461   [normalize #k2 #a1 #a2 #a3 #H destruct
 462   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
 463    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 464    [#eqa1a2 destruct #H @loop_incr //
 465    |normalize >(Hpq … pa1) normalize
 466     #H1 #H2 @(Hind … H2) //
 467    ]
 468  ]
 469 qed.
 470 *)
 471
 472 definition initc ≝ λsig.λM:TM sig.λt.
 473   mk_config sig M (start sig M) t.
 474
 475 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 476 ∀t.∃i.∃outc.
 477   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
 478   R t (ctape ?? outc).
 479
 480 (* Compositions *)
 481
 482 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 483 λp. let 〈s,a〉 ≝ p in
 484   match s with
 485   [ inl s1 ⇒
 486       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 487       else
 488       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 489       〈inl … news1,m〉
 490   | inr s2 ⇒
 491       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 492       〈inr … news2,m〉
 493   ].
 494
 495 definition seq ≝ λsig. λM1,M2 : TM sig.
 496   mk_TM sig
 497     (FinSum (states sig M1) (states sig M2))
 498     (seq_trans sig M1 M2)
 499     (inl … (start sig M1))
 500     (λs.match s with
 501       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 502
 503 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 504   ∃am.R1 a1 am ∧ R2 am a2.
 505
 506 (*
 507 definition injectRl ≝ λsig.λM1.λM2.λR.
 508    λc1,c2. ∃c11,c12.
 509      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 510      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 511      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 512      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 513      R c11 c12.
 514
 515 definition injectRr ≝ λsig.λM1.λM2.λR.
 516    λc1,c2. ∃c21,c22.
 517      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 518      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 519      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 520      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 521      R c21 c22.
 522
 523 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 524   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 525   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 526   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 527
 528 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 529
 530 definition lift_confL ≝
 531   λsig,M1,M2,c.match c with
 532   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 533 definition lift_confR ≝
 534   λsig,M1,M2,c.match c with
 535   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 536
 537 definition halt_liftL ≝
 538   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 539   match s with
 540   [ inl s1 ⇒ halt sig M1 s1
 541   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 542
 543 definition halt_liftR ≝
 544   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 545   match s with
 546   [ inl _ ⇒ false
 547   | inr s2 ⇒ halt sig M2 s2 ].
 548
 549 lemma p_halt_liftL : ∀sig,M1,M2,c.
 550   halt sig M1 (cstate … c) =
 551      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 552 #sig #M1 #M2 #c cases c #s #t %
 553 qed.
 554
 555 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 556   halt ? M1 s = false →
 557   trans sig M1 〈s,a〉 = 〈news,move〉 →
 558   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 559 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 560 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 561 qed.
 562
 563 lemma config_eq :
 564   ∀sig,M,c1,c2.
 565   cstate sig M c1 = cstate sig M c2 →
 566   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 567 #sig #M1 * #s1 #t1 * #s2 #t2 //
 568 qed.
 569
 570 lemma step_lift_confL : ∀sig,M1,M2,c0.
 571  halt ? M1 (cstate ?? c0) = false →
 572  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 573  lift_confL sig M1 M2 (step sig M1 c0).
 574 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
 575 #rs #Hhalt
 576 whd in ⊢ (???(????%));whd in ⊢ (???%);
 577 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
 578 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
 579 #s0 #m0 #Heq whd in ⊢ (???%);
 580 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 581 >(trans_liftL … Heq)
 582 [% | //]
 583 qed.
 584
 585 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 586   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 587     loop ? k (step sig (seq sig M1 M2))
 588       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 589     Some ? (lift_confL … c2).
 590 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 591 elim k
 592 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 593 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 594  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 595  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 596  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 597    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 598    | // ]
 599  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 600    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 601     @step_lift_confL //
 602    | // ]
 603 qed.
 604
 605 STOP!
 606
 607 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
 608   loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
 609     loop ? k (step sig (seq sig M1 M2))
 610       (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
 611     Some ? (lift_confR … c2).
 612 #sig #k #M1 #M2 #c1 #c2
 613 elim k
 614 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 615 |#k0 #IH whd in ⊢ (??%? → ??%?);
 616  lapply (refl ? (halt ?? (cstate sig M2 c1)))
 617  cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
 618  [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
 619    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
 620    | (* ... *) ]
 621  | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
 622    [whd in ⊢ (??%? → ??%?); #Hc2 <IH
 623      [@eq_f (* @step_lift_confR // *)
 624      |
 625    | // ]
 626 qed. *)
 627
 628 lemma loop_Some :
 629   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 630 #A #k #f #p #a #b elim k
 631 [normalize #Hfalse destruct
 632 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
 633  [ normalize #H1 destruct
 634
 635 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 636   halt ? M1 s = true →
 637   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 638 #sig #M1 #M2 #s #a
 639 #Hhalt whd in ⊢ (??%?); >Hhalt %
 640 qed.
 641
 642 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
 643   ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
 644 #sig #M1 #M2 #outc cases outc #s #t %
 645 qed.
 646
 647 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
 648   ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
 649 #sig #M1 #M2 #outc cases outc #s #t %
 650 qed.
 651
 652 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 653   Realize sig M1 R1 → Realize sig M2 R2 →
 654     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 655 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 656 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 657 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 658 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 659 %
 660 [@(loop_split ??????????? (loop_liftL … Hloop1))
 661  [* *
 662    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 663    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 664  ||4:cases outc1 #s1 #t1 %
 665  |5:@(loop_liftR … Hloop2)
 666  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 667   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 668   >(trans_liftL_true sig M1 M2 ??)
 669   [ whd in ⊢ (??%?); whd in ⊢ (???%);
 670     @config_eq //
 671   | @(loop_Some ?????? Hloop10) ]
 672  ]
 673 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 674   % //
 675 ]
 676 qed.
 677
 678 (* boolean machines: machines with two distinguished halting states *)
 679
 680
 681
 682 (* old stuff *)
 683 definition empty_tapes ≝ λsig.λn.
 684 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 685 elim n // normalize //
 686 qed.
 687
 688 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 689   mk_config ??
 690     (start sig M)
 691     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 692     [ ].
 693
 694 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 695   halt sig M (state sig M c).
 696
 697 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 698   match n with
 699   [ O ⇒ None ?
 700   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 701   ].
 702
 703 (* Compute ? M f states that f is computed by M *)
 704 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 705 ∀l.∃i.∃c.
 706   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 707   out ?? c = f l.
 708
 709 (* for decision problems, we accept a string if on termination
 710 output is not empty *)
 711
 712 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 713 ∀l.∃i.∃c.
 714   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 715   (isnilb ? (out ?? c) = false).
 716
 717 (* alternative approach.
 718 We define the notion of computation. The notion must be constructive,
 719 since we want to define functions over it, like lenght and size
 720
 721 Perche' serve Type[2] se sposto a e b a destra? *)
 722
 723 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 724   mk_move: p a = false → b = f a → cmove A f p a b.
 725
 726 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 727 | empty : ∀a. cstar A M a a
 728 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 729
 730 definition computation ≝ λsig.λM:TM sig.
 731   cstar ? (cmove ? (step sig M) (stop sig M)).
 732
 733 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 734   ∀l.∃c.computation sig M (init sig M l) c →
 735    (stop sig M c = true) ∧ out ?? c = f l.
 736
 737 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 738   ∀l.∃c.computation sig M (init sig M l) c →
 739    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
 740 *)