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

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

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.

(* rotation of a power by one cell *)
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 lshift (xs : list sym) n (l : side) : l <* xs <* xs^^n = l <* xs^^(S n).
Proof.
  cbn. rewrite <-Str_app_assoc, lpow_shift. reflexivity.
Qed.

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

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

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

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


Lemma p01 n (Y : side) : [0;1]^^n *> 0 >> 1 >> Y = 0 >> 1 >> [0;1]^^n *> Y.
Proof. exact (lpow_shift' _ n [0;1] Y). Qed.
Lemma p10 n (Y : side) : [1;0]^^n *> 1 >> 0 >> Y = 1 >> 0 >> [1;0]^^n *> Y.
Proof. exact (lpow_shift' _ n [1;0] Y). 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.

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

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

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

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

(* right-edge chunk shared by M and O: (10)^a 000 (10)^b B> 0^inf -> <E (01)^a 011 (01)^(b+2) 0^inf *)
Lemma chunkA a b l:
  l <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf -->+
  l <{{E}} [0;1]^^a *> [0;1;1] *> [0;1]^^(S (S b)) *> 0inf.
Proof. es. Qed.

(* end of M: C> 11 (01)^a 011 (01)^(b+2) 0^inf -> (10)^(a+1) 000 (10)^(b+2) B> 0^inf *)
Lemma chunkC a b l:
  l {{C}}> [1;1] *> [0;1]^^a *> [0;1;1] *> [0;1]^^(S (S b)) *> 0inf -->*
  l <* [0;1]^^(S a) <* [0;0;0] <* [0;1]^^(S (S b)) {{B}}> 0inf.
Proof.
  follow S5. follow T8. follow S1. fin.
Qed.

(* end of O: 000 B> (01)^(a+1) 011 (01)^(b+2) 0^inf -> 10 (01)^(a+1) (10)^(b+3) 000 10 B> 0^inf *)
Lemma chunkO a b l:
  l <* [0;0;0] {{B}}> [0;1]^^(S a) *> [0;1;1] *> [0;1]^^(S (S b)) *> 0inf -->*
  l <* [0;1] <* [1;0]^^(S a) <* [0;1]^^(S (S (S b))) <* [0;0;0] <* [0;1] {{B}}> 0inf.
Proof.
  follow S1. follow T11. follow S5. follow T12. follow S4. follow T13. follow S4. follow T2. follow S1. follow S1_1.
  rewrite (rot01 (S (S b))).
  follow (S6 (l <* [0;0;1] <* [0;1]^^a <* [1]) ([1;1;0;1] *> 0inf) (S (S (S b)))).
  follow T14. fin.
Qed.

(* ---------- the digit list ---------- *)
Inductive dg := d0 (u v : nat) | d1 (u v : nat).

(* left-side lists are written nearest-cell first: (10)^u is [0;1]^^u, (01)^v is [1;0]^^v *)
Definition dl (d : dg) (l : side) : side :=
  match d with
  | d0 u v => l <* [0;1]^^u <* [0;0] <* [1;0]^^v
  | d1 u v => l <* [0;1]^^u <* [1;0]^^v
  end.

(* digit lists are least significant digit first *)
Fixpoint app_ds (l : side) (ds : list dg) : side :=
  match ds with
  | [] => l
  | d :: t => dl d (app_ds l t)
  end.

Definition L0 : side := 0inf <* [1;0;0;1].

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

Definition map1 (os : list (nat*nat)) := map (fun '(u,v) => d1 (S u) (S v)) os.
Definition map0 (os : list (nat*nat)) := map (fun '(u,v) => d0 (S u) v) os.

Fixpoint rw (os : list (nat*nat)) (r : side) : side :=
  match os with
  | [] => r
  | (u,v) :: t => rw t ([0;1]^^(S u) *> [1;0]^^v *> [1;1] *> r)
  end.

Lemma app_ds_app l xs ys : app_ds l (xs ++ ys) = app_ds (app_ds l ys) xs.
Proof. induction xs; cbn; congruence. Qed.

Lemma LbS os: forall l r, app_ds l (map1 os) <{{E}} r -->* l <{{E}} rw os r.
Proof.
  induction os as [|[u v] t IH]; intros.
  - finish.
  - cbn [map1 map app_ds dl rw]. follow Lb. apply IH.
Qed.

Lemma RbS os: forall l r, l {{C}}> [1;1] *> rw os r -->* app_ds l (map0 os) {{C}}> [1;1] *> r.
Proof.
  induction os as [|[u v] t IH]; intros.
  - finish.
  - cbn [map0 map app_ds dl rw]. follow IH. apply Rb.
Qed.

Fixpoint ro_out (os : list (nat*nat)) (l : side) : side :=
  match os with
  | [] => l
  | (u,v) :: t => ro_out t l <* [0;0] <* [1;0]^^(S u) <* [0;1]^^v
  end.

Lemma RoS os: forall l r, l <* [0;0;0] {{B}}> rw os r -->* ro_out os l <* [0;0;0] {{B}}> r.
Proof.
  induction os as [|[u v] t IH]; intros.
  - finish.
  - cbn [ro_out rw]. follow IH. apply Ro.
Qed.

Fixpoint Oz (t : list (nat*nat)) (u : nat) : list dg :=
  match t with
  | [] => [d0 0 u]
  | (a, b) :: t' => d0 b u :: Oz t' (S a)
  end.

Definition Oout (os : list (nat*nat)) (A : nat) : list dg :=
  match os with
  | [] => []
  | (u, v) :: t => d1 (S v) A :: Oz t (S u)
  end.

Lemma Ozeq t: forall u l, ro_out t l <* [0;0] <* [1;0]^^u = app_ds l (Oz t u).
Proof.
  induction t as [|[a b] t IH]; intros.
  - reflexivity.
  - cbn [ro_out Oz app_ds dl]. rewrite <- IH. reflexivity.
Qed.

(* M: carry *)
Lemma M_spec os u v rest a b:
  K (map1 os ++ d0 u (S v) :: rest) a b -->+
  K (map0 os ++ d1 (S u) v :: rest) (S a) (S (S b)).
Proof.
  unfold K. rewrite !app_ds_app.
  follow10 chunkA.
  follow LbS.
  cbn [app_ds dl].
  follow Lf.
  follow RbS.
  apply chunkC.
Qed.

(* M with the flipped digit dropping: (u+1,1,0) fuses into the digit below it *)
Lemma Mdrop_spec os u2 v2 u rest a b:
  K (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) a b -->+
  K (map0 os ++ d0 (S u2 + S u) v2 :: rest) (S a) (S (S b)).
Proof.
  follow10 (M_spec (os ++ [(u2,v2)]) u 0 rest a b).
  assert (E: app_ds L0 (map0 (os ++ [(u2,v2)]) ++ d1 (S u) 0 :: rest) =
             app_ds L0 (map0 os ++ d0 (S u2 + S u) v2 :: rest)).
  { unfold map0. rewrite map_app, <- app_assoc. cbn [map app].
    rewrite !app_ds_app. f_equal. cbn [app_ds dl].
    rewrite (lpow_add _ (S u2) (S u)), Str_app_assoc. reflexivity. }
  unfold K. rewrite E. finish.
Qed.

(* O: overflow *)
Lemma O_spec os a b: os <> [] ->
  K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1.
Proof.
  intro H. destruct os as [|[u v] t]; [congruence|].
  unfold K.
  follow10 chunkA.
  follow LbS.
  follow T9.
  follow RoS.
  follow chunkO.
  apply evstep_refl'. cbn [Oout app_ds dl ro_out]. rewrite <- Ozeq. reflexivity.
Qed.

Lemma init: c0 -->* K [d1 1 2] 8 5.
Proof. unfold K, L0. cbn. solve_init. Qed.