(* 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- never halts.  (WORK IN PROGRESS: round 1 of the
   formalization; the final theorem is not proved yet, see rocq/log.md.)
   Skelet 1-like Class 2: a binary down-counter on a list of pairs (10)^p (01)^q s(d)
   (s(1) = 0001, s(0) = 0010) behind a left marker (10)^h 11001, with overflow re-pairing.
   Loose template: vendor/busycoq/verify/SBCv6.v, Module TM21 (pair list + counter sweeps +
   re-pairing at overflow); the sweep lemmas here are new and proved by plain [es].
   Informal proof: machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/proof.md.
   Formalized with Claude Code (AI-assisted); checked by tools/check_kill.sh *)

From BusyCoq Require Import Individual62.
Require Import Arith Lia List.
Require Import String.
Import ListNotations.

Definition tm := Eval compute in (TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---").

Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Open Scope list.

Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.
Proof. intros H E. subst. exact H. Qed.

Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.
Proof. intros H E. subst. exact H. Qed.

(** * Low-level sweeps (all by [es]).
    Paper words: pair [p,q,d] = (10)^p (01)^q s(d), s(1) = 0001, s(0) = 0010.
    During the long rightward sweep a passed pair [p,q+1,0] is left behind as
    region (paper) 0 (01)^p 110 (01)^q 11, the 0 being the boundary cell. *)

Lemma Start h r : 0inf <{{A}} [1;0]^^h *> [1;1;0;0;1] *> r -->+
  0inf <* <[1;0]^^(4+h) <* <[1;1;1] <* [0] {{B}}> r.
Proof. es. Qed.

Lemma PassR l p q r : l <* [0] {{B}}> [1;0]^^p *> [0;1]^^(S q) *> [0;0;1;0] *> r -->*
  l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^q <* <[1;1] <* [0] {{B}}> r.
Proof. es. Qed.

Lemma Borrow l p q r : l {{B}}> [1;0]^^p *> [0;1]^^(S (S q)) *> [0;0;0;1] *> r -->*
  l <{{D}} [1;0]^^(S p) *> [0;1]^^(S q) *> [0;0;1;0] *> r.
Proof. es. Qed.

Lemma PassL l p q r : l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] <{{D}} r -->*
  l <* [0] <{{D}} [1;0]^^(S p) *> [0;1]^^(S q) *> [0;0;0;1] *> r.
Proof. es. Qed.

Lemma EndPh h r : 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <* [0] <{{D}} r -->*
  0inf <{{A}} [1;0]^^(4+h) *> [1;1;0;0;1] *> r.
Proof. es. Qed.

Lemma EndT l p q : l <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] {{B}}> 0inf -->*
  l <{{D}} [1;0]^^(S p) *> [0;1]^^(S q) *> [0;0;1;0] *> [1;0;1] *> 0inf.
Proof. es. Qed.

Lemma EndLastT l p : l <* <[0;1]^^p <* <[1;1;0] <* <[1;1] <* [0] {{B}}> 0inf -->*
  l <{{D}} [1;0]^^(p+4) *> [1] *> 0inf.
Proof. es. Qed.

Lemma MergeB l p p' r : l {{B}}> [1;0]^^p *> [0;1] *> [0;0;0;1] *> [1;0]^^p' *> r -->*
  l <{{D}} [1;0]^^(p+p'+3) *> r.
Proof. es. Qed.

Lemma MergeE l p : l {{B}}> [1;0]^^p *> [0;1] *> [0;0;0;1] *> 0inf -->*
  l <{{D}} [1;0]^^(p+2) *> [1] *> 0inf.
Proof. es. Qed.

Lemma OvT l t : l <* [0] {{B}}> [1;0]^^t *> [1] *> 0inf -->*
  l <{{D}} [0;1]^^(S t) *> [0;0;0;1] *> 0inf.
Proof. es. Qed.

Lemma OvL l p q r : l <* [0] <* <[0;1]^^(S p) <* <[1;1;0] <* <[0;1]^^q <* <[1;1] <{{D}} r -->*
  l <{{D}} [0;1]^^(S p) *> [0;0;0;1] *> [1;0]^^(S q) *> r.
Proof. es. Qed.

Lemma OvEnd h p r : 0inf <* <[1;0]^^(4+h) <* <[1;1;1] <{{D}} [0;1]^^(S (S p)) *> [0;0;0;1] *> r -->*
  0inf <{{A}} [1;0]^^2 *> [1;1;0;0;1] *> [1;0]^^(h+5) *> [0;1]^^(S p) *> [0;0;1;0] *> r.
Proof. es. Qed.

Lemma X1Sw l p r : l <* [0] <* <[0;1]^^(S p) <* <[1;1;0] <* <[1;1] <* [0] <{{D}} r -->*
  l <{{D}} [0;1]^^(S p) *> [0;0;1;0;1;0;1] *> r.
Proof. es. Qed.

Lemma X2T l p q k : l <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(S q) <* <[1;1] <* [0] {{B}}> [1;0;1;1;0;1] *> [0;1]^^(S k) *> 0inf -->*
  l <{{D}} [1;0]^^(S p) *> [0;1]^^(S q) *> [0;0;1;0] *> [1;0]^^3 *> [0;1]^^(S k) *> [0;0;0;1] *> 0inf.
Proof. es. Qed.

(** * The family K (proof.md section 1) *)

Definition sd (d : bool) : list Sym := if d then [0;0;0;1] else [0;0;1;0].

Fixpoint RP (P : list (nat*nat*bool)) (r : side) : side :=
  match P with
  | [] => r
  | (p,q,d) :: P' => [1;0]^^p *> [0;1]^^q *> sd d *> RP P' r
  end.

Inductive Tl := TN | TA (t : nat) | TB (k : nat).

Definition RT (T : Tl) : side :=
  match T with
  | TN => 0inf
  | TA t => [1;0]^^t *> [1] *> 0inf
  | TB k => [1;0;1;1;0;1] *> [0;1]^^k *> 0inf
  end.

Definition K (h : nat) (P : list (nat*nat*bool)) (T : Tl) : Q * tape :=
  0inf <{{A}} [1;0]^^h *> [1;1;0;0;1] *> RP P (RT T).

Definition pre (h : nat) : side := 0inf <* <[1;0]^^(4+h) <* <[1;1;1].

(** region left behind by the rightward sweep over pair (p,q,_) *)
Definition reg (p q : nat) (l : side) : side :=
  l <* [0] <* <[0;1]^^p <* <[1;1;0] <* <[0;1]^^(pred q) <* <[1;1].

Fixpoint LP (Z : list (nat*nat*bool)) (l : side) : side :=
  match Z with
  | [] => l
  | (p,q,d) :: Z' => LP Z' (reg p q l)
  end.

(** what the overflow sweep leaves for pair (p,q,_) *)
Fixpoint OvR (Z : list (nat*nat*bool)) (r : side) : side :=
  match Z with
  | [] => r
  | (p,q,d) :: Z' => [0;1]^^p *> [0;0;0;1] *> [1;0]^^q *> OvR Z' r
  end.

Definition touch (x : nat*nat*bool) : nat*nat*bool :=
  let '(p,q,d) := x in (S p, pred q, negb d).

Definition okR (x : nat*nat*bool) : Prop := let '(p,q,d) := x in d = false /\ 1 <= q.
Definition okL (x : nat*nat*bool) : Prop := let '(p,q,d) := x in d = false /\ 2 <= q.
Definition okO (x : nat*nat*bool) : Prop := let '(p,q,d) := x in 1 <= p /\ 1 <= q.

Lemma RP_app Z W r : RP (Z ++ W) r = RP Z (RP W r).
Proof.
  induction Z as [|[[p q] d] Z IH]; cbn; [reflexivity|]. rewrite IH. reflexivity.
Qed.

Lemma LP_app Z W l : LP (Z ++ W) l = LP W (LP Z l).
Proof.
  revert l. induction Z as [|[[p q] d] Z IH]; intros l; cbn; [reflexivity|]. apply IH.
Qed.

Lemma PassesR Z : Forall okR Z -> forall l r,
  l <* [0] {{B}}> RP Z r -->* LP Z l <* [0] {{B}}> r.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros HZ l r; cbn [RP LP]; [finish|].
  inversion HZ as [|? ? Hx HZ']; subst; hnf in Hx; destruct Hx as [Hd Hq]; subst d.
  destruct q as [|q]; [lia|].
  eapply evstep_trans. { apply PassR. }
  apply (IH HZ' (reg p (S q) l) r).
Qed.

Lemma PassesL Z : Forall okL Z -> forall l r,
  LP Z l <* [0] <{{D}} r -->* l <* [0] <{{D}} RP (map touch Z) r.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros HZ l r; cbn [RP LP map]; [finish|].
  inversion HZ as [|? ? Hx HZ']; subst; hnf in Hx; destruct Hx as [Hd Hq]; subst d.
  destruct q as [|[|q]]; [lia|lia|].
  eapply evstep_trans. { apply (IH HZ' (reg p (S (S q)) l)). }
  unfold reg. cbn [pred]. apply PassL.
Qed.

Lemma OvPasses Z : Forall okO Z -> forall l r,
  LP Z l <{{D}} r -->* l <{{D}} OvR Z r.
Proof.
  induction Z as [|[[p q] d] Z IH]; intros HZ l r; cbn [OvR LP]; [finish|].
  inversion HZ as [|? ? Hx HZ']; subst; hnf in Hx; destruct Hx as [Hp Hq].
  destruct p as [|p]; [lia|]. destruct q as [|q]; [lia|].
  eapply evstep_trans. { apply (IH HZ' (reg (S p) (S q) l)). }
  unfold reg. cbn [pred]. apply OvL.
Qed.

Lemma okL_R Z : Forall okL Z -> Forall okR Z.
Proof.
  intros H. eapply Forall_impl; [|exact H]. intros [[p q] d] [H1 H2]. split; [exact H1 | lia].
Qed.

(** * Macro rules (proof.md section 2) *)

Lemma Dec h Z p q R T : Forall okL Z ->
  K h (Z ++ (p, S (S q), true) :: R) T -->+ K (4+h) (map touch Z ++ (S p, S q, false) :: R) T.
Proof.
  intros HZ. unfold K. rewrite !RP_app. cbn [RP sd].
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR, okL_R, HZ. }
  eapply evstep_trans. { apply Borrow. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  apply EndPh.
Qed.

Lemma DecMerge h Z p p' q' d' R T : Forall okL Z ->
  K h (Z ++ (p, 1%nat, true) :: (p', q', d') :: R) T -->+ K (4+h) (map touch Z ++ (p+p'+3, q', d') :: R) T.
Proof.
  intros HZ. unfold K. rewrite !RP_app. cbn [RP sd].
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR, okL_R, HZ. }
  eapply evstep_trans. { apply MergeB. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  apply EndPh.
Qed.

Lemma DecMergeTail h Z p t : Forall okL Z ->
  K h (Z ++ [(p, 1%nat, true)]) (TA t) -->+ K (4+h) (map touch Z) (TA (p+t+3)).
Proof.
  intros HZ. unfold K. rewrite !RP_app. cbn [RP sd RT].
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR, okL_R, HZ. }
  eapply evstep_trans. { apply MergeB. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  apply EndPh.
Qed.

Lemma DecMergeEmpty h Z p : Forall okL Z ->
  K h (Z ++ [(p, 1%nat, true)]) TN -->+ K (4+h) (map touch Z) (TA (p+2)).
Proof.
  intros HZ. unfold K. rewrite !RP_app. cbn [RP sd RT].
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR, okL_R, HZ. }
  eapply evstep_trans. { apply MergeE. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  apply EndPh.
Qed.

Lemma Forall_snoc {A} (P : A -> Prop) Z x : Forall P Z -> P x -> Forall P (Z ++ [x]).
Proof. intros H1 H2. apply Forall_app. split; auto. Qed.

Lemma EndR h Z p q : Forall okL Z ->
  K h (Z ++ [(p, S (S q), false)]) TN -->+ K (4+h) (map touch Z ++ [(S p, S q, false)]) (TA 1).
Proof.
  intros HZ. unfold K.
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR. apply Forall_snoc; [apply okL_R, HZ | cbn; split; [reflexivity | lia]]. }
  rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
  eapply evstep_trans. { apply EndT. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  rewrite RP_app. apply EndPh.
Qed.

Lemma EndLast h Z p : Forall okL Z ->
  K h (Z ++ [(p, 1%nat, false)]) TN -->+ K (4+h) (map touch Z) (TA (p+4)).
Proof.
  intros HZ. unfold K.
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR. apply Forall_snoc; [apply okL_R, HZ | cbn; split; [reflexivity | lia]]. }
  rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
  eapply evstep_trans. { apply EndLastT. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  apply EndPh.
Qed.

Lemma X2 h Z p q k : Forall okL Z ->
  K h (Z ++ [(p, S (S q), false)]) (TB (S k)) -->+
  K (4+h) (map touch Z ++ [(S p, S q, false); (3%nat, S k, true)]) TN.
Proof.
  intros HZ. unfold K.
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR. apply Forall_snoc; [apply okL_R, HZ | cbn; split; [reflexivity | lia]]. }
  rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
  eapply evstep_trans. { apply X2T. }
  eapply evstep_trans. { apply (PassesL Z HZ). }
  rewrite RP_app. apply EndPh.
Qed.

Fixpoint ovp (q : nat) (Z : list (nat*nat*bool)) (t : nat) : list (nat*nat*bool) :=
  match Z with
  | [] => [(q, S t, true)]
  | (p',q',_) :: Z' => (q, p', true) :: ovp q' Z' t
  end.

Lemma ovp_eq Z : forall q t, RP (ovp q Z t) 0inf = [1;0]^^q *> OvR Z ([0;1]^^(S t) *> [0;0;0;1] *> 0inf).
Proof.
  induction Z as [|[[p q'] d] Z IH]; intros q t; cbn [ovp RP OvR sd]; [reflexivity|].
  rewrite IH. reflexivity.
Qed.

Lemma Ov h p1 q1 Z t : 1 <= q1 -> Forall okR Z -> Forall okO Z ->
  K h ((S (S p1), q1, false) :: Z) (TA t) -->+ K 2 ((h+5, S p1, false) :: ovp q1 Z t) TN.
Proof.
  intros Hq HR HO. unfold K.
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR. constructor; [cbn; split; [reflexivity|lia] | exact HR]. }
  cbn [RT LP].
  eapply evstep_trans. { apply OvT. }
  eapply evstep_trans. { apply (OvPasses Z HO). }
  destruct q1 as [|q1]; [lia|]. unfold reg. cbn [pred].
  eapply evstep_trans. { apply OvL. }
  eapply ev_eq. { apply OvEnd. }
  cbn [RP sd RT]. rewrite ovp_eq. reflexivity.
Qed.

Fixpoint ovpX (q : nat) (Z : list (nat*nat*bool)) (pa : nat) : list (nat*nat*bool) :=
  match Z with
  | [] => [(q, pa, false)]
  | (p',q',_) :: Z' => (q, p', true) :: ovpX q' Z' pa
  end.

Lemma ovpX_eq Z : forall q pa r, RP (ovpX q Z pa) r = [1;0]^^q *> OvR Z ([0;1]^^pa *> [0;0;1;0] *> r).
Proof.
  induction Z as [|[[p q'] d] Z IH]; intros q pa r; cbn [ovpX RP OvR sd]; [reflexivity|].
  rewrite IH. reflexivity.
Qed.

Lemma tailB_eq n : [0;0;1;0;1;0;1] *> [1;0]^^(S n) *> [1] *> 0inf = [0;0;1;0] *> RT (TB n).
Proof.
  cbn [RT]. cbn [lpow app]. cbn [Str_app]. f_equal. f_equal. f_equal. f_equal. f_equal. f_equal. f_equal.
  f_equal. f_equal. f_equal.
  change ([1;0]^^n *> 1 >> 0inf = 1 >> [0;1]^^n *> 0inf).
  apply lpow_rotate.
Qed.

Lemma X1 h p1 q1 Z pa pb : 1 <= q1 -> Forall okR Z -> Forall okO Z ->
  K h ((S (S p1), q1, false) :: Z ++ [(S pa, 1%nat, false); (pb, 1%nat, false)]) TN -->+
  K 2 ((h+5, S p1, false) :: ovpX q1 Z (S pa)) (TB (pb+3)).
Proof.
  intros Hq HR HO. unfold K.
  eapply progress_evstep_trans. { apply Start. }
  eapply evstep_trans. { apply PassesR. constructor; [cbn; split; [reflexivity|lia] |].
    apply Forall_app. split; [exact HR|]. repeat constructor; lia. }
  cbn [LP]. rewrite LP_app. cbn [LP RT]. unfold reg at 1. cbn [pred].
  eapply evstep_trans. { apply EndLastT. }
  unfold reg at 1. cbn [pred].
  eapply evstep_trans. { apply X1Sw. }
  eapply evstep_trans. { apply (OvPasses Z HO). }
  destruct q1 as [|q1]; [lia|]. unfold reg. cbn [pred].
  eapply evstep_trans. { apply OvL. }
  eapply ev_eq. { apply OvEnd. }
  cbn [RP sd]. rewrite ovpX_eq. replace (pb+4) with (S (pb+3)) by lia. rewrite tailB_eq. reflexivity.
Qed.

(** * Start (proof.md 3.7): c0 reaches K0 = K(2; (11,11,0); -) in 956 steps, and the base
    E-start after overflow 6, K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); -), in 78,710 steps.
    Both by direct execution ([esx]); the second takes about 30 s. *)

Lemma init0 : c0 -->* K 2 [(11%nat, 11%nat, false)] TN.
Proof. unfold K. cbn [RP RT sd]. esx. Qed.

Definition base : list (nat*nat*bool) :=
  [(95%nat, 68%nat, false); (34%nat, 33%nat, true); (10%nat, 15%nat, true); (1%nat, 24%nat, true)].

Lemma init : c0 -->* K 2 base TN.
Proof. unfold K, base. cbn [RP RT sd]. esx. Qed.

(*
```
1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---

[p,q,d] := (10)^p (01)^q s(d),  s(1) = 0001, s(0) = 0010                 [RP]
K(h; P; T) := 0^inf <A (10)^h 11001 [p_1,q_1,d_1] ... [p_L,q_L,d_L] T 0^inf   [K]
T in { -, (10)^t 1, (101)^2 (01)^k }                                       [TN, TA t, TB k]
k := least j with d_j = 1;  Z := pairs 1..k-1 (all d = 0, q >= 2)
touch (p,q,d) := (p+1, q-1, 1-d)

Dec            K(h; Z ++ (p,q+2,1) :: R; T)        -->+ K(h+4; touch Z ++ (p+1,q+1,0) :: R; T)
DecMerge       K(h; Z ++ (p,1,1) :: (p',q',d') :: R; T) -->+ K(h+4; touch Z ++ (p+p'+3,q',d') :: R; T)
DecMergeTail   K(h; Z ++ [(p,1,1)]; (10)^t 1)      -->+ K(h+4; touch Z; (10)^(p+t+3) 1)
DecMergeEmpty  K(h; Z ++ [(p,1,1)]; -)             -->+ K(h+4; touch Z; (10)^(p+2) 1)
End            K(h; Z ++ [(p,q+2,0)]; -)           -->+ K(h+4; touch Z ++ [(p+1,q+1,0)]; (10)^1 1)
EndLast        K(h; Z ++ [(p,1,0)]; -)             -->+ K(h+4; touch Z; (10)^(p+4) 1)
X2             K(h; Z ++ [(p,q+2,0)]; (101)^2 (01)^(k+1))
                                                   -->+ K(h+4; touch Z ++ [(p+1,q+1,0); (3,k+1,1)]; -)
Ov             K(h; (p1+2,q1,0) :: Y; (10)^t 1)    -->+ K(2; (h+5,p1+1,0) :: ovp q1 Y t; -)
               Y all d = 0, p,q >= 1, q1 >= 1;  ovp q [] t = [(q,t+1,1)],
               ovp q ((p',q',_) :: Y) t = (q,p',1) :: ovp q' Y t
X1             K(h; (p1+2,q1,0) :: Y ++ [(pa+1,1,0); (pb,1,0)]; -)
                                                   -->+ K(2; (h+5,p1+1,0) :: ovpX q1 Y (pa+1); (101)^2 (01)^(pb+3))
               ovpX q [] pa = [(q,pa,0)], ovpX q ((p',q',_) :: Y) pa = (q,p',1) :: ovpX q' Y pa
start: c0 -->(956) K(2; (11,11,0); -) -->(77,754) K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); -)
```
*)