(* Plan check for proof.md section 6 (NOT the kill file): the mirror dictionary applied to kill #11's
   window lemmas, digit lemmas, K and init, on 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---.
   Mirror dictionary: l {{q}}> r  <->  r <{{pi q}} l ;  l <* xs  <->  xs *> l (list literals unchanged);
   pi = (A,B,C,D,E,F) -> (B,C,D,A,E,F). *)
From BusyCoq Require Import Individual62.
Require Import ZifyNat Lia.
Require Import String.
Require Import List.
Require Import Arith.

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

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

Open Scope list.

(* ---------- shift lemmas (one block, then shift_rule_L/R) ---------- *)
Lemma S1_1 l r: l <* [0;1] <{{C}} [] *> r -->* l <{{C}} [] *> [0;1] *> r.  Proof. es. Qed.
Lemma S2_1 l r: l <* [1;0] <{{D}} [] *> r -->* l <{{D}} [] *> [1;0] *> r.  Proof. es. Qed.
Lemma S3_1 l r: l <* [] {{A}}> [1;0] *> r -->* l <* [1;0] <* [] {{A}}> r.  Proof. es. Qed.
Lemma S4_1 l r: l <* [] {{E}}> [0;1] *> r -->* l <* [0;1] <* [] {{E}}> r.  Proof. es. Qed.
Lemma S6_1 l r: l <* [1;0] <{{C}} [0] *> r -->* l <{{C}} [0] *> [0;1] *> r.  Proof. es. Qed.
Lemma S5_1 l r: l <* [0;1] <* [1;1] <{{D}} r -->* l <* [1;1] <{{D}} [0;1] *> r.  Proof. es. Qed.

Definition S1 := shift_rule_L _ _ _ _ _ S1_1.
Definition S2 := shift_rule_L _ _ _ _ _ S2_1.
Definition S3 := shift_rule_R _ _ _ _ _ S3_1.
Definition S4 := shift_rule_R _ _ _ _ _ S4_1.
Definition S6 := shift_rule_L _ _ _ _ _ S6_1.

Lemma S5 n: forall l r, l <* [0;1]^^n <* [1;1] <{{D}} r -->* l <* [1;1] <{{D}} [0;1]^^n *> r.
Proof.
  induction n; intros.
  - finish.
  - simpl_tape. follow S5_1. follow IHn. rewrite lpow_shift'. finish.
Qed.

(* ---------- finite turns ---------- *)
Lemma T1 r: 0inf <{{C}} r -->* 0inf <* [0;1] {{E}}> r.  Proof. es. Qed.
Lemma T2 l r: l {{E}}> [0;0;0] *> r -->* l <{{C}} [0;0;1] *> r.  Proof. es. Qed.
Lemma T3 l r: l {{E}}> [0;0;1] *> r -->* l <* [0;1;1] {{E}}> r.  Proof. es. Qed.
Lemma T4 l r: l {{E}}> [1;0] *> r -->* l <* [1;1] {{A}}> r.  Proof. es. Qed.
Lemma T5 l r: l {{A}}> [0;1] *> r -->* l <* [0;1] {{E}}> r.  Proof. es. Qed.
Lemma T6 l r: l {{A}}> [0;0] *> r -->* l <{{D}} [0;1] *> r.  Proof. es. Qed.
Lemma T7 l r: l <* [1;1] <{{D}} r -->* l <{{D}} [0;0] *> r.  Proof. es. Qed.
Lemma T8 l r: l <* [1;1;0;1;1] <{{D}} r -->* l <{{C}} [0;0;0;0;1] *> r.  Proof. es. Qed.
Lemma T9 l: l {{E}}> [1;0;0;1] *> 0inf -->* l <{{C}} [0;0;0] *> [1;0;0;1] *> 0inf.  Proof. es. Qed.
Lemma T10 l r: l <* [1;1] <{{C}} r -->* l <{{C}} [0;0] *> r.  Proof. es. Qed.
Lemma T11 l r: l <* [0] <{{C}} r -->* l <{{D}} [1] *> r.  Proof. es. Qed.
Lemma T12 r: 0inf <* [1;1] <{{D}} r -->* 0inf <* [0;1;1;0;1] {{E}}> r.  Proof. es. Qed.
Lemma T13 l r: l {{E}}> [1;0;1] *> r -->* l <* [0;1;1] {{E}}> r.  Proof. es. Qed.
Lemma T14 l r: l <* [1;1;0;1] <{{C}} r -->* l <{{C}} [0;1;0;0] *> r.  Proof. es. Qed.

(* ---------- digit lemmas (proof.md 2.1), mirrored from #11 ---------- *)
Lemma rot01 n (Y : side) : [0;1]^^n *> (0 >> Y) = 0 >> ([1;0]^^n *> Y).
Proof. induction n; cbn; [reflexivity|]. rewrite IHn. reflexivity. Qed.
Lemma rot10 n (Y : side) : [1;0]^^n *> (1 >> Y) = 1 >> ([0;1]^^n *> Y).
Proof. induction n; cbn; [reflexivity|]. rewrite IHn. reflexivity. Qed.
Ltac fin := apply evstep_refl'; simpl_tape; repeat (rewrite rot01 || rewrite rot10); try reflexivity.

Lemma Lb u v l r:
  l {{E}}> [1;0]^^(S v) *> [0;1]^^(S u) *> r -->*
  l <* [1;1] <* [1;0]^^v <* [0;1]^^(S u) {{E}}> r.
Proof. follow T4. follow S3. follow T5. follow S4. fin. Qed.

Lemma Lf u v l r:
  l {{E}}> [1;0]^^(S v) *> [0;0] *> [0;1]^^u *> r -->*
  l <* [1;1] <{{D}} [1;0]^^v *> [0;1]^^(S u) *> r.
Proof. follow T4. follow S3. follow T6. follow S2. fin. Qed.

Lemma Rb u v l r:
  l <* [1;1] <* [1;0]^^v <* [0;1]^^u <* [1;1] <{{D}} r -->*
  l <* [1;1] <{{D}} [1;0]^^v *> [0;0] *> [0;1]^^u *> r.
Proof. follow S5. follow T7. follow S2. fin. Qed.

Lemma Ro u v l r:
  l <* [1;1] <* [1;0]^^v <* [0;1]^^(S u) <{{C}} [0;0;0] *> r -->*
  l <{{C}} [0;0;0] *> [0;1]^^v *> [1;0]^^(S u) *> [0;0] *> r.
Proof. follow S1. follow S6. follow T10. fin. Qed.

(* ---------- the family K and the initial segment (proof.md 1, 4) ---------- *)
Inductive dg := d0 (u v : nat) | d1 (u v : nat).

(* right-side lists are nearest-cell first: d0 u v reads (10)^v 00 (01)^u from the head side *)
Definition dr (d : dg) (r : side) : side :=
  match d with
  | d0 u v => [1;0]^^v *> [0;0] *> [0;1]^^u *> r
  | d1 u v => [1;0]^^v *> [0;1]^^u *> r
  end.

(* digit lists are least significant digit first, as in #11 *)
Fixpoint app_ds (r : side) (ds : list dg) : side :=
  match ds with
  | [] => r
  | d :: t => dr d (app_ds r t)
  end.

Definition R0 : side := [1;0;0;1] *> 0inf.

Definition K (ds : list dg) (a b : nat) : Q * tape :=
  0inf <{{C}} [0;1]^^b *> [0;0;0] *> [0;1]^^a *> app_ds R0 ds.

Lemma init: c0 -->* K [d1 1 3] 4 1.
Proof. unfold K, R0. cbn. solve_init. Qed.