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

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

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.

(** ** Tokens *)
Inductive tok := T0 | T1 | TZ.
Definition tokw (t : tok) : list Sym :=
  match t with T0 => [0;0] | T1 => [0;1] | TZ => [1;0;0] end.
Fixpoint tw (ts : list tok) : list Sym :=
  match ts with [] => [] | t :: ts => tokw t ++ tw ts end.

Inductive ptok := P | PZ.
Definition pw (p : ptok) : list Sym := match p with P => [0;1] | PZ => [0;1;0] end.
Fixpoint pl (ps : list ptok) : list Sym :=
  match ps with [] => [] | p :: ps => pw p ++ pl ps end.
Definition proc (t : tok) : ptok := match t with TZ => PZ | _ => P end.

Lemma tw_app xs ys : tw (xs ++ ys) = tw xs ++ tw ys.
Proof. induction xs; cbn; [reflexivity|]. rewrite IHxs, app_assoc. reflexivity. Qed.
Lemma tw_cons x xs : tw (x :: xs) = tokw x ++ tw xs.
Proof. reflexivity. Qed.
Lemma pl_app xs ys : pl (xs ++ ys) = pl xs ++ pl ys.
Proof. induction xs; cbn; [reflexivity|]. rewrite IHxs, app_assoc. reflexivity. Qed.

(** ** Window lemmas *)
Lemma AT0 l r : l {{A}}> [0;0] *> r -->* l <* [0;1] {{C}}> r.  Proof. es. Qed.
Lemma CT1 l r : l {{C}}> [0;1] *> r -->* l <* [0;1] {{C}}> r.  Proof. es. Qed.
Lemma CTZ l r : l {{C}}> [1;0;0] *> r -->* l <* [0;1;0] {{C}}> r.  Proof. es. Qed.
Lemma CT0 l r : l {{C}}> [0;0] *> r -->* l <{{E}} [0;1] *> r.  Proof. es. Qed.
Lemma EPZ l r : l <* [0;1;0] <{{E}} r -->* l <{{E}} [1;0;0] *> r.  Proof. es. Qed.
Lemma EP l r : l <* [0;1] <{{E}} r -->* l <{{F}} [0;0] *> r.  Proof. es. Qed.
Lemma FP l r : l <* [0;1] <{{F}} r -->* l <{{E}} [0;1] *> r.  Proof. es. Qed.
Lemma FPZP l r : l <* [0;1] <* [0;1;0] <{{F}} [0;0] *> r -->*
  l <{{E}} [0;0] *> [1;0;0] *> [0;1] *> r.  Proof. es. Qed.
Lemma ENDl l r : l <* [0;0] <{{F}} r -->* l <{{A}} [0;1] *> r.  Proof. es. Qed.
Lemma B1 l r : l <* [1;0] <{{F}} r -->* l <* [0;0] {{A}}> r.  Proof. es. Qed.
Lemma BN l r : l <* [0;1;0;0;1;0] <{{F}} [0;0] *> r -->* l <{{A}} [0;0;0;1;0;0;0;1] *> r.  Proof. es. Qed.
Lemma ENDZX l r : l <* [0;0;1;0;0;1;0;1;0;0;1;0] <{{F}} r -->* l <{{A}} [0;0;0;1;0;0;0;1;1;0;0;1] *> r.  Proof. es. Qed.

(** ** C sweep over T1/TZ tokens *)
Fixpoint noT0 (ts : list tok) : Prop :=
  match ts with [] => True | T0 :: _ => False | _ :: ts => noT0 ts end.
Definition prc (ts : list tok) : list ptok := rev (map proc ts).

Lemma Csweep ts : noT0 ts -> forall l r,
  l {{C}}> tw ts *> r -->* l <* pl (prc ts) {{C}}> r.
Proof.
  induction ts as [|t ts IH]; intros H l r; [finish|].
  unfold prc. cbn [map rev]. rewrite pl_app. cbn [tw].
  rewrite Str_app_assoc.
  destruct t; cbn in H; [contradiction| |].
  - follow CT1. follow (IH H). cbn [pl proc]. rewrite Str_app_assoc. finish.
  - follow CTZ. follow (IH H). cbn [pl proc]. rewrite Str_app_assoc. finish.
Qed.

(** ** The leftward return over processed tokens *)
Fixpoint retf (m : Q) (ps : list ptok) (rs : list tok) {struct ps} : Q * list ptok * list tok :=
  match m, ps with
  | E, PZ :: ps' => retf E ps' (TZ :: rs)
  | E, P :: ps' => retf F ps' (T0 :: rs)
  | F, P :: ps' => retf E ps' (T1 :: rs)
  | F, PZ :: P :: ps' =>
      match rs with
      | T0 :: rs' => retf E ps' (T0 :: TZ :: T1 :: rs')
      | _ => (m, ps, rs)
      end
  | _, _ => (m, ps, rs)
  end.

Lemma retf_spec_n n : forall ps, length ps <= n -> forall m rs m' ps' rs',
  retf m ps rs = (m', ps', rs') -> forall l r,
  l <* pl ps <{{m}} tw rs *> r -->* l <* pl ps' <{{m'}} tw rs' *> r.
Proof.
  induction n as [|n IH]; intros ps Hn m rs m' ps' rs' Hr l r.
  - destruct ps; [|cbn in Hn; lia].
    destruct m; cbn in Hr; inversion Hr; subst; finish.
  - destruct ps as [|p ps].
    { destruct m; cbn in Hr; inversion Hr; subst; finish. }
    cbn in Hn.
    destruct m, p; cbn in Hr; try (inversion Hr; subst; solve [finish]).
    + (* E, P *)
      cbn [pl]. rewrite Str_app_assoc. cbn [pw].
      follow EP. apply (IH ps ltac:(lia) _ _ _ _ _ Hr).
    + (* E, PZ *)
      cbn [pl]. rewrite Str_app_assoc. cbn [pw].
      follow EPZ. apply (IH ps ltac:(lia) _ _ _ _ _ Hr).
    + (* F, P *)
      cbn [pl]. rewrite Str_app_assoc. cbn [pw].
      follow FP. apply (IH ps ltac:(lia) _ _ _ _ _ Hr).
    + (* F, PZ *)
      destruct ps as [|[|] ps]; try (inversion Hr; subst; solve [finish]).
      destruct rs as [|[| |] rs]; try (inversion Hr; subst; solve [finish]).
      cbn [pl tw]. rewrite !Str_app_assoc. cbn [pw tokw].
      cbn in Hn.
      follow FPZP.
      assert (H := IH ps ltac:(lia) _ _ _ _ _ Hr l r).
      cbn [tw] in H. rewrite !Str_app_assoc in H. exact H.
Qed.

Lemma retf_spec ps m rs m' ps' rs' :
  retf m ps rs = (m', ps', rs') -> forall l r,
  l <* pl ps <{{m}} tw rs *> r -->* l <* pl ps' <{{m'}} tw rs' *> r.
Proof. intros. eapply retf_spec_n; [apply le_n|eassumption]. Qed.

(** ** Shift rules *)
Lemma CTZ' l r : l <* [] {{C}}> [1;0;0] *> r -->* l <* [0;1;0] <* [] {{C}}> r.  Proof. es. Qed.
Definition CTZs := shift_rule_R _ _ _ _ _ CTZ'.
Lemma EPZ' l r : l <* [0;1;0] <{{E}} [] *> r -->* l <{{E}} [] *> [1;0;0] *> r.  Proof. es. Qed.
Definition EPZs := shift_rule_L _ _ _ _ _ EPZ'.

Lemma tw_Z g : tw (repeat TZ g) = [1;0;0]^^g.
Proof. induction g; cbn; [reflexivity|]. rewrite IHg. reflexivity. Qed.

(** ** The counter: digits b Z 1 Z^g, LSB first; the last digit is its bit only *)
Definition bit (v : nat) : tok := if Nat.odd v then T1 else T0.
Fixpoint ctr (gs : list nat) (v : nat) : list tok :=
  match gs with
  | [] => [bit v]
  | g :: gs' => bit v :: TZ :: T1 :: repeat TZ g ++ ctr gs' (Nat.div2 v)
  end.

Lemma bit_even w : bit (2*w) = T0.
Proof. unfold bit. rewrite Nat.odd_even. reflexivity. Qed.
Lemma bit_odd w : bit (S (2*w)) = T1.
Proof. unfold bit. replace (S (2*w)) with (2*w+1) by lia. rewrite Nat.odd_odd. reflexivity. Qed.

Lemma ctr_even g gs w : ctr (g :: gs) (2*w) = T0 :: TZ :: T1 :: repeat TZ g ++ ctr gs w.
Proof. cbn [ctr]. rewrite bit_even, Nat.div2_double. reflexivity. Qed.
Lemma ctr_odd g gs w : ctr (g :: gs) (S (2*w)) = T1 :: TZ :: T1 :: repeat TZ g ++ ctr gs w.
Proof. cbn [ctr]. rewrite bit_odd, Nat.div2_succ_double. reflexivity. Qed.

Lemma ctr_hd_even gs w : exists rest, ctr gs (2*w) = T0 :: rest /\ ctr gs (S (2*w)) = T1 :: rest.
Proof.
  destruct gs as [|g gs].
  - exists (@nil tok). cbn [ctr]. rewrite bit_even, bit_odd. auto.
  - eexists. rewrite ctr_even, ctr_odd. split; reflexivity.
Qed.

Lemma pow2S n : 2 ^ S n = 2 * 2 ^ n.
Proof. apply Nat.pow_succ_r'. Qed.

Lemma IncC gs : forall v, S v < 2 ^ S (length gs) -> forall l r t,
  l {{C}}> tw (ctr gs v ++ t) *> r -->* l <{{E}} tw (ctr gs (S v) ++ t) *> r.
Proof.
  induction gs as [|g gs IH]; intros v Hv l r t;
  destruct (Nat.Even_or_Odd v) as [[w ->]|[w ->]].
  - cbn [ctr app tw]. rewrite bit_even. replace (S (2*w)) with (2*w+1) by lia.
    unfold bit. rewrite Nat.odd_odd. cbn [tokw]. rewrite !Str_app_assoc. apply CT0.
  - cbn [length] in Hv. rewrite pow2S in Hv. cbn in Hv. lia.
  - destruct (ctr_hd_even (g :: gs) w) as (rest & E0 & E1).
    rewrite E0, E1. cbn [app tw]. rewrite !Str_app_assoc. apply CT0.
  - replace (2*w+1) with (S (2*w)) by lia. rewrite ctr_odd.
    replace (S (S (2*w))) with (2 * S w) by lia. rewrite ctr_even.
    cbn [length] in Hv. rewrite !pow2S in Hv.
    cbn [app]. rewrite <- !app_assoc. cbn [tw].
    rewrite !(tw_app (repeat TZ g)), tw_Z, !Str_app_assoc. cbn [tokw].
    follow CT1. follow CTZ. follow CT1.
    follow CTZs.
    follow (IH w ltac:(rewrite pow2S; lia)).
    follow EPZs. follow EP. follow FPZP. finish.
Qed.

Lemma IncL gs v a : S v < 2 ^ S (length gs) -> forall l r t,
  l {{A}}> tw (T0 :: repeat TZ a ++ ctr gs v ++ t) *> r -->*
  l <{{F}} tw (T0 :: repeat TZ a ++ ctr gs (S v) ++ t) *> r.
Proof.
  intros Hv l r t.
  cbn [tw]. rewrite !(tw_app (repeat TZ a)), tw_Z, !Str_app_assoc. cbn [tokw].
  follow AT0. follow CTZs.
  follow (IncC gs v Hv).
  follow EPZs. follow EP. finish.
Qed.

(** ** The left bounce: F at the edge adds one 100 to the lead and returns to A *)
Lemma Bnc X : (const 0) <{{F}} [0;0] *> [1;0;0] *> X -->*
  (const 0) {{A}}> [0;0] *> [1;0;0] *> [1;0;0] *> X.
Proof. rewrite (const_unfold _ 0) at 1. es. Qed.

(** ** Normal-mode increment: one bounce, lead a -> a+1, counter v -> v+1 *)
Lemma Inc gs v a : S v < 2 ^ S (length gs) -> forall t,
  (const 0) {{A}}> tw (T0 :: repeat TZ (S a) ++ ctr gs v ++ t) *> (const 0) -->*
  (const 0) {{A}}> tw (T0 :: repeat TZ (S (S a)) ++ ctr gs (S v) ++ t) *> (const 0).
Proof.
  intros Hv t.
  follow (IncL gs v (S a) Hv).
  (* 0inf <F tw(T0 :: 100^(S a) ++ ctr(Sv) ++ t) ; peel 00 100 and bounce *)
  cbn [repeat app]. rewrite !tw_cons. cbn [tokw]. rewrite !Str_app_assoc.
  follow Bnc. finish.
Qed.

(** ** Overflow return: C sweeps a T0-free word, turns at the next 0, then retf returns.
    This is the whole tail table T(f) of the write-up, with no 2^14-entry table: the head
    stops at the first 0 of the tail and the leftward return is the finite automaton [retf]. *)
Lemma OvRet w rest : noT0 w ->
  forall m' ps' rs', retf E (prc w ++ [P]) (T1 :: rest) = (m', ps', rs') ->
  forall l r,
  l {{A}}> tw (T0 :: w ++ T0 :: rest) *> r -->*
  l <* pl ps' <{{m'}} tw rs' *> r.
Proof.
  intros Hw m' ps' rs' Hr l r.
  rewrite tw_cons. cbn [tokw]. rewrite (tw_app w (T0 :: rest)), !Str_app_assoc.
  follow AT0.
  follow (Csweep w Hw).
  rewrite tw_cons. cbn [tokw]. rewrite Str_app_assoc.
  follow CT0.
  (* now:  l <* [0;1] <* pl (prc w) <{{E}} [0;1] *> tw rest *> r *)
  assert (H := retf_spec (prc w ++ [P]) E (T1 :: rest) m' ps' rs' Hr l r).
  rewrite pl_app in H. cbn [pl pw] in H.
  cbn [tw tokw] in H.
  rewrite !Str_app_assoc in H.
  follow H. finish.
Qed.