matita/matita/lib/turing/multi_universal/binaryTM.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "turing/mono.ma".
  16
  17 (* given a FinSet F:
  18    - get its cardinality
  19    - return its nth element
  20    - return the index of a given element
  21  *)
  22 axiom FS_crd : FinSet → nat.
  23 axiom FS_nth : ∀F:FinSet.nat → option F.
  24 axiom index_of_FS : ∀F:FinSet.F → nat.
  25
  26 (* unary bit representation (with a given length) of a certain number *)
  27 axiom unary_of_nat : nat → nat → (list bool).
  28
  29 axiom FinVector : Type[0] → nat → FinSet.
  30
  31 definition binary_base_states ≝ initN 6.
  32
  33 definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 6 (refl …)).
  34 definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 6 (refl …)).
  35 definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 6 (refl …)).
  36 definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 6 (refl …)).
  37 definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 6 (refl …)).
  38 definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 6 (refl …)).
  39
  40 definition states_binaryTM : FinSet → FinSet → FinSet ≝ λsig,states.
  41  FinProd (FinProd states binary_base_states)
  42          (FinProd (FinOption sig) (initN (S (S (2 * (FS_crd sig)))))).
  43
  44 axiom daemon : ∀T:Type[0].T.
  45
  46 definition to_initN : ∀n,m.n < m → initN m ≝ λn,m,Hn.mk_Sig … n ….// qed.
  47
  48 definition initN_pred : ∀n.∀m:initN n.initN n ≝ λn,m.mk_Sig … (pred (pi1 … m)) ….
  49 cases m #m0 /2 by le_to_lt_to_lt/ qed.
  50
  51 definition displ_of_move ≝ λsig,mv.
  52   match mv with
  53   [ L ⇒ 2*FS_crd sig
  54   | N ⇒ FS_crd sig
  55   | R ⇒ O ].
  56
  57 lemma le_displ_of_move : ∀sig,mv.displ_of_move sig mv ≤ S (2*FS_crd sig).
  58 #sig * /2 by le_S/
  59 qed.
  60
  61 (* controllare i contatori, molti andranno incrementati di uno *)
  62 definition trans_binaryTM : ∀sig,states:FinSet.
  63   (states × (option sig) → states × (option sig) × move) →
  64   ((states_binaryTM sig states) × (option bool) →
  65    (states_binaryTM sig states) × (option bool) × move)
  66 ≝ λsig,states,trans,p.
  67   let 〈s,a〉 ≝ p in
  68   let 〈s0,phase,ch,count〉 ≝ s in
  69   let (H1 : O < S (S (2*FS_crd sig))) ≝ ? in
  70   let (H2 : FS_crd sig < S (S (2*FS_crd sig))) ≝ ? in
  71   match pi1 … phase with
  72   [ O ⇒ (*** PHASE 0: read ***)
  73       match pi1 … count with
  74       [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
  75       | S k ⇒ match a with
  76         [ Some a0 ⇒ if (a0 == true)
  77                     then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
  78                     else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉
  79         | None ⇒ (* Overflow position! *)
  80           let 〈s',a',mv〉 ≝ trans 〈s0,None ?〉 in
  81           match a' with
  82           [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,bin2,None ?,to_initN 0 ? H1〉,None ?,N〉
  83           | Some _ ⇒ (* maybe extend tape *) 〈〈s0,bin4,None ?,to_initN O ? H1〉,None ?,R〉 ] ] ]
  84   | S phase ⇒ match phase with
  85   [ O ⇒ (*** PHASE 1: restart ***)
  86       match pi1 … count with
  87       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
  88       | S k ⇒ 〈〈s0,bin1,ch,initN_pred … count〉,None ?,L〉 ]
  89   | S phase ⇒ match phase with
  90   [ O ⇒ (*** PHASE 2: write ***)
  91       let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
  92       match pi1 … count with
  93       [ O ⇒ 〈〈s',bin3,ch,to_initN (displ_of_move sig mv) ??〉,None ?,N〉
  94       | S k ⇒ match a' with
  95          [ None ⇒ 〈〈s0,bin2,ch,initN_pred … count〉,None ?,R〉
  96          | Some a0' ⇒ let out ≝ (FS_nth ? k == a') in
  97                       〈〈s0,bin2,ch,initN_pred … count〉,Some ? out,R〉 ]
  98       ]
  99   | S phase ⇒ match phase with
 100   [ O ⇒ (*** PHASE 3: move head left ***)
 101       match pi1 … count with
 102       [ O ⇒ 〈〈s0,bin0,None ?,to_initN (FS_crd sig) ? H2〉, None ?,N〉 (* the end: restart *)
 103       | S k ⇒ 〈〈s0,bin3,ch,initN_pred … count〉, None ?,L〉 ]
 104   | S phase ⇒ match phase with
 105   [ O ⇒ (*** PHASE 4: check position ***)
 106       match a with
 107       [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
 108       | Some _ ⇒ (* leftof *)
 109         let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
 110         match a' with
 111         [ None ⇒ (* (vacuous) go to end of 2 *) 〈〈s0,bin2,ch,to_initN 0 ? H1〉,None ?,N〉
 112         | Some _ ⇒ (* extend tape *) 〈〈s0,bin5,ch,to_initN (FS_crd sig) ? H2〉,None ?,L〉 ]
 113       ]
 114   | S _ ⇒ (*** PHASE 5: left extension ***)
 115       match pi1 … count with
 116       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,R〉
 117       | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]].
 118 [2,3: /2 by lt_S_to_lt/] /2 by le_S_S/
 119 qed.
 120
 121 definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝
 122   λsig,M,s.let 〈s0,phase,ch,count〉 ≝ s in
 123   pi1 … phase == O ∧ halt sig M s0.
 124
 125 (*
 126  * Una mk_binaryTM prende in input una macchina M e produce una macchina che:
 127  * - ha per alfabeto FinBool
 128  * - ha stati di tipo ((states … M) × (initN 7)) ×
 129        ((option sig) × (initN (2*dimensione dell'alfabeto di M + 1))
 130  *   dove il primo elemento corrisponde allo stato della macchina input,
 131  *   il secondo identifica la fase (lettura, scrittura, spostamento)
 132  *   il terzo identifica il carattere oggetto letto
 133  *   il quarto è un contatore
 134  * - la funzione di transizione viene prodotta da trans_binaryTM
 135  * - la funzione di arresto viene prodotta da halt_binaryTM
 136  *)
 137 definition mk_binaryTM ≝
 138   λsig.λM:TM sig.
 139   mk_TM FinBool (states_binaryTM sig (states sig M))
 140     (trans_binaryTM sig (states sig M) (trans sig M))
 141     (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).
 142 /2 by lt_S_to_lt/ qed.
 143
 144 definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
 145
 146 definition opt_bin_char ≝ λsig,c.match c with
 147 [ None ⇒ [ ] | Some c0 ⇒ bin_char sig c0 ].
 148
 149 definition bin_list ≝ λsig,l.flatten ? (map ?? (bin_char sig) l).
 150 definition rev_bin_list ≝ λsig,l.flatten ? (map ?? (λc.reverse ? (bin_char sig c)) l).
 151
 152 definition tape_bin_lift ≝ λsig,t.
 153 let ls' ≝ rev_bin_list ? (left ? t) in
 154 let c' ≝ option_hd ? (opt_bin_char sig (current ? t)) in
 155 let rs' ≝ (tail ? (opt_bin_char sig (current ? t))@bin_list ? (right ? t)) in
 156  mk_tape ? ls' c' rs'.
 157
 158 definition R_bin_lift ≝ λsig,R,t1,t2.
 159   ∃u1.t1 = tape_bin_lift sig u1 →
 160   ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2.
 161
 162 definition state_bin_lift :
 163   ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M)
 164  ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉./2 by lt_S_to_lt/ qed.
 165
 166 lemma lift_halt_binaryTM :
 167   ∀sig,M,q.halt sig M q = halt ? (mk_binaryTM sig M) (state_bin_lift ? M q).
 168 // qed.
 169
 170 lemma binaryTM_bin0_bin1 :
 171   ∀sig,M,t,q,ch.
 172   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,O〉) t)
 173   = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. //
 174 qed.
 175
 176 lemma binaryTM_bin0_bin2 :
 177   ∀sig,M,t,q,ch,k,qn,mv.
 178   current ? t = None ? → S k <S (2*FS_crd sig) →
 179   〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 →
 180   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 181   = mk_config ?? (〈q,bin2,None ?,to_initN O ??〉) t. [2,3:/2 by transitive_lt/]
 182 #sig #M #t #q #ch #k #qn #mv #Hcur #Hk #Htrans
 183 whd in match (step ???); whd in match (trans ???);
 184 >Hcur <Htrans %
 185 qed.
 186
 187 lemma binaryTM_bin0_bin4 :
 188   ∀sig,M,t,q,ch,k,qn,chn,mv.
 189   current ? t = None ? → S k <S (2*FS_crd sig) →
 190   〈qn,Some ? chn,mv〉 = trans sig M 〈q,None ?〉 →
 191   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 192   = mk_config ?? (〈q,bin4,None ?,to_initN 0 ??〉) (tape_move ? t R). [2,3:/2 by transitive_lt/]
 193 #sig #M #t #q #ch #k #qn #chn #mv #Hcur #Hk #Htrans
 194 whd in match (step ???); whd in match (trans ???);
 195 >Hcur <Htrans %
 196 qed.
 197
 198 lemma binaryTM_bin0_true :
 199   ∀sig,M,t,q,ch,k.
 200   current ? t = Some ? true → S k <S (2*FS_crd sig) →
 201   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 202   = mk_config ?? (〈q,bin0,FS_nth sig k,to_initN k ??〉) (tape_move ? t R).[2,3:@le_S /2 by lt_S_to_lt/]
 203 #sig #M #t #q #ch #k #Hcur #Hk
 204 whd in match (step ???); whd in match (trans ???);
 205 >Hcur %
 206 qed.
 207
 208 lemma binaryTM_bin0_false :
 209   ∀sig,M,t,q,ch,k.
 210   current ? t = Some ? false → S k <S (2*FS_crd sig) →
 211   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 212   = mk_config ?? (〈q,bin0,ch,to_initN k ??〉) (tape_move ? t R).[2,3:@le_S /2 by lt_S_to_lt/]
 213 #sig #M #t #q #ch #k #Hcur #Hk
 214 whd in match (step ???); whd in match (trans ???);
 215 >Hcur %
 216 qed.
 217
 218 (* to be checked *)
 219 axiom binary_to_bin_char :∀sig,csl,csr,a.
 220   csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
 221
 222 lemma binaryTM_phase0_midtape_aux :
 223   ∀sig,M,q,ls,a,rs,k.
 224   halt sig M q=false →
 225   ∀csr,csl,t,ch.length ? csr < S (2*FS_crd sig) →
 226   t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) →
 227   csl@csr = bin_char sig a →
 228   |csl@csr| = FS_crd sig →
 229   (index_of_FS ? a < |csl| → ch = Some ? a) →
 230   loopM ? (mk_binaryTM sig M) (S (length ? csr) + k)
 231     (mk_config ?? (〈q,bin0,ch,length ? csr〉) t)
 232   = loopM ? (mk_binaryTM sig M) k
 233       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
 234         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3:@le_S /2 by O/]
 235 #sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
 236 [ #csl #t #ch #Hlen #Ht >append_nil #Hcsl #Hlencsl #Hch >loopM_unfold >loop_S_false [|normalize //]
 237   >Hch [| >Hlencsl (* lemmatize *) @daemon]
 238   <loopM_unfold @eq_f >binaryTM_bin0_bin1 @eq_f >Ht
 239   whd in match (step ???); whd in match (trans ???); <Hcsl %
 240 | #c cases c
 241   [ #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
 242     <loopM_unfold lapply (binary_to_bin_char … Heq) #Ha >binaryTM_bin0_true
 243     [| >Ht % ]
 244     lapply (IH (csl@[true]) (tape_move FinBool t R) ??????)
 245     [ //
 246     | >associative_append @Hcrd
 247     | >associative_append @Heq
 248     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
 249       cases csr0
 250       [ cases rs
 251         [ normalize >rev_append_def >rev_append_def >reverse_append %
 252         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 253       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 254     | /2 by lt_S_to_lt/
 255     |]
 256     #H whd in match (plus ??); >H @eq_f @eq_f2 %
 257   | #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
 258     <loopM_unfold >binaryTM_bin0_false [| >Ht % ]
 259     lapply (IH (csl@[false]) (tape_move FinBool t R) ??????)
 260     [6: @ch
 261     | (* by cases: if index < |csl|, then Hch, else False *)
 262        @daemon
 263     | >associative_append @Hcrd
 264     | >associative_append @Heq
 265     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
 266       cases csr0
 267       [ cases rs
 268         [ normalize >rev_append_def >rev_append_def >reverse_append %
 269         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 270       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 271     | /2 by lt_S_to_lt/
 272     |]
 273     #H whd in match (plus ??); >H @eq_f @eq_f2 %
 274   ]
 275 ]
 276 qed.
 277
 278 lemma le_to_eq : ∀m,n.m ≤ n → ∃k. n = m + k. /3 by plus_minus, ex_intro/
 279 qed.
 280
 281 lemma minus_tech : ∀a,b.a + b - a = b. // qed.
 282
 283 lemma binaryTM_phase0_midtape :
 284   ∀sig,M,t,q,ls,a,rs,ch,k.
 285   halt sig M q=false → S (FS_crd sig) ≤ k →
 286   t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a)@rs) →
 287   loopM ? (mk_binaryTM sig M) k
 288     (mk_config ?? (〈q,bin0,ch,FS_crd sig〉) t)
 289   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 290       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
 291         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [|*:@le_S //]
 292 #sig #M #t #q #ls #a #rs #ch #k #Hhalt #Hk #Ht
 293 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 294 cut (∃c,cl.bin_char sig a = c::cl) [@daemon] * #c * #cl #Ha >Ha
 295 cut (FS_crd sig = |bin_char sig a|) [@daemon] #Hlen
 296 @(trans_eq ?? (loopM ? (mk_binaryTM ? M) (S (|c::cl|) + k0)
 297    (mk_config ?? 〈q,bin0,〈ch,|c::cl|〉〉 t)))
 298 [ /2 by O/ | @eq_f2 // @eq_f2 // @eq_f <Ha >Hlen % ]
 299 >(binaryTM_phase0_midtape_aux ? M q ls a rs ? ? (c::cl) [ ] t ch) //
 300 [| normalize #Hfalse @False_ind cases (not_le_Sn_O ?) /2/
 301 | <Ha (* |bin_char sig ?| = FS_crd sig *) @daemon
 302 | >Ha %
 303 | >Ht >Ha %
 304 | <Ha <Hlen // ]
 305 <Ha %
 306 qed.
 307
 308 lemma binaryTM_phase0_None_None :
 309   ∀sig,M,t,q,ch,k,n,qn,mv.
 310   O < n →  n < 2*FS_crd sig → O < k →
 311   halt sig M q=false →
 312   current ? t = None ? →
 313   〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 →
 314   loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t)
 315   = loopM ? (mk_binaryTM sig M) (k-1)
 316       (mk_config ?? (〈q,bin2,None ?,to_initN O ??〉) t). [2,3: /2 by transitive_lt/ ]
 317 #sig #M #t #q #ch #k #n #qn #mv #HOn #Hn #Hk #Hhalt
 318 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 319 cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0)
 320 cases t
 321 [ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/
 322 | #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/
 323 | #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/
 324 | #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 325 qed.
 326
 327 lemma binaryTM_phase0_None_Some :
 328   ∀sig,M,t,q,ch,k,n,qn,chn,mv.
 329   O < n →  n < 2*FS_crd sig → O < k →
 330   halt sig M q=false →
 331   current ? t = None ? →
 332   〈qn,Some ? chn,mv〉 = trans sig M 〈q,None ?〉 →
 333   loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t)
 334   = loopM ? (mk_binaryTM sig M) (k-1)
 335       (mk_config ?? (〈q,bin4,None ?,to_initN O ??〉) (tape_move ? t R)). [2,3: /2 by transitive_lt/ ]
 336 #sig #M #t #q #ch #k #n #qn #chn #mv #HOn #Hn #Hk #Hhalt
 337 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 338 cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0)
 339 cases t
 340 [ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
 341 | #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
 342 | #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
 343 | #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 344 qed.
 345
 346 lemma binaryTM_bin1_O :
 347   ∀sig,M,t,q,ch.
 348   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,O〉) t)
 349   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3:/2 by lt_S_to_lt/]
 350 #sig #M #t #q #ch %
 351 qed.
 352
 353 lemma binaryTM_bin1_S :
 354   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 355   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,S k〉) t)
 356   = mk_config ?? (〈q,bin1,ch,to_initN k ??〉) (tape_move ? t L). [2,3:@le_S /2 by lt_S_to_lt/]
 357 #sig #M #t #q #ch #k #HSk %
 358 qed.
 359
 360 lemma binaryTM_phase1 :
 361   ∀sig,M,q,ls1,ls2,cur,rs,ch,k.
 362   S (FS_crd sig) ≤ k → |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) →
 363   loopM ? (mk_binaryTM sig M) k
 364     (mk_config ?? (〈q,bin1,ch,FS_crd sig〉) (mk_tape ? (ls1@ls2) cur rs))
 365   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 366       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 367         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 368           (tail ? (reverse ? ls1@option_cons ? cur rs)))). [2,3:/2 by O/]
 369 cut (∀sig,M,q,ls1,ls2,ch,k,n,cur,rs.
 370   |ls1| = n →  n<S (2*FS_crd sig) → (cur = None ? → rs = [ ]) →
 371   loopM ? (mk_binaryTM sig M) (S n + k)
 372     (mk_config ?? (〈q,bin1,ch,n〉) (mk_tape ? (ls1@ls2) cur rs))
 373   = loopM ? (mk_binaryTM sig M) k
 374       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 375         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 376           (tail ? (reverse ? ls1@option_cons ? cur rs))))) [1,2:@le_S //]
 377 [ #sig #M #q #ls1 #ls2 #ch #k elim ls1
 378   [ #n normalize in ⊢ (%→?); #cur #rs #Hn <Hn #Hcrd #Hcur >loopM_unfold >loop_S_false [| % ]
 379     >binaryTM_bin1_O cases cur in Hcur;
 380     [ #H >(H (refl ??)) -H %
 381     | #cur' #_ % ]
 382   | #l0 #ls0 #IH * [ #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 383     #n #cur #rs normalize in ⊢ (%→?); #H destruct (H) #Hlt #Hcur
 384     >loopM_unfold >loop_S_false [|%] >binaryTM_bin1_S
 385     <(?:mk_tape ? (ls0@ls2) (Some ? l0) (option_cons ? cur rs) =
 386         tape_move FinBool (mk_tape FinBool ((l0::ls0)@ls2) cur rs) L)
 387     [| cases cur in Hcur; [ #H >(H ?) // | #cur' #_ % ] ]
 388     >(?:loop (config FinBool (states FinBool (mk_binaryTM sig M))) (S (|ls0|)+k)
 389       (step FinBool (mk_binaryTM sig M))
 390       (λc:config FinBool (states FinBool (mk_binaryTM sig M))
 391        .halt FinBool (mk_binaryTM sig M)
 392        (cstate FinBool (states FinBool (mk_binaryTM sig M)) c))
 393       (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 394        〈q,bin1,ch,to_initN (|ls0|) ?
 395         (le_S ?? (lt_S_to_lt (|ls0|) (S (2*FS_crd sig)) Hlt))〉
 396        (mk_tape FinBool (ls0@ls2) (Some FinBool l0) (option_cons FinBool cur rs)))
 397       = loopM FinBool (mk_binaryTM sig M) k
 398          (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 399           〈q,bin2,〈ch,FS_crd sig〉〉
 400           (mk_tape FinBool ls2
 401            (option_hd FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs))
 402            (tail FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs)))))
 403     [| /2/
 404     | >(?: l0::option_cons ? cur rs = option_cons ? (Some ? l0) (option_cons ? cur rs)) [| % ]
 405       @trans_eq [|| @(IH ??? (refl ??)) [ /2 by lt_S_to_lt/ | #H destruct (H) ] ]
 406       %
 407     ]
 408    >reverse_cons >associative_append %
 409  ]
 410 | #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #k #Hk #Hlen
 411   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @Hcut // ]
 412 qed.
 413
 414 lemma binaryTM_bin2_O :
 415   ∀sig,M,t,q,qn,ch,chn,mv.
 416   〈qn,chn,mv〉 = trans sig M 〈q,ch〉 →
 417   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
 418   = mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉) t.[2,3:/2 by lt_S_to_lt,le_S_S/]
 419 #sig #M #t #q #qn #ch #chn #mv #Htrans
 420 whd in match (step ???); whd in match (trans ???); <Htrans %
 421 qed.
 422
 423 lemma binaryTM_bin2_S_None :
 424   ∀sig,M,t,q,qn,ch,mv,k.
 425   k < S (2*FS_crd sig) →
 426   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 427   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
 428   = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? t R).
 429 [2,3: @le_S_S /2 by lt_to_le/ ]
 430 #sig #M #t #q #qn #ch #mv #k #Hk #Htrans
 431 whd in match (step ???); whd in match (trans ???); <Htrans %
 432 qed.
 433
 434 lemma binaryTM_bin2_S_Some :
 435   ∀sig,M,t,q,qn,ch,chn,mv,k.
 436   k< S (2*FS_crd sig) →
 437   〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 438   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
 439   = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? (tape_write ? t (Some ? (FS_nth ? k == Some ? chn))) R).
 440 [2,3: @le_S_S /2 by lt_to_le/ ]
 441 #sig #M #t #q #qn #ch #chn #mv #k #Hk #Htrans
 442 whd in match (step ???); whd in match (trans ???); <Htrans %
 443 qed.
 444
 445 let rec iter (T:Type[0]) f n (t:T) on n ≝
 446   match n with [ O ⇒ t | S n0 ⇒ iter T f n0 (f t) ].
 447
 448 lemma binaryTM_phase2_None :∀sig,M,q,ch,qn,mv,k,n. S n ≤ k →
 449   ∀t.n≤S (2*FS_crd sig) →
 450   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 451   loopM ? (mk_binaryTM sig M) k
 452     (mk_config ?? (〈q,bin2,ch,n〉) t)
 453   = loopM ? (mk_binaryTM sig M) (k - S n)
 454       (mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉)
 455         (iter ? (λt0.tape_move ? t0 R) n t)). [2,3: @le_S_S /2 by lt_S_to_lt/]
 456 #sig #M #q #ch #qn #mv #k #n #Hk
 457 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 458 elim n
 459 [ #t #Hle #Htrans >loopM_unfold >loop_S_false //
 460   >(binaryTM_bin2_O … Htrans) //
 461 | #n0 #IH #t #Hn0 #Htrans >loopM_unfold >loop_S_false //
 462   >(binaryTM_bin2_S_None … Htrans) @(trans_eq ???? (IH …)) //
 463 ]
 464 qed.
 465
 466 lemma binaryTM_phase2_Some_of : ∀sig,M,q,ch,qn,chn,mv,ls,k.
 467   S (FS_crd sig) ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 468   loopM ? (mk_binaryTM sig M) k
 469     (mk_config ?? (〈q,bin2,ch,FS_crd sig〉) (mk_tape ? ls (None ?) [ ]))
 470   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 471       (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 472         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (None ?) [ ])). [2,3:@le_S_S //]
 473 cut (∀sig,M,q,ch,qn,chn,mv,ls,k,n.
 474   S n ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 475   ∀csl. n <S (2*FS_crd sig) →
 476   |csl| + n = FS_crd sig →
 477   (∃fs.bin_char sig chn = reverse ? csl@fs) →
 478   loopM ? (mk_binaryTM sig M) k
 479     (mk_config ?? (〈q,bin2,ch,n〉) (mk_tape ? (csl@ls) (None ?) [ ]))
 480   = loopM ? (mk_binaryTM sig M) (k - S n)
 481       (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 482         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (None ?) [ ]))) [1,2:@le_S_S //]
 483 [ #sig #M #q #ch #qn #chn #mv #ls #k #n #Hk
 484   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 485   #Htrans elim n
 486   [ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // <loopM_unfold
 487     cut (fs = [ ])
 488     [ cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
 489       >length_append >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 490       <Hcrd >length_reverse #H1 cut (O = |f0::fs0|) [ /2/ ]
 491       normalize #H1 destruct (H1) ]
 492     #H destruct (H) >append_nil in Hfs; #Hfs
 493     >Hfs >reverse_reverse >(binaryTM_bin2_O … Htrans) //
 494   | #n0 #IH #csl #Hcount #Hcrd * #fs #Hfs
 495     >loopM_unfold >loop_S_false // <loopM_unfold
 496     >(?: step FinBool (mk_binaryTM sig M)
 497          (mk_config FinBool (states FinBool (mk_binaryTM sig M)) 〈q,bin2,〈ch,S n0〉〉
 498          (mk_tape FinBool (csl@ls) (None FinBool) []))
 499         = mk_config ?? (〈q,bin2,ch,n0〉)
 500           (tape_move ? (tape_write ?
 501             (mk_tape ? (csl@ls) (None ?) [ ]) (Some ? (FS_nth ? n0 == Some ? chn))) R))
 502     [| /2 by lt_S_to_lt/ | @(binaryTM_bin2_S_Some … Htrans) ]
 503     >(?: tape_move ? (tape_write ???) ? =
 504           mk_tape ? (((FS_nth ? n0 == Some sig chn)::csl)@ls) (None ?) [ ])
 505     [| cases csl // cases ls // ]
 506     cases fs in Hfs;
 507     [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
 508       -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 509       <Hcrd in ⊢ (%→?); >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 510       #Hfalse cut (S n0 = O) /2 by injective_plus_r/ #H destruct (H)
 511     | #f0 #fs0 #Hbinchar
 512       cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0) [@daemon]
 513       -Hbinchar #Hbinchar >Hbinchar @(trans_eq ???? (IH …)) //
 514       [ %{fs0} >reverse_cons >associative_append @Hbinchar
 515       | whd in ⊢ (??%?); /2 by / ]
 516       @eq_f @eq_f @eq_f3 //
 517     ]
 518   ]
 519 | #Hcut #sig #M #q #ch #qn #chn #mv #ls #k #Hk #Htrans
 520   @trans_eq
 521   [3: @(trans_eq ???? (Hcut ??????? ls ? (FS_crd sig) ? Htrans …)) //
 522     [3:@([ ]) | %{(bin_char ? chn)} % | % ]
 523   || % ]
 524 ]
 525 qed.
 526
 527 lemma binaryTM_phase2_Some_ow : ∀sig,M,q,ch,qn,chn,mv,ls,k,cs,rs.
 528   S (FS_crd sig) ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 529   |cs| = FS_crd sig →
 530   loopM ? (mk_binaryTM sig M) k
 531     (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 532       (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs))))
 533   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 534       (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 535         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs))). [2,3:@le_S_S /2 by O/]
 536 cut (∀sig,M,q,ch,qn,chn,mv,ls,rs,k,csr.
 537      〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 538      ∀csl.|csr|<S (2*FS_crd sig) →
 539      |csl@csr| = FS_crd sig →
 540      (∃fs.bin_char sig chn = reverse ? csl@fs) →
 541      loopM ? (mk_binaryTM sig M) (S (|csr|) + k)
 542        (mk_config ?? (〈q,bin2,ch,|csr|〉)
 543          (mk_tape ? (csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs))))
 544      = loopM ? (mk_binaryTM sig M) k
 545          (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 546            (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)))) [1,2: @le_S_S /2 by le_S/]
 547 [ #sig #M #q #ch #qn #chn #mv #ls #rs #k #csr #Htrans elim csr
 548   [ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [ ]);
 549     >(binaryTM_bin2_O … Htrans) <loopM_unfold @eq_f @eq_f @eq_f3 //
 550     cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
 551     >length_append >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 552     <Hcrd >length_reverse #H1 cut (O = |f0::fs0|) [ /2/ ]
 553     normalize #H1 destruct (H1)
 554   | #b0 #bs0 #IH #csl #Hcount #Hcrd * #fs #Hfs
 555     >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans)
 556     >(?: tape_move ? (tape_write ???) ? =
 557           mk_tape ? (((FS_nth ? (|bs0|)==Some sig chn)::csl)@ls)
 558             (option_hd ? (bs0@rs)) (tail ? (bs0@rs)))
 559       in match (tape_move ? (tape_write ???) ?);
 560     [| cases bs0 // cases rs // ] @IH
 561     [ whd in Hcount:(?%?); /2 by lt_S_to_lt/
 562     | <Hcrd >length_append >length_append normalize //
 563     | cases fs in Hfs;
 564       [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]      -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 565         <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 566         #Hfalse cut (S (|bs0|) = O) /2 by injective_plus_r/ #H destruct (H)
 567       | #f0 #fs0 #Hbinchar
 568         cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|bs0|) == Some ? chn)::fs0) [@daemon]
 569         -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
 570       ]
 571     ]
 572   ]
 573 | #Hcut #sig #M #q #ch #qn #chn #mv #ls #k #cs #rs #Hk #Htrans #Hcrd
 574   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @trans_eq
 575   [3: @(trans_eq ???? (Hcut ??????? ls ?? cs Htrans [ ] …)) //
 576     [ normalize % // | normalize @Hcrd | >Hcrd // ]
 577   || @eq_f2 [ >Hcrd % | @eq_f2 // @eq_f cases Hcrd // ] ] ]
 578 qed.
 579
 580 lemma binaryTM_bin3_O :
 581   ∀sig,M,t,q,ch.
 582   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,O〉) t)
 583   = mk_config ?? (〈q,bin0,None ?,to_initN (FS_crd sig) ??〉) t. [2,3:@le_S //]
 584 #sig #M #t #q #ch %
 585 qed.
 586
 587 lemma binaryTM_bin3_S :
 588   ∀sig,M,t,q,ch,k. S k ≤ S (2*FS_crd sig) →
 589   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,S k〉) t)
 590   = mk_config ?? (〈q,bin3,ch,to_initN k ??〉) (tape_move ? t L). [2,3: @le_S_S /2 by lt_to_le/]
 591 #sig #M #t #q #ch #k #HSk %
 592 qed.
 593
 594 lemma binaryTM_phase3 :∀sig,M,q,ch,k,n.
 595   S n ≤ k → n ≤ S (2*FS_crd sig) →
 596   ∀t.loopM ? (mk_binaryTM sig M) k
 597     (mk_config ?? (〈q,bin3,ch,n〉) t)
 598   = loopM ? (mk_binaryTM sig M) (k - S n)
 599       (mk_config ?? (〈q,bin0,None ?,FS_crd sig〉)
 600         (iter ? (λt0.tape_move ? t0 L) n t)). [2,3: /2 by lt_S_to_lt, le_to_lt_to_lt/]
 601 #sig #M #q #ch #k #n #Hk
 602 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech elim n
 603 [ #Hcrd #t >loopM_unfold >loop_S_false [| % ] >binaryTM_bin3_O //
 604 | #n0 #IH #Hlt #t >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S [|//]
 605   <IH [|/2 by lt_to_le/]
 606   <loopM_unfold % ]
 607 qed.
 608
 609 lemma binaryTM_bin4_None :
 610   ∀sig,M,t,q,ch.
 611   current ? t = None ? →
 612   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 613   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3: @le_S //]
 614 #sig #M #t #q #ch #Hcur whd in ⊢ (??%?); >Hcur %
 615 qed.
 616
 617 lemma binaryTM_phase4_write : ∀sig,M,q,ch,k,t.
 618   O < k → current ? t = None ? →
 619   loopM ? (mk_binaryTM sig M) k
 620     (mk_config ?? (〈q,bin4,ch,O〉) t)
 621   = loopM ? (mk_binaryTM sig M) (k-1)
 622       (mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t). [2,3: @le_S //]
 623 #sig #M #q #ch #k #t #Hk #Hcur
 624 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 625 >loopM_unfold >loop_S_false // <loopM_unfold >binaryTM_bin4_None //
 626 qed.
 627
 628 (* we don't get here any more! *
 629 lemma binaryTM_bin4_noextend :
 630   ∀sig,M,t,q,ch,cur,qn,mv.
 631   current ? t = Some ? cur →
 632   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 633   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 634   = mk_config ?? (〈q,bin2,ch,to_initN O ??〉) t. [2,3://]
 635 #sig #M #t #q #ch #cur #qn #mv #Hcur #Htrans
 636 whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 637 whd in match (trans FinBool ??); <Htrans %
 638 qed.
 639 *)
 640
 641 lemma binaryTM_bin4_extend :
 642   ∀sig,M,t,q,ch,cur,qn,an,mv.
 643   current ? t = Some ? cur →
 644   〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
 645   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 646   = mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L). [2,3:@le_S //]
 647 #sig #M #t #q #ch #cur #qn #an #mv #Hcur #Htrans
 648 whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 649 whd in match (trans FinBool ??); <Htrans %
 650 qed.
 651
 652 lemma binaryTM_phase4_extend : ∀sig,M,q,ch,k,t,cur,qn,an,mv.
 653   O < k → current ? t = Some ? cur →
 654   〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
 655   loopM ? (mk_binaryTM sig M) k
 656     (mk_config ?? (〈q,bin4,ch,O〉) t)
 657   = loopM ? (mk_binaryTM sig M) (k-1)
 658       (mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L)). [2,3: @le_S //]
 659 #sig #M #q #ch #k #t #cur #qn #an #mv #Hk #Hcur #Htrans
 660 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 661 >loopM_unfold >loop_S_false // <loopM_unfold >binaryTM_bin4_extend //
 662 qed.
 663
 664 lemma binaryTM_bin5_O :
 665   ∀sig,M,t,q,ch.
 666   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,O〉) t)
 667   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t R). [2,3:@le_S //]
 668 #sig #M #t #q #ch %
 669 qed.
 670
 671 lemma binaryTM_bin5_S :
 672   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 673   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,S k〉) t)
 674   = mk_config ?? (〈q,bin5,ch,to_initN k ??〉) (tape_move ? (tape_write ? t (Some ? false)) L). [2,3:@le_S /2 by lt_S_to_lt/]
 675 #sig #M #t #q #ch #k #HSk %
 676 qed.
 677
 678 (* extends the tape towards the left with an unimportant sequence that will be
 679    immediately overwritten *)
 680 lemma binaryTM_phase5 :∀sig,M,q,ch,k,n. S n ≤ k →
 681   ∀rs.n<S (2*FS_crd sig) →
 682   ∃bs.|bs| = n ∧
 683   loopM ? (mk_binaryTM sig M) k
 684     (mk_config ?? (〈q,bin5,ch,n〉) (mk_tape ? [] (None ?) rs))
 685   = loopM ? (mk_binaryTM sig M) (k - S n)
 686       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 687         (mk_tape ? [] (option_hd ? (bs@rs)) (tail ? (bs@rs)))). [2,3:@le_S //]
 688 #sig #M #q #ch #k #n #Hk
 689 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 690 elim n
 691 [ #rs #Hlt %{[]} % // cases rs //
 692 | #n0 #IH #rs #Hn0 cases (IH (false::rs) ?) [|/2 by lt_S_to_lt/]
 693   #bs * #Hbs -IH #IH
 694   %{(bs@[false])} % [ <Hbs >length_append /2 by increasing_to_injective/ ]
 695   >loopM_unfold >loop_S_false // >binaryTM_bin5_S
 696   >associative_append normalize in match ([false]@?); <IH
 697   >loopM_unfold @eq_f @eq_f cases rs //
 698 ]
 699 qed.
 700
 701 lemma current_None_or_midtape :
 702   ∀sig,t.current sig t = None sig ∨ ∃ls,c,rs.t = midtape sig ls c rs.
 703 #sig * normalize /2/ #ls #c #rs %2 /4 by ex_intro/
 704 qed.
 705
 706 lemma state_bin_lift_unfold :
 707   ∀sig.∀M:TM sig.∀q:states sig M.
 708   state_bin_lift sig M q = 〈q,bin0,None ?,FS_crd sig〉.// qed.
 709
 710 axiom current_tape_bin_list :
 711  ∀sig,t.current sig t = None ? → current ? (tape_bin_lift sig t) = None ?.
 712
 713 lemma tape_bin_lift_unfold :
 714  ∀sig,t. tape_bin_lift sig t =
 715  mk_tape ? (rev_bin_list ? (left ? t)) (option_hd ? (opt_bin_char sig (current ? t)))
 716    (tail ? (opt_bin_char sig (current ? t))@bin_list ? (right ? t)). //
 717 qed.
 718
 719 lemma reverse_bin_char_list : ∀sig,c,l.
 720   reverse ? (bin_char sig c)@rev_bin_list ? l = rev_bin_list ? (c::l). // qed.
 721
 722 lemma left_midtape : ∀sig,ls,c,rs.left ? (midtape sig ls c rs) = ls.// qed.
 723 lemma current_midtape : ∀sig,ls,c,rs.current ? (midtape sig ls c rs) = Some ? c.// qed.
 724 lemma right_midtape : ∀sig,ls,c,rs.right ? (midtape sig ls c rs) = rs.// qed.
 725 lemma opt_bin_char_Some : ∀sig,c.opt_bin_char sig (Some ? c) = bin_char ? c.// qed.
 726
 727 lemma opt_cons_hd_tl : ∀A,l.option_cons A (option_hd ? l) (tail ? l) = l.
 728 #A * // qed.
 729
 730 lemma le_tech : ∀a,b,c.a ≤ b → a * c ≤ b * c.
 731 #a #b #c #H /2 by monotonic_le_times_r/
 732 qed.
 733
 734 lemma iter_split : ∀T,f,m,n,x.
 735   iter T f (m+n) x = iter T f m (iter T f n x).
 736 #T #f #m #n elim n /2/
 737 #n0 #IH #x <plus_n_Sm whd in ⊢ (??%(????%)); >IH %
 738 qed.
 739
 740 lemma iter_tape_move_R : ∀T,n,ls,cs,rs.|cs| = n →
 741   iter ? (λt0.tape_move T t0 R) n (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs)))
 742   = mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs).
 743 #T #n elim n
 744 [ #ls * [| #c0 #cs0 #rs #H normalize in H; destruct (H) ] #rs #_ %
 745 | #n0 #IH #ls * [ #rs #H normalize in H; destruct (H) ] #c #cs #rs #Hlen
 746   whd in ⊢ (??%?);
 747   >(?: (tape_move T (mk_tape T ls (option_hd T ((c::cs)@rs)) (tail T ((c::cs)@rs))) R)
 748     = mk_tape ? (c::ls) (option_hd ? (cs@rs)) (tail ? (cs@rs))) in ⊢ (??(????%)?);
 749   [| cases cs // cases rs // ] >IH
 750   [ >reverse_cons >associative_append %
 751   | normalize in Hlen; destruct (Hlen) % ]
 752 ]
 753 qed.
 754
 755 lemma tail_tech : ∀T,l1,l2.O < |l1| → tail T (l1@l2) = tail ? l1@l2.
 756 #T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/
 757 qed.
 758
 759 lemma hd_tech : ∀T,l1,l2.O < |l1| → option_hd T (l1@l2) = option_hd ? l1.
 760 #T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/
 761 qed.
 762
 763 lemma iter_tape_move_l_nil : ∀T,n,rs.
 764   iter ? (λt0.tape_move T t0 L) n (mk_tape ? [ ] (None ?) rs) =
 765   mk_tape ? [ ] (None ?) rs.
 766 #T #n #rs elim n // #n0 #IH <IH in ⊢ (???%); cases rs //
 767 qed.
 768
 769 lemma iter_tape_move_L_left : ∀T,n,cs,rs. O < n →
 770   iter ? (λt0.tape_move T t0 L) n
 771     (mk_tape ? [ ] (option_hd ? cs) (tail ? cs@rs)) =
 772   mk_tape ? [ ] (None ?) (cs@rs).
 773 #T #n #cs #rs *
 774 [ cases cs // cases rs //
 775 | #m #_ whd in ⊢ (??%?); <(iter_tape_move_l_nil ? m) cases cs // cases rs // ]
 776 qed.
 777
 778 lemma iter_tape_move_L : ∀T,n,ls,cs,rs.|cs| = n →
 779   iter ? (λt0.tape_move T t0 L) n (mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs))
 780   = mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs)).
 781 #T #n elim n
 782 [ #ls * [| #c0 #cs0 #rs #H normalize in H; destruct (H) ] #rs #_ %
 783 | #n0 #IH #ls #cs #rs @(list_elim_left … cs)
 784   [ #H normalize in H; destruct (H) ] -cs
 785   #c #cs #_ #Hlen >reverse_append whd in ⊢ (??%?);
 786   >(?: tape_move T (mk_tape T ((reverse T [c]@reverse T cs)@ls) (option_hd T rs) (tail T rs)) L
 787     = mk_tape ? (reverse T cs@ls) (option_hd ? (c::rs)) (tail ? (c::rs))) in ⊢ (??(????%)?);
 788   [| cases rs // ] >IH
 789   [ >associative_append %
 790   | >length_append in Hlen; normalize // ]
 791 ]
 792 qed.
 793
 794 lemma binaryTM_loop :
 795  ∀sig,M,i,t,q,tf,qf.
 796  O < FS_crd sig →
 797  loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
 798  ∃k.loopM ? (mk_binaryTM sig M) k
 799   (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) =
 800   Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf)).
 801 #sig #M #i elim i
 802 [ #t #q #qf #tf #Hcrd change with (None ?) in ⊢ (??%?→?); #H destruct (H)
 803 | -i #i #IH #t #q #tf #qf #Hcrd >loopM_unfold
 804   lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t))))
 805   cases (halt ?? q) in ⊢ (???%→?); #Hhalt
 806   [ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
 807     #H destruct (H) %{1} >loopM_unfold >loop_S_true // ]
 808   (* interesting case: more than one step *)
 809   >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
 810   <loopM_unfold >(config_expand ?? (step ???)) #Hloop
 811   lapply (IH … Hloop) [@Hcrd] -IH * #k0 #IH <config_expand in Hloop; #Hloop
 812   %{(7*(S (FS_crd sig)) + k0)}
 813   (*** PHASE 0 ***)
 814   >state_bin_lift_unfold cases (current_None_or_midtape ? t)
 815   (* 0.1) current = None *)
 816   [ (* #Hcur >state_bin_lift_unfold in ⊢ (??%?);
 817     lapply (current_tape_bin_list … Hcur) #Hcur'
 818     >binaryTM_phase0_None /2 by monotonic_lt_plus_l/
 819     >(?: FS_crd sig + k0 = S (FS_crd sig + k0 - 1)) [|@daemon]
 820     >loopM_unfold >loop_S_false // lapply (refl ? t) cases t in ⊢ (???%→?);
 821     [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H) normalize in Hcur; destruct (Hcur)
 822     | #Ht >Ht >binaryTM_bin4_None // <loopM_unfold *)
 823   (* 0.2) midtape *)
 824   | * #ls * #c * #rs #Ht >Ht >tape_bin_lift_unfold
 825     >left_midtape >current_midtape >right_midtape >opt_bin_char_Some
 826     >(binaryTM_phase0_midtape … Hhalt ? (refl ??)) [| // ]
 827     >(?: 7*S (FS_crd sig) + k0 - S (FS_crd sig) = 6*S (FS_crd sig) + k0) [|/2 by plus_minus/]
 828     (*** PHASE 1 ***)
 829     >binaryTM_phase1
 830     [| cases (bin_list ? rs) normalize // #r0 #rs0 #H destruct (H)
 831     | >length_reverse @daemon
 832     | // ]
 833     >(?:6*S (FS_crd sig) + k0 - S (FS_crd sig) = 5*S (FS_crd sig) + k0) [|/2 by plus_minus/]
 834     >reverse_reverse >opt_cons_hd_tl
 835     cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,Some ? c〉)
 836     [ cases (trans ? M 〈q,Some ? c〉) * #qn #chn #mv /4 by ex_intro/ ]
 837     * #qn * #chn * #mv cases chn -chn
 838     [ (* no write! *) #Htrans >(binaryTM_phase2_None … Htrans) [2,3: //]
 839       >iter_tape_move_R [|@daemon]
 840       >(?:5*S (FS_crd sig) + k0 - S (FS_crd sig) = 4*S (FS_crd sig) + k0) [|/2 by plus_minus/]
 841       >binaryTM_phase3
 842       [|//| cut (S (displ_of_move sig mv) ≤ 2*(S (FS_crd sig)))
 843         [ /2 by le_S_S/
 844         | #H @(transitive_le ??? H) -H -Hcrd @(transitive_le ? (4*S (FS_crd sig))) /2 by le_plus_a/ ]
 845       ]
 846       cut (∀sig,M,m,n,cfg,cfg'.m < n → loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg') [@daemon]
 847       #Hcut <(Hcut ??? (4*S (FS_crd sig) + k0 - S (displ_of_move sig mv)) ??? IH)
 848       [| cases mv
 849         [ >(?:displ_of_move sig L = 2*FS_crd sig) //
 850           >eq_minus_S_pred
 851           @(transitive_le ? (pred (4*FS_crd sig+k0-2*FS_crd sig)))
 852           [ >(?:4*FS_crd sig+k0-2*FS_crd sig = 2*FS_crd sig + k0)
 853             [ cases Hcrd /2 by le_minus_to_plus, le_n/
 854             | <plus_minus [2://]
 855               >(commutative_times 4) >(commutative_times 2)
 856               <distributive_times_minus //
 857             ]
 858           | @monotonic_pred /2 by monotonic_le_minus_l/ ]
 859         | whd in match (displ_of_move ??); @(transitive_le ? (4*1+k0-1))
 860           [ //
 861           | change with (pred (4*1+k0)) in ⊢ (?%?);
 862              >eq_minus_S_pred <minus_n_O @monotonic_pred // ]
 863         | >(?:displ_of_move sig N = FS_crd sig) //
 864           >eq_minus_S_pred
 865           @(transitive_le ? (pred (4*FS_crd sig+k0-1*FS_crd sig)))
 866           [ >(?:4*FS_crd sig+k0-1*FS_crd sig = 3*FS_crd sig + k0)
 867             [ cases Hcrd /2 by le_minus_to_plus, le_n/
 868             | <plus_minus [2://]
 869               >(commutative_times 4) >(commutative_times 1)
 870               <distributive_times_minus //
 871             ]
 872           | @monotonic_pred /2 by transitive_le, le_n/ ] ] ]
 873       @eq_f @eq_f2
 874       [ <state_bin_lift_unfold >Ht whd in match (step ???); <Htrans %
 875       | (* must distinguish mv *)
 876         cases mv in Htrans; #Htrans
 877         [ >(?:displ_of_move ? L = FS_crd sig + FS_crd sig) [| normalize // ]
 878           >iter_split >iter_tape_move_L [|@daemon] >Ht cases ls
 879           [ normalize in match (rev_bin_list ??);
 880             >hd_tech [|@daemon] >tail_tech [|@daemon]
 881             >iter_tape_move_L_left // whd in match (step ???);
 882             <Htrans whd in match (ctape ???);
 883             >tape_bin_lift_unfold %
 884           | #l0 #ls0 change with (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) in match (rev_bin_list ??);
 885             >iter_tape_move_L [|@daemon]
 886             >hd_tech [|@daemon] >tail_tech [|@daemon]
 887             whd in match (step ???); <Htrans whd in match (ctape ???);
 888             >tape_bin_lift_unfold >left_midtape >current_midtape
 889             >opt_bin_char_Some >right_midtape %
 890           ]
 891         | change with
 892             (mk_tape ? (reverse ? (bin_char ? c)@rev_bin_list ? ls)
 893               (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
 894           in ⊢ (??%?);
 895           >reverse_bin_char_list <IH
 896           >Ht >tape_bin_lift_unfold @eq_f3
 897           whd in match (step ???); <Htrans cases rs //
 898           #r0 #rs0 whd in match (ctape ???); >current_midtape >opt_bin_char_Some
 899           [ <hd_tech in ⊢(???%); // @daemon
 900           | >right_midtape <tail_tech // @daemon ]
 901         | whd in match (displ_of_move ? N); >iter_tape_move_L [|@daemon]
 902           >Ht whd in match (step ???); <Htrans whd in match (ctape ???);
 903           >tape_bin_lift_unfold >left_midtape >current_midtape >right_midtape
 904           >opt_bin_char_Some lapply Hcrd >(?:FS_crd sig = |bin_char ? c|) [| @daemon ]
 905           cases (bin_char ? c) // #H normalize in H; @False_ind
 906           cases (not_le_Sn_O O) /2/
 907         ]
 908       ]
 909
 910
 911
 912
 913
 914 (*
 915 theorem sem_binaryTM : ∀sig,M.
 916   mk_binaryTM sig M ⊫ R_bin_lift ? (R_TM ? M (start ? M)).
 917 #sig #M #t #i generalize in match t; -t
 918 @(nat_elim1 … i) #m #IH #intape #outc #Hloop
 919
 920 *)