matita/matita/lib/turing/universal/compare.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
  13 (* COMPARE BIT
  14
  15 *)
  16
  17 include "turing/while_machine.ma".
  18
  19 (* ADVANCE TO MARK (right)
  20
  21    sposta la testina a destra fino a raggiungere il primo carattere marcato
  22
  23 *)
  24
  25 (* 0, a ≠ mark _ ⇒ 0, R
  26 0, a = mark _ ⇒ 1, N *)
  27
  28 definition atm_states ≝ initN 3.
  29
  30 definition atm0 : initN 3 ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
  31 definition atm1 : initN 3 ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
  32 definition atm2 : initN 3 ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
  33
  34
  35 definition atmr_step ≝
  36   λalpha:FinSet.λtest:alpha→bool.
  37   mk_TM alpha atm_states
  38   (λp.let 〈q,a〉 ≝ p in
  39    match a with
  40    [ None ⇒ 〈atm1, None ?〉
  41    | Some a' ⇒
  42      match test a' with
  43      [ true ⇒ 〈atm1,None ?〉
  44      | false ⇒ 〈atm2,Some ? 〈a',R〉〉 ]])
  45   atm0 (λx.notb (x == atm0)).
  46
  47 definition Ratmr_step_true ≝
  48   λalpha,test,t1,t2.
  49    ∃ls,a,rs.
  50    t1 = midtape alpha ls a rs ∧ test a = false ∧
  51    t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
  52
  53 definition Ratmr_step_false ≝
  54   λalpha,test,t1,t2.
  55     t1 = t2 ∧
  56     (current alpha t1 = None ? ∨
  57      (∃a.current ? t1 = Some ? a ∧ test a = true)).
  58
  59 lemma atmr_q0_q1 :
  60   ∀alpha,test,ls,a0,rs. test a0 = true →
  61   step alpha (atmr_step alpha test)
  62     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  63   mk_config alpha (states ? (atmr_step alpha test)) atm1
  64     (midtape … ls a0 rs).
  65 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  66 whd in match (trans … 〈?,?〉); >Htest %
  67 qed.
  68
  69 lemma atmr_q0_q2 :
  70   ∀alpha,test,ls,a0,rs. test a0 = false →
  71   step alpha (atmr_step alpha test)
  72     (mk_config ?? atm0 (midtape … ls a0 rs)) =
  73   mk_config alpha (states ? (atmr_step alpha test)) atm2
  74     (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
  75 #alpha #test #ls #a0 #ts #Htest whd in ⊢ (??%?);
  76 whd in match (trans … 〈?,?〉); >Htest cases ts //
  77 qed.
  78
  79 lemma sem_atmr_step :
  80   ∀alpha,test.
  81   accRealize alpha (atmr_step alpha test)
  82     atm2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
  83 #alpha #test cut (∀P:Prop.atm1 = atm2 →P) [#P normalize #Hfalse destruct] #Hfalse
  84 *
  85 [ @(ex_intro ?? 2)
  86   @(ex_intro ?? (mk_config ?? atm1 (niltape ?))) %
  87   [ % // @Hfalse | #_ % // % % ]
  88 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (leftof ? a al)))
  89   % [ % // @Hfalse | #_ % // % % ]
  90 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? atm1 (rightof ? a al)))
  91   % [ % // @Hfalse | #_ % // % % ]
  92 | #ls #c #rs @(ex_intro ?? 2)
  93   cases (true_or_false (test c)) #Htest
  94   [ @(ex_intro ?? (mk_config ?? atm1 ?))
  95     [| %
  96       [ %
  97         [ whd in ⊢ (??%?); >atmr_q0_q1 //
  98         | @Hfalse]
  99       | #_ % // %2 @(ex_intro ?? c) % // ]
 100     ]
 101   | @(ex_intro ?? (mk_config ?? atm2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
 102     %
 103     [ %
 104       [ whd in ⊢ (??%?); >atmr_q0_q2 //
 105       | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
 106         % // % //
 107       ]
 108     | #Hfalse @False_ind @(absurd ?? Hfalse) %
 109     ]
 110   ]
 111 ]
 112 qed.
 113
 114 (*
 115 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 116   ∀ls,c,rs.
 117   t1 = mk_tape alpha ls c rs  →
 118   (c = None ? ∧ t2 = t1) ∨
 119   (∃c'.c = Some ? c' ∧
 120     ((test c' = true ∧ t2 = t1) ∨
 121      (test c' = false ∧
 122        (((∀x.memb ? x rs = true → test x = false) ∧
 123          t2 = mk_tape ? (reverse ? rs@c'::ls) (None ?) []) ∨
 124         (∃rs1,b,rs2.rs = rs1@b::rs2 ∧
 125          test b = true ∧ (∀x.memb ? x rs1 = true → test x = false) ∧
 126          t2 = midtape ? (reverse ? rs1@c'::rs) b rs2))))).
 127
 128 definition adv_to_mark_r ≝
 129   λalpha,test.whileTM alpha (atmr_step alpha test) 2.
 130
 131 lemma wsem_adv_to_mark_r :
 132   ∀alpha,test.
 133   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 134 #alpha #test #t #i #outc #Hloop
 135 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 136 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 137 [ #tapea * #Htapea *
 138   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 139     #Hfalse destruct (Hfalse)
 140   | * #a * #Ha #Htest #ls #c #rs cases c
 141     [ #Htapea' % % // >Htapea %
 142     | #c' #Htapea' %2 @(ex_intro ?? c') % //
 143       cases (true_or_false (test c')) #Htestc
 144       [ % % // >Htapea %
 145       | %2 % // generalize in match Htapea'; -Htapea'
 146         cases rs
 147         [ #Htapea' % %
 148           [ normalize #x #Hfalse destruct (Hfalse)
 149           | <Htapea >Htapea' %
 150
 151
 152    #H2 %
 153     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % // <Htapea //
 154   ]
 155 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 156   lapply (IH HRfalse) -IH #IH
 157   #ls #c #rs #Htapea
 158   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 159   >Htapea' in Htapea; #Htapea destruct (Htapea) %2 % //
 160   generalize in match Htapeb; -Htapeb
 161   generalize in match Htapea'; -Htapea'
 162   cases rs
 163   [ #Htapea #Htapeb % %
 164     [ #x0 normalize #Hfalse destruct (Hfalse)
 165     | normalize in Htapeb; cases (IH
 166
 167
 168    [//]
 169    cases (true_or_false (test c))
 170   [ #Htestc %
 171
 172
 173   [ #Htapea %2 % [ %2 // ]
 174     #rs #Htapea %2
 175
 176
 177    *
 178   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 179     cases (IH … Htapeb)
 180     [ * #_ #Houtc >Houtc >Htapeb %
 181     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 182   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 183     cases (IH … Htapeb)
 184     [ * #Hfalse >(Hmemb …) in Hfalse;
 185       [ #Hft destruct (Hft)
 186       | @memb_hd ]
 187     | * #Htestr1 #H1 >reverse_cons >associative_append
 188       @H1 // #x #Hx @Hmemb @memb_cons //
 189     ]
 190   ]
 191 qed. *)
 192
 193 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
 194   ∀ls,c,rs.
 195   (t1 = midtape alpha ls c rs  →
 196   ((test c = true ∧ t2 = t1) ∨
 197    (test c = false ∧
 198     ∀rs1,b,rs2. rs = rs1@b::rs2 →
 199      test b = true → (∀x.memb ? x rs1 = true → test x = false) →
 200      t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
 201
 202 definition adv_to_mark_r ≝
 203   λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
 204
 205 lemma wsem_adv_to_mark_r :
 206   ∀alpha,test.
 207   WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 208 #alpha #test #t #i #outc #Hloop
 209 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
 210 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 211 [ #tapea * #Htapea *
 212   [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
 213     #Hfalse destruct (Hfalse)
 214   | * #a * #Ha #Htest #ls #c #rs #H2 %
 215     >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
 216     <Htapea //
 217   ]
 218 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
 219   lapply (IH HRfalse) -IH #IH
 220   #ls #c #rs #Htapea %2
 221   cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
 222
 223   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
 224   [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
 225     cases (IH … Htapeb)
 226     [ * #_ #Houtc >Houtc >Htapeb %
 227     | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
 228   | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
 229     cases (IH … Htapeb)
 230     [ * #Hfalse >(Hmemb …) in Hfalse;
 231       [ #Hft destruct (Hft)
 232       | @memb_hd ]
 233     | * #Htestr1 #H1 >reverse_cons >associative_append
 234       @H1 // #x #Hx @Hmemb @memb_cons //
 235     ]
 236   ]
 237 qed.
 238
 239 lemma terminate_adv_to_mark_r :
 240   ∀alpha,test.
 241   ∀t.Terminate alpha (adv_to_mark_r alpha test) t.
 242 #alpha #test #t
 243 @(terminate_while … (sem_atmr_step alpha test))
 244   [ %
 245   | cases t
 246     [ % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 247     |2,3: #a0 #al0 % #t1 * #ls0 * #c0 * #rs0 * * #Hfalse destruct (Hfalse)
 248     | #ls #c #rs generalize in match c; -c generalize in match ls; -ls
 249       elim rs
 250       [#ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 251        #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 252        % #t2 * #ls1 * #c1 * #rs1 * * >Ht1
 253        normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
 254       | #r0 #rs0 #IH #ls #c % #t1 * #ls0 * #c0 * #rs0 * *
 255         #H1 destruct (H1) #Hc0 #Ht1 normalize in Ht1;
 256         >Ht1 @IH
 257       ]
 258     ]
 259   ]
 260 qed.
 261
 262 lemma sem_adv_to_mark_r :
 263   ∀alpha,test.
 264   Realize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
 265 /2/
 266 qed.
 267
 268 (*
 269    q0 _ → q1, R
 270    q1 〈a,false〉 → qF, 〈a,true〉, N
 271    q1 〈a,true〉 → qF, _ , N
 272    qF _ → None ?
 273  *)
 274
 275 definition mark_states ≝ initN 3.
 276
 277 definition mark0 : initN 3 ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 278 definition mark1 : initN 3 ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 279 definition mark2 : initN 3 ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 280
 281 definition mark ≝
 282   λalpha:FinSet.mk_TM (FinProd … alpha FinBool) mark_states
 283   (λp.let 〈q,a〉 ≝ p in
 284     match a with
 285     [ None ⇒ 〈mark2,None ?〉
 286     | Some a' ⇒ match pi1 … q with
 287       [ O ⇒ 〈mark1,Some ? 〈a',R〉〉
 288       | S q ⇒ match q with
 289         [ O ⇒ let 〈a'',b〉 ≝ a' in
 290               〈mark2,Some ? 〈〈a'',true〉,N〉〉
 291         | S _ ⇒ 〈mark2,None ?〉 ] ] ])
 292   mark0 (λq.q == mark2).
 293
 294 definition R_mark ≝ λalpha,t1,t2.
 295   ∀ls,c,d,b,rs.
 296   t1 = midtape (FinProd … alpha FinBool) ls c (〈d,b〉::rs) →
 297   t2 = midtape ? (c::ls) 〈d,true〉 rs.
 298
 299 (*lemma mark_q0_q1 :
 300   ∀alpha,ls,c,rs.
 301   step alpha (mark alpha)
 302     (mk_config ?? 0 (midtape … ls c rs)) =
 303   mk_config alpha (states ? (mark alpha)) 1
 304     (midtape … (ls a0 rs).*)
 305
 306 lemma sem_mark :
 307   ∀alpha.Realize ? (mark alpha) (R_mark alpha).
 308 #alpha #intape @(ex_intro ?? 3) cases intape
 309 [ @ex_intro
 310   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 311 |#a #al @ex_intro
 312   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 313 |#a #al @ex_intro
 314   [| % [ % | #ls #c #d #b #rs #Hfalse destruct ] ]
 315 | #ls #c *
 316   [ @ex_intro [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #Hfalse destruct ] ]
 317   | * #d #b #rs @ex_intro
 318     [| % [ % | #ls0 #c0 #d0 #b0 #rs0 #H1 destruct (H1) % ] ] ] ]
 319 qed.
 320
 321 include "turing/if_machine.ma".
 322
 323 (* TEST CHAR
 324
 325    stato finale diverso a seconda che il carattere
 326    corrente soddisfi un test booleano oppure no
 327
 328    q1 = true or no current char
 329    q2 = false
 330 *)
 331
 332 definition tc_states ≝ initN 3.
 333
 334 definition tc0 : initN 3 ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
 335 definition tc1 : initN 3 ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
 336 definition atm2 : initN 3 ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 337
 338 definition test_char ≝
 339   λalpha:FinSet.λtest:alpha→bool.
 340   mk_TM alpha tc_states
 341   (λp.let 〈q,a〉 ≝ p in
 342    match a with
 343    [ None ⇒ 〈1, None ?〉
 344    | Some a' ⇒
 345      match test a' with
 346      [ true ⇒ 〈1,None ?〉
 347      | false ⇒ 〈2,None ?〉 ]])
 348   O (λx.notb (x == 0)).
 349
 350 definition Rtc_true ≝
 351   λalpha,test,t1,t2.
 352    ∀c. current alpha t1 = Some ? c →
 353    test c = true ∧ t2 = t1.
 354
 355 definition Rtc_false ≝
 356   λalpha,test,t1,t2.
 357     ∀c. current alpha t1 = Some ? c →
 358     test c = false ∧ t2 = t1.
 359
 360 lemma tc_q0_q1 :
 361   ∀alpha,test,ls,a0,rs. test a0 = true →
 362   step alpha (test_char alpha test)
 363     (mk_config ?? 0 (midtape … ls a0 rs)) =
 364   mk_config alpha (states ? (test_char alpha test)) 1
 365     (midtape … ls a0 rs).
 366 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
 367 qed.
 368
 369 lemma tc_q0_q2 :
 370   ∀alpha,test,ls,a0,rs. test a0 = false →
 371   step alpha (test_char alpha test)
 372     (mk_config ?? 0 (midtape … ls a0 rs)) =
 373   mk_config alpha (states ? (test_char alpha test)) 2
 374     (midtape … ls a0 rs).
 375 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
 376 qed.
 377
 378 lemma sem_test_char :
 379   ∀alpha,test.
 380   accRealize alpha (test_char alpha test)
 381     1 (Rtc_true alpha test) (Rtc_false alpha test).
 382 #alpha #test *
 383 [ @(ex_intro ?? 2)
 384   @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
 385   [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 386 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
 387   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 388 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
 389   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
 390 | #ls #c #rs @(ex_intro ?? 2)
 391   cases (true_or_false (test c)) #Htest
 392   [ @(ex_intro ?? (mk_config ?? 1 ?))
 393     [| %
 394       [ %
 395         [ whd in ⊢ (??%?); >tc_q0_q1 //
 396         | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
 397       | * #Hfalse @False_ind @Hfalse % ]
 398     ]
 399   | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
 400     %
 401     [ %
 402       [ whd in ⊢ (??%?); >tc_q0_q2 //
 403       | #Hfalse destruct (Hfalse) ]
 404     | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
 405     ]
 406   ]
 407 ]
 408 qed.
 409
 410 axiom myalpha : FinSet.
 411 axiom is_bar : FinProd … myalpha FinBool → bool.
 412 axiom is_grid : FinProd … myalpha FinBool → bool.
 413 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
 414 axiom bar : FinProd … myalpha FinBool.
 415 axiom grid : FinProd … myalpha FinBool.
 416
 417 definition mark_next_tuple ≝
 418   seq ? (adv_to_mark_r ? bar_or_grid)
 419      (ifTM ? (test_char ? is_bar)
 420        (mark ?) (nop ?) 1).
 421
 422 definition R_mark_next_tuple ≝
 423   λt1,t2.
 424     ∀ls,c,rs1,rs2.
 425     (* c non può essere un separatore ... speriamo *)
 426     t1 = midtape ? ls c (rs1@grid::rs2) →
 427     memb ? grid rs1 = false → bar_or_grid c = false →
 428     (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
 429       memb ? bar rs3 = false ∧
 430       Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
 431       t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
 432     ∨
 433     (memb ? bar rs1 = false ∧
 434      t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
 435
 436 axiom tech_split :
 437   ∀A:DeqSet.∀f,l.
 438    (∀x.memb A x l = true → f x = false) ∨
 439    (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
 440 (*#A #f #l elim l
 441 [ % #x normalize #Hfalse *)
 442
 443 theorem sem_mark_next_tuple :
 444   Realize ? mark_next_tuple R_mark_next_tuple.
 445 #intape
 446 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
 447          (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
 448 [@sem_if //
 449 | //
 450 |||#Hif cases (Hif intape) -Hif
 451    #j * #outc * #Hloop * #ta * #Hleft #Hright
 452    @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
 453    -Hloop
 454    #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
 455    cases (Hleft … Hrs)
 456    [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
 457    | * #_ #Hta cases (tech_split ? is_bar rs1)
 458      [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
 459        [ (* Hrs1, H1 *) @daemon
 460        | (* bar_or_grid grid = true *) @daemon
 461        | -Hta #Hta cases Hright
 462          [ * #tb * whd in ⊢ (%→?); #Hcurrent
 463            @False_ind cases(Hcurrent grid ?)
 464            [ #Hfalse (* grid is not a bar *) @daemon
 465            | >Hta % ]
 466          | * #tb * whd in ⊢ (%→?); #Hcurrent
 467            cases (Hcurrent grid ?)
 468            [  #_ #Htb whd in ⊢ (%→?); #Houtc
 469              %2 %
 470              [ (* H1 *) @daemon
 471              | >Houtc >Htb >Hta % ]
 472            | >Hta % ]
 473          ]
 474        ]
 475     | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
 476       % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
 477      lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
 478      [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
 479      | (* bar → bar_or_grid *) @daemon
 480      | >Hsplit >associative_append % ] -Hta #Hta
 481        cases Hright
 482        [ * #tb * whd in ⊢ (%→?); #Hta'
 483          whd in ⊢ (%→?); #Htb
 484          cases (Hta' c0 ?)
 485          [ #_ #Htb' >Htb' in Htb; #Htb
 486            generalize in match Hsplit; -Hsplit
 487            cases rs4 in Hta;
 488            [ >(eq_pair_fst_snd … grid)
 489              #Hta #Hsplit >(Htb … Hta)
 490              >(?:c0 = bar)
 491              [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
 492                % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
 493                      | (* Hc0 *) @daemon ]
 494            | #r5 #rs5 >(eq_pair_fst_snd … r5)
 495              #Hta #Hsplit >(Htb … Hta)
 496              >(?:c0 = bar)
 497              [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
 498                % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
 499                      | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
 500              | * #tb * whd in ⊢ (%→?); #Hta'
 501                whd in ⊢ (%→?); #Htb
 502                cases (Hta' c0 ?)
 503                [ #Hfalse @False_ind >Hfalse in Hc0;
 504                  #Hc0 destruct (Hc0)
 505                | >Hta % ]
 506 ]]]]
 507 qed.