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.