Require Import ssim.
From BusyCoq Require Import Individual62.
Require Import Lia ZifyNat List Arith NArith.
Import ListNotations.

Open Scope nat_scope.

Definition cn (n : N) : lf := LF n [].

(* ===================================================================== *)
(* Blocks of the chain.                                                  *)
(* ===================================================================== *)

Fixpoint mkruns (b : Sym) (ns : list lf) : list run :=
  match ns with [] => [] | n :: ns' => (b, n) :: mkruns (lastb b n) ns' end.

(* gap variables of an m = 3 block: t = 4 + 4 x0, s = 4 + 4 x1, a = 1 + 4 x2, lp = 2 + 4 x3 *)
Definition vt c := LF c [4;0;0;0]%N.
Definition vs c := LF c [0;4;0;0]%N.
Definition va c := LF c [0;0;4;0]%N.
Definition vl c := LF c [0;0;0;4]%N.

Inductive lab := U0 | U1 | U2 | W0 | W1 | D0 | D1 | D2.

Definition lens (s : lab) : list lf :=
  match s with
  | U0 => [cn 3; vt 4; vs 4; va 1; vl 2]
  | U1 => [cn 3; vt 4; vs 4; va 2; vl 1]
  | U2 => [cn 3; vt 4; vs 4; va 3; vl 0]
  | W0 => [cn 3; vt 1; vs 6; va 4; vl 0]
  | W1 => [cn 3; vt 2; vs 5; va 4; vl 0]
  | D0 => [cn 3; vt 3; vs 4; va 4; vl 0]
  | D1 => [cn 2; vt 4; vs 4; va 4; vl 0]
  | D2 => [cn 1; vt 5; vs 4; va 4; vl 0]
  end%N.
Definition blk (s : lab) : list run := mkruns S0 (lens s).

(* a full block after the head has passed it leftward (now on the right of the head) *)
Definition rlens (s : lab) : list lf :=
  match s with
  | D0 => [vl 0; va 4; vs 4; vt 3; cn 3]
  | _  => [vl 0; va 3; vs 4; vt 4; cn 3]
  end%N.
Definition rblk (s : lab) : list run := mkruns S0 (rlens s).

(* block 1 (m = 1), concrete *)
Inductive lab1 := P0 | P1 | PD0 | PD1 | PD2.
Definition lens1 (s : lab1) : list lf :=
  match s with
  | P0 => [cn 3; cn 1; cn 3] | P1 => [cn 3; cn 2; cn 2] | PD0 => [cn 3; cn 3; cn 1]
  | PD1 => [cn 2; cn 4; cn 1] | PD2 => [cn 1; cn 5; cn 1]
  end%N.
Definition blk1 (s : lab1) : list run := mkruns S0 (lens1 s).
Definition rblk1 : list run := mkruns S1 [cn 1; cn 3; cn 3]%N.

(* exit phase: true = c + 2 (state A at the cut), false = c (state B) *)
Definition stp (p : bool) : Q := if p then A else B.

Definition turn (s : lab) : option (lab * bool) :=
  match s with
  | U0 => Some (U1, true) | U1 => Some (U2, true) | W0 => Some (W1, true) | W1 => Some (D0, true)
  | D1 => Some (D0, false) | D2 => Some (D1, false) | _ => None
  end.
Definition reset (s : lab) (p : bool) : option (lab * bool) :=
  match s, p with
  | U2, true => Some (U0, true) | U2, false => Some (W0, true) | D0, false => Some (D2, false)
  | _, _ => None
  end.
Definition turn1 (s : lab1) : option (lab1 * bool) :=
  match s with
  | P0 => Some (P1, true) | P1 => Some (PD0, true) | PD1 => Some (PD0, false) | PD2 => Some (PD1, false)
  | PD0 => None
  end.

Definition sg2 (L R : side) : nat -> side := fun k => match k with O => L | _ => R end.

Lemma reach_LR fuel q q' l l' nu L R :
  reach fuel (Lc q (l, TV 0) ([], TV 1)) (Rc q' (l', TV 0) ([], TV 1)) = true ->
  ev_runs nu l L <{{q}} R -->+ ev_runs nu l' L {{q'}}> R.
Proof. intros H. exact (reach_spec _ _ _ H nu (sg2 L R)). Qed.

Lemma reach_LL fuel q q' l r' nu L R :
  reach fuel (Lc q (l, TV 0) ([], TV 1)) (Lc q' ([], TV 0) (r', TV 1)) = true ->
  ev_runs nu l L <{{q}} R -->+ L <{{q'}} ev_runs nu r' R.
Proof. intros H. exact (reach_spec _ _ _ H nu (sg2 L R)). Qed.

Lemma reach_RR fuel q q' r l' nu L R :
  reach fuel (Rc q ([], TV 0) (r, TV 1)) (Rc q' (l', TV 0) ([], TV 1)) = true ->
  L {{q}}> ev_runs nu r R -->+ ev_runs nu l' L {{q'}}> R.
Proof. intros H. exact (reach_spec _ _ _ H nu (sg2 L R)). Qed.

Lemma blk_turn s s' p nu L R : turn s = Some (s', p) ->
  ev_runs nu (blk s) L <{{D}} R -->+ ev_runs nu (blk s') L {{stp p}}> R.
Proof.
  intros H. destruct s; cbn in H; inversion H; subst; clear H; cbn [stp];
    apply (reach_LR 100); vm_compute; reflexivity.
Qed.

Lemma blk_pass s nu L R : turn s = None ->
  ev_runs nu (blk s) L <{{D}} R -->+ L <{{D}} ev_runs nu (rblk s) R.
Proof.
  intros H. destruct s; cbn in H; inversion H; apply (reach_LL 100); vm_compute; reflexivity.
Qed.

Lemma blk_reset s p s' p' nu L R : reset s p = Some (s', p') ->
  L {{stp p}}> ev_runs nu (rblk s) R -->+ ev_runs nu (blk s') L {{stp p'}}> R.
Proof.
  intros H. destruct s, p; cbn in H; inversion H; subst; clear H; cbn [stp];
    apply (reach_RR 100); vm_compute; reflexivity.
Qed.

Lemma blk1_turn s s' p L R : turn1 s = Some (s', p) ->
  ev_runs [] (blk1 s) L <{{D}} R -->+ ev_runs [] (blk1 s') L {{stp p}}> R.
Proof.
  intros H. destruct s; cbn in H; inversion H; subst; clear H; cbn [stp];
    apply (reach_LR 100); vm_compute; reflexivity.
Qed.

Lemma blk1_pass L R : ev_runs [] (blk1 PD0) L <{{D}} R -->+ L <{{E}} ev_runs [] rblk1 R.
Proof. refine (reach_LL 100 D E (blk1 PD0) rblk1 [] L R _). vm_compute. reflexivity. Qed.

Lemma blk1_back L R : L {{B}}> ev_runs [] rblk1 R -->+ ev_runs [] (blk1 PD2) L {{B}}> R.
Proof. refine (reach_RR 100 B B rblk1 (blk1 PD2) [] L R _). vm_compute. reflexivity. Qed.

(* ===================================================================== *)
(* The left word: a 4-digit ternary counter (episodes 0..79), and the    *)
(* left record (episode 80).                                             *)
(* ===================================================================== *)

Definition dgr (v : nat) : list run :=
  match v with
  | O => [(S0, cn 1); (S0, cn 5)]
  | S O => [(S0, cn 2); (S1, cn 4)]
  | _ => [(S0, cn 3); (S0, cn 3)]
  end%N.

Definition lw (i : nat) : list run :=
  if Nat.ltb i 81 then
    [(S1, cn 3); (S1, cn 4)] ++ dgr (i mod 3) ++ dgr (i / 3 mod 3) ++ dgr (i / 9 mod 3) ++ dgr (i / 27 mod 3)
      ++ [(S0, cn 2)]
  else [(S0, cn 6); (S1, cn 4)] ++ dgr 0 ++ dgr 0 ++ dgr 0 ++ dgr 0 ++ [(S0, cn 2)].

Definition LWs (i : nat) : side := ev_runs [] (lw i) (const S0).

Lemma reach_T0 fuel q q' l l' (Y : side) :
  reach fuel (Lc q (l, T0) ([], TV 0)) (Rc q' (l', T0) ([], TV 0)) = true ->
  ev_runs [] l (const S0) <{{q}} Y -->+ ev_runs [] l' (const S0) {{q'}}> Y.
Proof. intros H. exact (reach_spec _ _ _ H [] (fun _ => Y)). Qed.

Definition lw_ok (i : nat) : bool := reach 1000 (Lc E (lw i, T0) ([], TV 0)) (Rc B (lw (S i), T0) ([], TV 0)).

Lemma lw_all : forallb lw_ok (seq 0 81) = true.
Proof. vm_compute. reflexivity. Qed.

Lemma lw_ok_spec i Y : lw_ok i = true ->
  ev_runs [] (lw i) (const S0) <{{E}} Y -->+ ev_runs [] (lw (S i)) (const S0) {{B}}> Y.
Proof. exact (reach_T0 1000 E B (lw i) (lw (S i)) Y). Qed.

Lemma lw_ok_lt i : i < 81 -> lw_ok i = true.
Proof. intros Hi. pose proof lw_all as H. rewrite forallb_forall in H. apply H, in_seq. lia. Qed.

Lemma lw_ep i Y : i < 81 -> LWs i <{{E}} Y -->+ LWs (S i) {{B}}> Y.
Proof. intros Hi. apply lw_ok_spec, lw_ok_lt, Hi. Qed.

(* ===================================================================== *)
(* The chain: m = 3 blocks (nearest the head first), then block 1, then  *)
(* the left word.                                                        *)
(* ===================================================================== *)

Fixpoint chs (ls : list lab) (nus : list (list N)) (L : side) : side :=
  match ls, nus with
  | s :: ls', nu :: nus' => ev_runs nu (blk s) (chs ls' nus' L)
  | _, _ => L
  end.

Fixpoint rchs (ls : list lab) (nus : list (list N)) (R : side) : side :=
  match ls, nus with
  | s :: ls', nu :: nus' => rchs ls' nus' (ev_runs nu (rblk s) R)
  | _, _ => R
  end.

Fixpoint visit3 (ls : list lab) : option (list lab * bool) :=
  match ls with
  | [] => None
  | s :: ls' =>
    match turn s with
    | Some (s', p) => Some (s' :: ls', p)
    | None =>
      match visit3 ls' with
      | Some (ls'', p') => match reset s p' with Some (s'', p'') => Some (s'' :: ls'', p'') | None => None end
      | None => None
      end
    end
  end.

Fixpoint cb (ls : list lab) (p : bool) : option (list lab * bool) :=
  match ls with
  | [] => Some ([], p)
  | s :: ls' =>
    match cb ls' p with
    | Some (ls'', p') => match reset s p' with Some (s'', p'') => Some (s'' :: ls'', p'') | None => None end
    | None => None
    end
  end.

Definition fullb (s : lab) : bool := match turn s with None => true | Some _ => false end.

Lemma visit3_spec ls : forall ls' p nus L R, visit3 ls = Some (ls', p) -> length ls = length nus ->
  chs ls nus L <{{D}} R -->+ chs ls' nus L {{stp p}}> R.
Proof.
  induction ls as [|s ls IH]; intros ls' p nus L R H Hl; [discriminate|].
  destruct nus as [|nu nus]; [discriminate|]. cbn in Hl. injection Hl as Hl.
  cbn [visit3] in H.
  destruct (turn s) as [[s1 p1]|] eqn:Et.
  - inversion H; subst. cbn [chs]. apply blk_turn, Et.
  - destruct (visit3 ls) as [[ls1 p1]|] eqn:Ev; [|discriminate].
    destruct (reset s p1) as [[s2 p2]|] eqn:Er; [|discriminate].
    inversion H; subst; clear H. cbn [chs].
    eapply progress_trans; [apply blk_pass, Et|].
    eapply progress_trans; [apply (IH _ _ _ _ _ eq_refl Hl)|].
    apply blk_reset, Er.
Qed.

Lemma pass_spec ls : forall nus L R, forallb fullb ls = true -> length ls = length nus ->
  chs ls nus L <{{D}} R -->* L <{{D}} rchs ls nus R.
Proof.
  induction ls as [|s ls IH]; intros nus L R H Hl.
  - destruct nus; [apply evstep_refl | discriminate].
  - destruct nus as [|nu nus]; [discriminate|]. cbn in Hl. injection Hl as Hl.
    cbn [forallb] in H. apply andb_prop in H as [H1 H2].
    cbn [chs rchs].
    eapply evstep_trans; [apply progress_evstep, blk_pass|].
    + unfold fullb in H1. destruct (turn s); [discriminate | reflexivity].
    + apply IH; assumption.
Qed.

Lemma cb_spec ls : forall p ls' p' nus L R, cb ls p = Some (ls', p') -> length ls = length nus ->
  L {{stp p}}> rchs ls nus R -->* chs ls' nus L {{stp p'}}> R.
Proof.
  induction ls as [|s ls IH]; intros p ls' p' nus L R H Hl.
  - destruct nus; [|discriminate]. inversion H; subst. apply evstep_refl.
  - destruct nus as [|nu nus]; [discriminate|]. cbn in Hl. injection Hl as Hl.
    cbn [cb] in H.
    destruct (cb ls p) as [[ls1 p1]|] eqn:Ec; [|discriminate].
    destruct (reset s p1) as [[s2 p2]|] eqn:Er; [|discriminate].
    inversion H; subst; clear H. cbn [chs rchs].
    eapply evstep_trans; [apply (IH _ _ _ _ _ _ Ec Hl)|].
    apply progress_evstep, blk_reset, Er.
Qed.

Lemma visit3_len ls : forall ls' p, visit3 ls = Some (ls', p) -> length ls' = length ls.
Proof.
  induction ls as [|s ls IH]; intros ls' p H; [discriminate|]. cbn in H.
  destruct (turn s) as [[s1 p1]|]; [inversion H; reflexivity|].
  destruct (visit3 ls) as [[ls1 p1]|] eqn:E; [|discriminate].
  destruct (reset s p1) as [[s2 p2]|]; [|discriminate].
  inversion H; subst. cbn. rewrite (IH _ _ eq_refl). reflexivity.
Qed.

Lemma cb_len ls : forall p ls' p', cb ls p = Some (ls', p') -> length ls' = length ls.
Proof.
  induction ls as [|s ls IH]; intros p ls' p' H; cbn in H; [inversion H; reflexivity|].
  destruct (cb ls p) as [[ls1 p1]|] eqn:E; [|discriminate].
  destruct (reset s p1) as [[s2 p2]|]; [|discriminate].
  inversion H; subst. cbn. rewrite (IH _ _ _ E). reflexivity.
Qed.

(* ===================================================================== *)
(* One visit of the whole chain (Lemma C, C', and the left episodes).   *)
(* ===================================================================== *)

Definition vst : Type := (list lab * lab1 * nat)%type.

Definition lab1_eqb (a b : lab1) : bool :=
  match a, b with P0, P0 | P1, P1 | PD0, PD0 | PD1, PD1 | PD2, PD2 => true | _, _ => false end.

Definition vis (st : vst) : option (vst * bool) :=
  let '(ls, b, i) := st in
  match visit3 ls with
  | Some (ls', p) => Some ((ls', b, i), p)
  | None =>
    if forallb fullb ls then
      match turn1 b with
      | Some (b', p1) => match cb ls p1 with Some (ls', p) => Some ((ls', b', i), p) | None => None end
      | None =>
        if andb (lab1_eqb b PD0) (Nat.ltb i 80) then
          match cb ls false with Some (ls', p) => Some ((ls', PD2, S i), p) | None => None end
        else None
      end
    else None
  end.

Definition b1s (b : lab1) (X : side) : side := ev_runs [] (blk1 b) X.

Definition Gc (st : vst) (nus : list (list N)) (R : side) : Q * tape :=
  let '(ls, b, i) := st in chs ls nus (b1s b (LWs i)) <{{D}} R.
Definition Gx (st : vst) (nus : list (list N)) (p : bool) (R : side) : Q * tape :=
  let '(ls, b, i) := st in chs ls nus (b1s b (LWs i)) {{stp p}}> R.

Definition vlen (st : vst) : nat := let '(ls, _, _) := st in length ls.

Lemma lab1_eqb_eq a b : lab1_eqb a b = true -> a = b.
Proof. destruct a, b; cbn; congruence. Qed.

Lemma vis_spec st st' p nus R : vis st = Some (st', p) -> vlen st = length nus ->
  Gc st nus R -->+ Gx st' nus p R /\ vlen st' = vlen st.
Proof.
  destruct st as [[ls b] i]. cbn [vis vlen]. intros H Hl.
  destruct (visit3 ls) as [[ls1 p1]|] eqn:Ev.
  - inversion H; subst; clear H. cbn [Gc Gx vlen]. split.
    + apply visit3_spec; assumption.
    + apply (visit3_len _ _ _ Ev).
  - destruct (forallb fullb ls) eqn:Ef; [|discriminate].
    destruct (turn1 b) as [[b1 p1]|] eqn:Et.
    + destruct (cb ls p1) as [[ls1 p2]|] eqn:Ec; [|discriminate].
      inversion H; subst; clear H. cbn [Gc Gx vlen]. split; [|apply (cb_len _ _ _ _ Ec)].
      eapply evstep_progress_trans; [apply pass_spec; assumption|].
      unfold b1s at 1. eapply progress_evstep_trans; [apply blk1_turn, Et|].
      apply cb_spec; assumption.
    + destruct (andb (lab1_eqb b PD0) (Nat.ltb i 80)) eqn:Eb; [|discriminate].
      apply andb_prop in Eb as [Eb Ei]. apply lab1_eqb_eq in Eb. subst b. apply Nat.ltb_lt in Ei.
      destruct (cb ls false) as [[ls1 p2]|] eqn:Ec; [|discriminate].
      inversion H; subst; clear H. cbn [Gc Gx vlen]. split; [|apply (cb_len _ _ _ _ Ec)].
      eapply evstep_progress_trans; [apply pass_spec; assumption|].
      unfold b1s at 1. eapply progress_trans; [apply blk1_pass|].
      eapply progress_trans; [apply lw_ep; lia|].
      eapply progress_evstep_trans; [apply blk1_back|].
      apply (cb_spec _ false); assumption.
Qed.

(* ===================================================================== *)
(* Right-region episodes, abstractly.                                    *)
(* ===================================================================== *)

Definition Ep (p : bool) (R R' : side) : Prop := forall l, l {{stp p}}> R -->* l <{{D}} R'.

Fixpoint EpSeq (ps : list bool) (R R' : side) : Prop :=
  match ps with
  | [] => R = R'
  | p :: ps' => exists R1, Ep p R R1 /\ EpSeq ps' R1 R'
  end.

Fixpoint runv (n : nat) (st : vst) : option (vst * list bool) :=
  match n with
  | O => Some (st, [])
  | S n' =>
    match vis st with
    | Some (st1, p) => match runv n' st1 with Some (st2, ps) => Some (st2, p :: ps) | None => None end
    | None => None
    end
  end.

Lemma runv_spec n : forall st st' ps nus R R', runv n st = Some (st', ps) -> vlen st = length nus ->
  EpSeq ps R R' -> Gc st nus R -->* Gc st' nus R'.
Proof.
  induction n as [|n IH]; intros st st' ps nus R R' H Hl HE.
  - cbn in H. inversion H; subst. cbn in HE. subst. apply evstep_refl.
  - cbn [runv] in H.
    destruct (vis st) as [[st1 p]|] eqn:Ev; [|discriminate].
    destruct (runv n st1) as [[st2 ps2]|] eqn:Er; [|discriminate].
    inversion H; subst; clear H.
    destruct HE as [R1 [HE1 HE2]].
    destruct (vis_spec _ _ _ nus R Ev Hl) as [H1 H2].
    eapply evstep_trans; [apply progress_evstep, H1|].
    eapply evstep_trans; [|apply (IH st1 st' ps2 nus R1 R' Er); [congruence | exact HE2]].
    destruct st1 as [[ls1 b1] i1]. cbn [Gx Gc]. apply HE1.
Qed.