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 "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF").

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.

(* R1: l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r --> l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r *)
Lemma tR1 n m x l r :
  l <* [1]^^(S (S n)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> [1]^^x *> [0] *> r -->+
  l <* [1]^^(S n) <* [0] <* [1]^^(S m) <{{A}} [0] *> [1]^^(S x) *> [0;0] *> r.
Proof. es. Qed.

(* R3: l 0 <A 0 1^(k+1) 0 0 1^m 0 r --> l 1^(k+2) <A 0 1^(m+1) 0 0 r *)
Lemma tR3 k m l r :
  l <* [0] <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+
  l <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r.
Proof. es. Qed.

(* R2: l 0 1^(k+1) 0 1 <A 0 r --> l <A 0 1^(k+2) 0 0 r *)
Lemma tR2 k l r :
  l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{A}} [0] *> r -->+
  l <{{A}} [0] *> [1]^^(S (S k)) *> [0;0] *> r.
Proof. es. Qed.

Lemma tR3c k m r :
  const 0 <{{A}} [0] *> [1]^^(S k) *> [0;0] *> [1]^^m *> [0] *> r -->+
  const 0 <* [1]^^(S (S k)) <{{A}} [0] *> [1]^^(S m) *> [0;0] *> r.
Proof. rewrite (const_unfold _ S0) at 1. es. Qed.

(* ---------- tape encoding of the run model ---------- *)
Fixpoint lsep (L : list nat) : side :=
  match L with
  | [] => const 0
  | y :: L' => lsep L' <* [1]^^y <* [0]
  end.

Definition lside (L : list nat) : side :=
  match L with
  | [] => const 0
  | x :: L' => lsep L' <* [1]^^x
  end.

Fixpoint rside (R : list nat) : side :=
  match R with
  | [] => const 0
  | [c] => [1]^^c *> const 0
  | c :: g :: R' => [1]^^c *> [0]^^g *> rside R'
  end.

Definition conf (L R : list nat) : Q * tape := lside L <{{A}} [0] *> rside R.

Lemma c0_1 : 0 >> const 0 = const 0.
Proof. symmetry. apply const_unfold. Qed.

Lemma lsep_eq L : lsep L = lside L <* [0].
Proof. destruct L; cbn; [apply const_unfold | reflexivity]. Qed.

Open Scope nat_scope.

(* ---------- the run model ---------- *)
(* A push reads the right word h :: R': it creates a child frame of value h and
   the word right of the head becomes [updt R'] (proof.md Lemma RM). *)
Definition updt (R' : list nat) : option (list nat) :=
  match R' with
  | [] => Some [1]
  | g :: R'' =>
    match g with
    | 0 | 1 => None
    | 2 => match R'' with
           | [] => None
           | c2 :: R3 => match R3 with
                         | [] => Some [S c2]
                         | 0 :: _ => None
                         | S g2 :: rest => Some (S c2 :: S (S g2) :: rest)
                         end
           end
    | S (S (S g')) => Some (1 :: S (S g') :: R'')
    end
  end.

Lemma updt_shape m R' R1 : updt R' = Some R1 ->
  exists x r, rside (S m :: R') = [S1]^^(S m) *> [S0;S0] *> [S1]^^x *> [S0] *> r /\
              rside R1 = [S1]^^(S x) *> [S0;S0] *> r.
Proof.
  intros H. destruct R' as [|g R'']; cbn in H.
  - inversion H; subst. exists 0, (const S0). cbn. rewrite !c0_1. split; reflexivity.
  - destruct g as [|[|[|g']]]; try discriminate.
    + destruct R'' as [|c2 R3]; try discriminate.
      destruct R3 as [|[|g2] rest]; try discriminate; inversion H; subst.
      * exists c2, (const S0). cbn. rewrite !c0_1. split; reflexivity.
      * exists c2, ([S0]^^g2 *> rside rest). cbn. split; reflexivity.
    + inversion H; subst. exists 0, ([S0]^^g' *> rside R''). cbn. split; reflexivity.
Qed.

Lemma push_ok y h R' R1 L : updt R' = Some R1 -> 1 <= y -> 1 <= h ->
  conf (S y :: L) (h :: R') -->+ conf (h :: y :: L) R1.
Proof.
  intros Hu Hy Hh. destruct y as [|n]; [lia|]. destruct h as [|m]; [lia|].
  destruct (updt_shape m R' R1 Hu) as (x & r & E1 & E2).
  unfold conf. change (lside (S (S n) :: L)) with (lsep L <* [S1]^^(S (S n))).
  change (lside (S m :: S n :: L)) with (lsep L <* [S1]^^(S n) <* [S0] <* [S1]^^(S m)).
  rewrite E1, E2. apply tR1.
Qed.

Lemma push0_ok h R' R1 : updt R' = Some R1 -> 1 <= h ->
  conf [] (h :: R') -->+ conf [S h] R1.
Proof.
  intros Hu Hh. destruct h as [|m]; [lia|].
  destruct (updt_shape m R' R1 Hu) as (x & r & E1 & E2).
  unfold conf. change (lside []) with (const S0).
  change (lside [S (S m)]) with (const S0 <* [S1]^^(S (S m))).
  rewrite E1, E2. apply tR3c.
Qed.

Lemma pop_ok y L R : 1 <= y -> conf (1 :: y :: L) R -->+ conf L (S y :: 2 :: R).
Proof.
  intros Hy. destruct y as [|k]; [lia|].
  unfold conf. change (lside (1 :: S k :: L)) with (lsep L <* [S1]^^(S k) <* [S0] <* [S1]^^1).
  rewrite lsep_eq.
  change (rside (S (S k) :: 2 :: R)) with ([S1]^^(S (S k)) *> [S0;S0] *> rside R).
  apply tR2.
Qed.

(* ---------- frame semantics ---------- *)
Inductive outcome := Fin (R : list nat) | Pop (c : nat) (R : list nat).

(* Life x R o: a frame of value x is on top with right word R.
   Fin R'  : it comes back on top with value 1 (it finishes; its parent is popped next);
   Pop c R': it created c children, and its last child finished, which popped it;
             R' is the right word after that pop (it starts with its value+1, then 2). *)
Inductive Life : nat -> list nat -> outcome -> Prop :=
| L_fin R : Life 1 R (Fin R)
| L_cf y h R' R1 Rc : 1 <= y -> updt R' = Some R1 -> Life h R1 (Fin Rc) ->
    Life (S y) (h :: R') (Pop 1 (S y :: 2 :: Rc))
| L_cpf y h R' R1 c' R2 Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
    Life y R2 (Fin Rf) -> Life (S y) (h :: R') (Fin Rf)
| L_cpp y h R' R1 c' R2 c Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
    Life y R2 (Pop c Rf) -> Life (S y) (h :: R') (Pop (S c) Rf).

Lemma Life_pos x R o : Life x R o -> 1 <= x.
Proof. destruct 1; lia. Qed.

Lemma Life_tm x R o : Life x R o -> forall L,
  match o with
  | Fin Rf => conf (x :: L) R -->* conf (1 :: L) Rf
  | Pop _ Rf => conf (x :: L) R -->+ conf L Rf
  end.
Proof.
  induction 1 as [R|y h R' R1 Rc Hy Hu H1 IH1|y h R' R1 c' R2 Rf Hy Hu H1 IH1 H2 IH2
                 |y h R' R1 c' R2 c Rf Hy Hu H1 IH1 H2 IH2]; intros L.
  - apply evstep_refl.
  - eapply progress_trans. { apply push_ok; eauto using Life_pos. }
    eapply evstep_progress_trans. { apply (IH1 (y :: L)). }
    apply pop_ok; lia.
  - apply progress_evstep. eapply progress_trans. { apply push_ok; eauto using Life_pos. }
    eapply progress_evstep_trans. { apply (IH1 (y :: L)). }
    apply IH2.
  - eapply progress_trans. { apply push_ok; eauto using Life_pos. }
    eapply progress_trans. { apply (IH1 (y :: L)). }
    apply IH2.
Qed.

(* ---------- epochs ---------- *)
(* Ep W c W': from Edge(W) = conf [] (3::2::W) the edge frame (value 4) creates c
   children and the epoch ends at conf [] ((5-c)::2::W'). *)
Definition Ep (W : list nat) (c : nat) (W' : list nat) : Prop :=
  exists R0, updt (2 :: W) = Some R0 /\ Life 4 R0 (Pop c ((5 - c) :: 2 :: W')).

Lemma Ep_tm W c W' : Ep W c W' -> conf [] (3 :: 2 :: W) -->+ conf [] ((5 - c) :: 2 :: W').
Proof.
  intros (R0 & Hu & HL).
  eapply progress_trans. { apply push0_ok; [exact Hu | lia]. }
  exact (Life_tm _ _ _ HL []).
Qed.

Lemma Life_shape x R o : Life x R o -> forall c Rf, o = Pop c Rf ->
  exists W', Rf = (x - c + 1) :: 2 :: W' /\ c + 1 <= x /\
    forall z, c + 1 <= z -> Life z R (Pop c ((z - c + 1) :: 2 :: W')).
Proof.
  induction 1 as [R|y h R' R1 Rc Hy Hu H1 IH1|y h R' R1 c' R2 Rf Hy Hu H1 IH1 H2 IH2
                 |y h R' R1 c' R2 c Rf Hy Hu H1 IH1 H2 IH2]; intros c0 Rf0 E; try discriminate.
  - inversion E; subst. exists Rc. split; [f_equal; lia|]. split; [lia|].
    intros z Hz. destruct z as [|z]; [lia|].
    replace (S z - 1 + 1) with (S z) by lia. eapply L_cf; eauto; lia.
  - inversion E; subst. destruct (IH2 c Rf0 eq_refl) as (W' & -> & Hc & Hm).
    exists W'. split; [f_equal; lia|]. split; [lia|].
    intros z Hz. destruct z as [|z]; [lia|].
    replace (S z - S c + 1) with (z - c + 1) by lia. eapply L_cpp; eauto; [lia | apply Hm; lia].
Qed.

Definition bump (o : outcome) : outcome :=
  match o with Fin W => Fin W | Pop c W => Pop (S c) W end.

Lemma L_cp y h R' R1 c' R2 o : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) ->
  Life y R2 o -> Life (S y) (h :: R') (bump o).
Proof. intros. destruct o; cbn; [eapply L_cpf | eapply L_cpp]; eauto. Qed.

Lemma updt_cons2 W R0 : updt (2 :: W) = Some R0 -> exists c2 W1, W = c2 :: W1.
Proof. destruct W; cbn; [discriminate | eauto]. Qed.

(* one child of a replay frame: the child runs a translated epoch (proof.md TL) *)
Lemma frame_step y z W c W' o y' z' : Ep W c W' -> 2 <= y -> c + 1 <= z ->
  y' = y - 1 -> z' = z - c + 1 ->
  Life y' (z' :: 2 :: W') o -> Life y (z :: 2 :: W) (bump o).
Proof.
  intros (R0 & Hu & HL) Hy Hz -> -> H.
  destruct (Life_shape _ _ _ HL c _ eq_refl) as (W'' & E & Hc & Hm).
  injection E as E. subst W''.
  destruct y as [|y]; [lia|].
  eapply L_cp; [lia | exact Hu | apply Hm; exact Hz | ].
  replace y with (S y - 1) by lia. exact H.
Qed.

(* ---------- concrete epoch rules (proof.md section 2) ---------- *)
Ltac lf :=
  first
  [ eassumption
  | apply L_fin
  | eapply L_cf; [lia | reflexivity | lf]
  | eapply L_cpf; [lia | reflexivity | lf | lf]
  | eapply L_cpp; [lia | reflexivity | lf | lf] ].

Ltac ep := eexists; split; [reflexivity | lf].

Definition tail_ok (N : list nat) : Prop := N = [] \/ exists g rest, N = S (S g) :: rest.

Lemma U0 : Ep [1] 2 [2;2;1].
Proof. ep. Qed.

Lemma U1 g rest : Ep (1 :: S (S (S (S g))) :: rest) 2 (2 :: 2 :: 1 :: S (S g) :: rest).
Proof. ep. Qed.

Lemma U2 b N : tail_ok N -> Ep (1 :: 2 :: S b :: N) 2 (S (S (S b)) :: 2 :: 1 :: N).
Proof. intros [-> | (g & rest & ->)]; ep. Qed.

Lemma ruleS a b N : tail_ok N ->
  Ep (2 :: 2 :: S a :: 2 :: S b :: N) 2 (S (S a) :: 2 :: S (S (S b)) :: 2 :: 1 :: N).
Proof. intros [-> | (g & rest & ->)]; ep. Qed.

Lemma TRF a b N Rc : tail_ok N -> 2 <= a ->
  Life a (S (S (S b)) :: 2 :: 1 :: N) (Fin Rc) -> Ep (a :: 2 :: S b :: N) 2 Rc.
Proof. intros [-> | (g & rest & ->)] Ha H; ep. Qed.

Lemma Xin0 a'' b'' : 1 <= a'' ->
  Life 2 [2; 2; a''; 2; b''] (Pop 1 [2; 2; S a''; 2; S b'']).
Proof. intros. lf. Qed.

Lemma Xin1 a'' b'' g rest : 1 <= a'' ->
  Life 2 (2 :: 2 :: a'' :: 2 :: b'' :: S g :: rest) (Pop 1 (2 :: 2 :: S a'' :: 2 :: S b'' :: S (S g) :: rest)).
Proof. intros. lf. Qed.

Lemma TRX0 a b N c a'' b'' : tail_ok N -> 2 <= a ->
  Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c [2; 2; S a''; 2; S b'']) ->
  Ep (a :: 2 :: S b :: N) 3 [S (S a''); 2; S (S b'')].
Proof. intros [-> | (g & rest & ->)] Ha H; ep. Qed.

Lemma TRX1 a b N c a'' b'' g rest : tail_ok N -> 2 <= a ->
  Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c (2 :: 2 :: S a'' :: 2 :: S b'' :: S g :: rest)) ->
  Ep (a :: 2 :: S b :: N) 3 (S (S a'') :: 2 :: S (S b'') :: S (S g) :: rest).
Proof. intros [-> | (g' & rest' & ->)] Ha H; ep. Qed.

(* ---------- marker words, orbits, replay ---------- *)
(* A marker word is given by its absorption indices P = [I_1; ...; I_m] (proof.md section 0):
   gaps g_j = I_j - I_(j-1) + 1, each followed by a lone 1. *)
Fixpoint mwf (s : nat) (P : list nat) : list nat :=
  match P with
  | [] => []
  | p :: P' => (p - s + 1) :: 1 :: mwf p P'
  end.
Definition mw (P : list nat) : list nat := mwf 0 P.

(* even gaps: each index is odd above the previous one *)
Fixpoint valid_from (s : nat) (P : list nat) : Prop :=
  match P with
  | [] => True
  | p :: P' => (exists t, p = s + 2 * t + 1) /\ valid_from p P'
  end.
Definition valid (P : list nat) : Prop := valid_from 0 P.

Definition cnt (Q : list nat) (n : nat) : nat := length (filter (fun q => q <? n) Q).
Definition ind (Q : list nat) (n : nat) : nat := cnt Q (S n) - cnt Q n.
Definition cost (Q : list nat) (n : nat) : nat := 2 + ind Q n.

Inductive Orb (Q : list nat) : nat -> list nat -> Prop :=
| O0 : Orb Q 0 (1 :: mw Q)
| OS n W W' : Orb Q n W -> Ep W (cost Q n) W' -> Orb Q (S n) W'.

Fixpoint bumpn (k : nat) (o : outcome) : outcome :=
  match k with 0 => o | S k => bumpn k (bump o) end.

Lemma bumpn_fin k W : bumpn k (Fin W) = Fin W.
Proof. induction k; cbn; auto. Qed.

Lemma bumpn_pop k c W : bumpn k (Pop c W) = Pop (k + c) W.
Proof. revert c. induction k; intros c; cbn; [reflexivity|]. rewrite IHk. f_equal. lia. Qed.

Lemma cnt_0 Q : cnt Q 0 = 0.
Proof. unfold cnt. induction Q; cbn [filter length]; auto. Qed.

Lemma cnt_mono Q n : cnt Q n <= cnt Q (S n).
Proof.
  unfold cnt. induction Q as [|q Q IH]; cbn [filter length]; [lia|].
  destruct (Nat.ltb_spec q n), (Nat.ltb_spec q (S n)); cbn [length]; lia.
Qed.

Lemma cnt_mono' Q n m : n <= m -> cnt Q n <= cnt Q m.
Proof. induction 1; [lia|]. pose proof (cnt_mono Q m). lia. Qed.

Lemma replay Q k Wk : Orb Q k Wk -> forall y z o, k + 1 <= y -> (k = 0 \/ k + 2 + cnt Q k <= z) ->
  Life (y - k) ((z - k - cnt Q k) :: 2 :: Wk) o -> Life y (z :: 2 :: 1 :: mw Q) (bumpn k o).
Proof.
  induction 1 as [|n W W' HO IH HE]; intros y z o Hy Hz H.
  - cbn in *. rewrite cnt_0, !Nat.sub_0_r in H. exact H.
  - cbn [bumpn]. pose proof (cnt_mono Q n) as Hm. unfold cost, ind in HE.
    apply IH; [lia | right; lia | ].
    eapply frame_step; [exact HE | lia | lia | | | exact H]; lia.
Qed.

Lemma mw_tail_ok Q : valid Q -> tail_ok (mw Q).
Proof.
  destruct Q as [|q Q]; [left; reflexivity|].
  intros [[t Ht] _]. right. exists (q - 1), (1 :: mwf q Q). cbn. f_equal. lia.
Qed.

Lemma ruleT a b Q W' : Orb Q (a - 1) W' -> 2 <= a -> 1 <= b -> valid Q ->
  a - 1 + cnt Q (a - 1) <= b ->
  Ep (a :: 2 :: b :: mw Q) 2 ((b + 3 - a - cnt Q (a - 1)) :: 2 :: W').
Proof.
  intros HO Ha Hb HV Hc. destruct b as [|b]; [lia|].
  apply TRF; [apply mw_tail_ok; exact HV | exact Ha | ].
  rewrite <- (bumpn_fin (a - 1)).
  apply (replay Q (a - 1) W' HO); [lia | lia | ].
  replace (a - (a - 1)) with 1 by lia.
  replace (S (S (S b)) - (a - 1) - cnt Q (a - 1)) with (S b + 3 - a - cnt Q (a - 1)) by lia.
  apply L_fin.
Qed.

Lemma mwf_shift s k P : mwf (s + k) (map (fun p => p + k) P) = mwf s P.
Proof.
  revert s. induction P as [|p P IH]; intros s; cbn; [reflexivity|].
  rewrite IH. f_equal. lia.
Qed.

Lemma ruleX a b Q a'' Q'' : Orb Q (a - 2) (a'' :: 2 :: b :: mw Q'') -> 3 <= a -> 1 <= b ->
  1 <= a'' -> valid Q -> valid Q'' -> b = a - 2 + cnt Q (a - 2) ->
  Ep (a :: 2 :: b :: mw Q) 3 (S (S a'') :: 2 :: S (S b) :: mw (map (fun q => q + 2) Q'')).
Proof.
  intros HO Ha Hb Ha'' HV HV'' Hbe. destruct b as [|b0]; [lia|].
  assert (Hz : S (S (S b0)) - (a - 2) - cnt Q (a - 2) = 2) by lia.
  assert (Hy : a - (a - 2) = 2) by lia.
  destruct Q'' as [|q Q2].
  - cbn. eapply TRX0 with (c := a - 2 + 1); [apply mw_tail_ok; exact HV | lia | ].
    rewrite <- bumpn_pop.
    apply (replay Q (a - 2) _ HO); [lia | lia | ].
    rewrite Hz, Hy. apply Xin0. exact Ha''.
  - change (mw (q :: Q2)) with ((q - 0 + 1) :: 1 :: mwf q Q2) in HO.
    replace (q - 0 + 1) with (S q) in HO by lia.
    cbn [mw mwf map]. replace (q + 2 - 0 + 1) with (S (S (S q))) by lia.
    replace (q + 2) with (q + 2) by reflexivity. rewrite mwf_shift.
    eapply TRX1 with (c := a - 2 + 1); [apply mw_tail_ok; exact HV | lia | ].
    rewrite <- bumpn_pop.
    apply (replay Q (a - 2) _ HO); [lia | lia | ].
    rewrite Hz, Hy. apply Xin1. exact Ha''.
Qed.