From BusyCoq Require Import Individual62.
From Dev Require Import Low.
Require Import Lia.
Require Import List.
Require Import Arith.
Import ListNotations.
Open Scope list.

Inductive dg := d0 | d1 | d2 | d3.
Inductive tok := Dg (d : dg) | Sw.
Inductive tt := tX | tS.

Definition rdw (d : dg) : list Sym :=
  match d with
  | d0 => [0;0;1;1;0;0;1;1]
  | d1 => [0;0;0;0;1;1]
  | d2 => [0;0;1;1;0;0;1]
  | d3 => [0;0;0;0;1]
  end.

Definition rtw (t : tok) : list Sym := match t with Dg d => rdw d | Sw => [0;0;1] end.

Definition lsd (l : side) (ts : list tok) : side := fold_left (fun l t => l <* rtw t) ts l.

Definition base (w : bool) : side := if w then const 0 <* [0;0;1;1] else const 0.

Definition K (w : bool) (ts : list tok) : Q * tape := lsd (base w) ts {{D}}> const 0.

Definition xw : list Sym := [1;0;1;0;1;0;1;0].

Fixpoint renc (T : list tt) (r : side) : side :=
  match T with
  | [] => r
  | tX :: T' => xw *> renc T' r
  | tS :: T' => [1;0;0] *> renc T' r
  end.

Definition tend : side := [1;0;1;0] *> const 0.

Definition tok_of (x : tt) : tok := match x with tX => Dg d0 | tS => Sw end.

Fixpoint rmS (T : list tt) : option (list tt) :=
  match T with
  | [] => None
  | tS :: T' => Some T'
  | tX :: T' => match rmS T' with Some T1 => Some (tX :: T1) | None => None end
  end.

Fixpoint lpass (w : bool) (Lr : list tok) (T : list tt) : option (bool * list tok) :=
  match Lr with
  | [] =>
      if w then Some (false, map tok_of T ++ [Sw; Sw])
      else match rmS T with
           | Some T1 =>
               match rev T1 with
               | tS :: Rv => Some (true, map tok_of (rev Rv) ++ [Dg d3; Sw; Sw; Sw])
               | _ => None
               end
           | None => None
           end
  | Sw :: Lr' => lpass w Lr' (tS :: T)
  | Dg d3 :: Lr' => match rmS T with Some T1 => lpass w Lr' (tX :: T1) | None => None end
  | Dg d0 :: Lr' => Some (w, rev Lr' ++ Dg d1 :: map tok_of T ++ [Sw; Sw])
  | Dg d1 :: Lr' =>
      match rmS T with
      | Some T1 => Some (w, rev Lr' ++ Dg d2 :: map tok_of T1 ++ [Sw; Sw])
      | None => None
      end
  | Dg d2 :: Lr' => Some (w, rev Lr' ++ Dg d3 :: map tok_of T ++ [Sw; Sw])
  end.

Definition sweep (w : bool) (ts : list tok) := lpass w (rev ts) [].

(* ---------- tape algebra ---------- *)

Lemma lsd_app l a b : lsd l (a ++ b) = lsd (lsd l a) b.
Proof. unfold lsd. apply fold_left_app. Qed.

Lemma lsd_cons l t ts : lsd l (t :: ts) = lsd (l <* rtw t) ts.
Proof. reflexivity. Qed.

Lemma lsd_nil l : lsd l [] = l.
Proof. reflexivity. Qed.

Lemma lsd_rep0 j : forall l, lsd l (repeat (Dg d0) j) = l <* [0;0;1;1;0;0;1;1]^^j.
Proof.
  induction j as [|j IH]; intros l; [reflexivity|].
  cbn [repeat]. rewrite lsd_cons, IH. cbn [rtw rdw lpow].
  rewrite Str_app_assoc. apply lpow_shift'.
Qed.

Lemma lsd_map_rep j l : lsd l (map tok_of (repeat tX j)) = l <* [0;0;1;1;0;0;1;1]^^j.
Proof. rewrite map_repeat. apply lsd_rep0. Qed.

Lemma renc_app a b r : renc (a ++ b) r = renc a (renc b r).
Proof. induction a as [|[] a IH]; cbn; [reflexivity | rewrite IH; reflexivity | rewrite IH; reflexivity]. Qed.

Lemma renc_rep j r : renc (repeat tX j) r = xw^^j *> r.
Proof. induction j as [|j IH]; cbn [repeat renc lpow]; [reflexivity|]. rewrite IH, Str_app_assoc. reflexivity. Qed.

Lemma decomp T : exists j rest, T = repeat tX j ++ rest /\ (rest = [] \/ exists T', rest = tS :: T').
Proof.
  induction T as [|[] T IH].
  - exists O, (@nil tt). auto.
  - destruct IH as (j & rest & -> & H). exists (S j), rest. auto.
  - exists O, (tS :: T). eauto.
Qed.

Lemma rmS_spec T T1 : rmS T = Some T1 ->
  exists j T', T = repeat tX j ++ tS :: T' /\ T1 = repeat tX j ++ T'.
Proof.
  revert T1; induction T as [|[] T IH]; intros T1 H; cbn in H; try discriminate.
  - destruct (rmS T) as [T2|] eqn:E; [|discriminate]. injection H as <-.
    destruct (IH T2 eq_refl) as (j & T' & -> & ->). exists (S j), T'. auto.
  - injection H as <-. exists O, T. auto.
Qed.

Lemma notin_rep j U : ~ (repeat tX j = U ++ [tS]).
Proof.
  intros H. assert (Hin : In tS (repeat tX j)) by (rewrite H; apply in_or_app; right; left; reflexivity).
  apply repeat_spec in Hin. discriminate.
Qed.

Lemma split_end j : forall T' V, repeat tX j ++ T' = V ++ [tS] ->
  exists U, T' = U ++ [tS] /\ V = repeat tX j ++ U.
Proof.
  intros T' V H.
  destruct (rev T') as [|x Rv] eqn:ER;
    apply (f_equal (@rev tt)) in ER; rewrite rev_involutive in ER; cbn in ER; subst T'.
  - rewrite app_nil_r in H. exfalso. exact (notin_rep j V H).
  - rewrite app_assoc in H. apply app_inj_tail in H. destruct H as [HV Hx]. subst x.
    exists (rev Rv). split; [reflexivity | symmetry; exact HV].
Qed.

(* ---------- soundness: right passes ---------- *)

Lemma Apass n : forall T l, length T <= n ->
  l <* [0;1] {{A}}> renc T tend -->+ lsd l (map tok_of T ++ [Sw; Sw]) {{D}}> const 0.
Proof.
  induction n as [|n IH]; intros T l Hn;
    destruct (decomp T) as (j & rest & -> & [-> | (T' & ->)]).
  1,3: rewrite !app_nil_r, renc_rep, lsd_app, lsd_map_rep;
       exact (RA3 l j).
  - rewrite length_app in Hn. cbn in Hn. lia.
  - rewrite renc_app, renc_rep. cbn [renc].
    rewrite map_app, <- app_assoc, lsd_app, lsd_map_rep. cbn [map app].
    rewrite lsd_cons.
    eapply progress_trans; [exact (RA1 l j (renc T' tend)) |].
    apply IH. rewrite length_app in Hn. cbn in Hn. lia.
Qed.

Lemma Epass n : forall T l U, length T <= n -> T = U ++ [tS] ->
  l <* [0;0;1] <* [1] {{E}}> renc T tend -->+
  lsd l (map tok_of U ++ [Dg d3; Sw; Sw; Sw]) {{D}}> const 0.
Proof.
  induction n as [|n IH]; intros T l U Hn HT;
    destruct (decomp T) as (j & rest & -> & [-> | (T' & ->)]).
  1,3: rewrite app_nil_r in HT; exfalso; exact (notin_rep j U HT).
  - rewrite length_app in Hn. cbn in Hn. lia.
  - rewrite renc_app, renc_rep. cbn [renc].
    eapply progress_trans; [exact (RE1 l j (renc T' tend)) |].
    assert (HT2 : (repeat tX j ++ [tS]) ++ T' = U ++ [tS]) by (rewrite <- app_assoc; exact HT).
    destruct (rev T') as [|x Rv] eqn:ER;
      apply (f_equal (@rev tt)) in ER; rewrite rev_involutive in ER; cbn in ER; subst T'.
    + rewrite app_nil_r in HT2. apply app_inj_tail in HT2. destruct HT2 as [HU _]. subst U.
      cbn [renc]. rewrite lsd_app, lsd_map_rep. exact (RE2 (l <* [0;0;1;1;0;0;1;1]^^j)).
    + rewrite app_assoc in HT2. apply app_inj_tail in HT2. destruct HT2 as [HU Hx]. subst x U.
      rewrite !map_app, <- !app_assoc, lsd_app, lsd_map_rep. cbn [map app]. rewrite lsd_cons.
      apply IH; [| reflexivity].
      clear - Hn. rewrite !length_app in Hn. cbn [length] in Hn. rewrite length_app in Hn.
      rewrite length_app. cbn [length] in Hn |- *. lia.
Qed.

(* ---------- soundness: the left pass and the whole sweep ---------- *)

Lemma lsd_snoc l a t : lsd l (a ++ [t]) = lsd l a <* rtw t.
Proof. rewrite lsd_app. reflexivity. Qed.

Lemma lpass_sound : forall Lr T w w' ts', lpass w Lr T = Some (w', ts') ->
  lsd (base w) (rev Lr) <{{B}} renc T tend -->+ K w' ts'.
Proof.
  induction Lr as [|[[] | ] Lr IH]; intros T w w' ts' H; cbn [lpass] in H.
  - destruct w.
    + (* O1: the wall is erased *)
      injection H as <- <-.
      eapply progress_trans; [exact (L6 (renc T tend)) |].
      exact (Apass (length T) T (const 0) (le_n _)).
    + (* O2: a wall and a new digit 3 *)
      destruct (rmS T) as [T1|] eqn:E; [|discriminate].
      destruct (rev T1) as [|[] Rv] eqn:ER; try discriminate. injection H as <- <-.
      destruct (rmS_spec _ _ E) as (j & T' & -> & ->).
      apply (f_equal (@rev tt)) in ER. rewrite rev_involutive in ER. cbn in ER.
      destruct (split_end j T' (rev Rv) ER) as (U & -> & HU).
      rewrite renc_app, renc_rep. cbn [renc].
      eapply progress_trans; [exact (L7 j (renc (U ++ [tS]) tend)) |].
      rewrite HU. unfold K. cbn [base]. rewrite map_app, <- app_assoc, lsd_app, lsd_map_rep.
      apply (Epass (length (U ++ [tS]))); [lia | reflexivity].
  - (* stop at phase 0 *)
    injection H as <- <-. cbn [rev]. rewrite lsd_snoc.
    eapply progress_trans; [exact (L3 (lsd (base w) (rev Lr)) (renc T tend)) |].
    unfold K. rewrite lsd_app, lsd_cons.
    exact (Apass (length T) T _ (le_n _)).
  - (* stop at phase 1 *)
    destruct (rmS T) as [T1|] eqn:E; [|discriminate]. injection H as <- <-.
    destruct (rmS_spec _ _ E) as (j & T' & -> & ->).
    cbn [rev]. rewrite lsd_snoc. unfold K. rewrite lsd_app, lsd_cons.
    destruct (decomp T') as (i & rest & -> & [-> | (T'' & ->)]).
    + rewrite !app_nil_r, renc_app, renc_rep. cbn [renc]. rewrite renc_rep.
      rewrite <- repeat_app, lsd_app, lsd_map_rep, Nat.add_comm.
      exact (L5e (lsd (base w) (rev Lr)) j i).
    + rewrite renc_app, renc_rep. cbn [renc]. rewrite renc_app, renc_rep. cbn [renc].
      rewrite app_assoc, <- repeat_app, map_app, <- app_assoc, lsd_app, lsd_map_rep.
      cbn [map app]. rewrite lsd_cons, (Nat.add_comm j i).
      eapply progress_trans; [exact (L5 (lsd (base w) (rev Lr)) j i (renc T'' tend)) |].
      exact (Apass (length T'') T'' _ (le_n _)).
  - (* stop at phase 2 *)
    injection H as <- <-. cbn [rev]. rewrite lsd_snoc.
    eapply progress_trans; [exact (L4 (lsd (base w) (rev Lr)) (renc T tend)) |].
    unfold K. rewrite lsd_app, lsd_cons.
    exact (Apass (length T) T _ (le_n _)).
  - (* a digit 3 wraps *)
    destruct (rmS T) as [T1|] eqn:E; [|discriminate].
    destruct (rmS_spec _ _ E) as (j & T' & -> & ->).
    cbn [rev]. rewrite lsd_snoc, renc_app, renc_rep. cbn [renc].
    eapply progress_trans; [exact (L2 (lsd (base w) (rev Lr)) j (renc T' tend)) |].
    specialize (IH _ _ _ _ H). cbn [renc] in IH. rewrite renc_app, renc_rep in IH. exact IH.
  - (* a sea word *)
    cbn [rev]. rewrite lsd_snoc.
    eapply progress_trans; [exact (L1 (lsd (base w) (rev Lr)) (renc T tend)) |].
    exact (IH _ _ _ _ H).
Qed.

Lemma sweep_sound w ts w' ts' : (exists u, ts = u ++ [Sw]) -> sweep w ts = Some (w', ts') ->
  K w ts -->+ K w' ts'.
Proof.
  intros [u ->] H. unfold sweep in H. apply lpass_sound in H. rewrite rev_involutive, lsd_snoc in H.
  unfold K at 1. rewrite lsd_snoc.
  eapply progress_trans; [exact (S0 (lsd (base w) u)) | exact H].
Qed.

(* ---------- the invariant ---------- *)

Open Scope nat_scope.

Definition odd (d : dg) : nat := match d with d1 | d3 => 1 | _ => 0 end.

Fixpoint JL (Lr : list tok) (n : nat) : Prop :=
  match Lr with
  | [] => 2 <= n
  | Sw :: Lr' => JL Lr' (S n)
  | Dg d :: Lr' => odd d + 2 <= n /\ JL Lr' (n - odd d)
  end.

Fixpoint cS (T : list tt) : nat :=
  match T with [] => 0 | tS :: T' => S (cS T') | tX :: T' => cS T' end.

Lemma JL_mono Lr : forall n m, n <= m -> JL Lr n -> JL Lr m.
Proof.
  induction Lr as [|[d|] Lr IH]; cbn [JL]; intros n m Hnm H.
  - lia.
  - destruct H as [H1 H2]. split; [lia|]. apply (IH (n - odd d)); [lia | exact H2].
  - apply (IH (S n)); [lia | exact H].
Qed.

Lemma cS_app a b : cS (a ++ b) = cS a + cS b.
Proof. induction a as [|[] a IH]; cbn [app cS]; lia. Qed.

Lemma cS_rev T : cS (rev T) = cS T.
Proof. induction T as [|[] T IH]; cbn [rev]; rewrite ?cS_app; cbn [cS]; lia. Qed.

Lemma JL_map V : forall n Lr, 2 <= n -> JL Lr (n + cS V) -> JL (map tok_of V ++ Lr) n.
Proof.
  induction V as [|[] V IH]; cbn [map app cS JL tok_of odd]; intros n Lr Hn H.
  - rewrite Nat.add_0_r in H. exact H.
  - split; [lia|]. rewrite Nat.sub_0_r. apply IH; assumption.
  - apply IH; [lia|]. rewrite Nat.add_succ_r in H. exact H.
Qed.

Lemma JL_out Lr d T : odd d + 2 <= 2 + cS T -> JL Lr (2 + cS T - odd d) ->
  JL (rev (rev Lr ++ Dg d :: map tok_of T ++ [Sw; Sw])) 0.
Proof.
  intros H1 H2.
  rewrite rev_app_distr, rev_involutive. cbn [rev]. rewrite rev_app_distr. cbn [rev app].
  rewrite <- map_rev, <- !app_assoc. cbn [app JL].
  apply JL_map; [lia|]. rewrite cS_rev. cbn [JL]. split; [lia | exact H2].
Qed.

Lemma rmS_cS T T1 : rmS T = Some T1 -> cS T = S (cS T1).
Proof.
  intros H. destruct (rmS_spec _ _ H) as (j & T' & -> & ->). rewrite !cS_app. cbn [cS]. lia.
Qed.

Lemma rmS_some T : 1 <= cS T -> exists T1, rmS T = Some T1.
Proof.
  induction T as [|[] T IH]; cbn [cS rmS]; intros H; [lia | | eauto].
  destruct (IH H) as (T1 & ->). eauto.
Qed.

Lemma rmS_snoc U : 1 <= cS U -> exists U1, rmS U = Some U1 /\ rmS (U ++ [tS]) = Some (U1 ++ [tS]).
Proof.
  induction U as [|[] U IH]; cbn [cS rmS app]; intros H; [lia | | eauto].
  destruct (IH H) as (U1 & -> & ->). eauto.
Qed.

Definition Eend (T : list tt) := T = [] \/ exists U, T = U ++ [tS].

Lemma lpass_inv : forall Lr T w, JL Lr (cS T) -> Eend T ->
  exists w' ts', lpass w Lr T = Some (w', ts') /\ JL (rev ts') 0.
Proof.
  induction Lr as [|[[] | ] Lr IH]; intros T w HJ HE; cbn [JL odd] in HJ; cbn [lpass].
  - destruct w.
    + eexists _, _. split; [reflexivity|].
      rewrite rev_app_distr. cbn [rev app]. rewrite <- map_rev, <- (app_nil_r (map tok_of (rev T))).
      cbn [JL]. apply JL_map; [lia|]. cbn [JL]. rewrite cS_rev. lia.
    + destruct HE as [-> | (U & ->)]; [cbn [cS] in HJ; lia|].
      rewrite cS_app in HJ. cbn [cS] in HJ.
      destruct (rmS_snoc U) as (U1 & _ & ->); [lia|].
      rewrite rev_app_distr. cbn [rev app].
      eexists _, _. split; [reflexivity|].
      rewrite rev_involutive, rev_app_distr. cbn [rev app].
      rewrite <- map_rev, <- (app_nil_r (map tok_of (rev U1))).
      cbn [JL odd]. split; [lia|]. apply JL_map; [lia|]. cbn [JL]. lia.
  - eexists _, _. split; [reflexivity|].
    apply JL_out; cbn [odd]; [lia|]. apply (JL_mono _ (cS T - 0)); [lia | tauto].
  - destruct (rmS_some T) as (T1 & E); [lia|]. rewrite E. pose proof (rmS_cS _ _ E) as HC.
    eexists _, _. split; [reflexivity|].
    apply JL_out; cbn [odd]; [lia|]. apply (JL_mono _ (cS T - 1)); [lia | tauto].
  - eexists _, _. split; [reflexivity|].
    apply JL_out; cbn [odd]; [lia|]. apply (JL_mono _ (cS T - 0)); [lia | tauto].
  - destruct HE as [-> | (U & ->)]; [cbn [cS] in HJ; lia|].
    rewrite cS_app in HJ. cbn [cS] in HJ.
    destruct (rmS_snoc U) as (U1 & HU & ->); [lia|]. pose proof (rmS_cS _ _ HU) as HC.
    apply IH.
    + cbn [cS]. rewrite cS_app. cbn [cS]. apply (JL_mono _ (cS U + 1 - 1)); [lia | tauto].
    + right. exists (tX :: U1). reflexivity.
  - apply IH; [exact HJ|].
    destruct HE as [-> | (U & ->)]; right; [exists (@nil tt); reflexivity | exists (tS :: U); reflexivity].
Qed.

Lemma JL_ends ts : JL (rev ts) 0 -> exists u, ts = u ++ [Sw].
Proof.
  intros H. destruct (rev ts) as [|[d|] Lr] eqn:E; cbn [JL] in H; [lia | destruct H; lia |].
  exists (rev Lr). apply (f_equal (@rev tok)) in E. rewrite rev_involutive in E. exact E.
Qed.

Lemma step_ok w ts : JL (rev ts) 0 -> exists w' ts', K w ts -->+ K w' ts' /\ JL (rev ts') 0.
Proof.
  intros HJ.
  destruct (lpass_inv (rev ts) [] w HJ (or_introl eq_refl)) as (w' & ts' & H & HI).
  exists w', ts'. split; [| exact HI].
  apply sweep_sound; [apply JL_ends; exact HJ | exact H].
Qed.

Lemma init : c0 -->* K false [Dg d1; Sw; Sw; Sw].
Proof. unfold K, lsd, base. cbn. solve_init. Qed.

Lemma nonhalt : ~ halts tm c0.
Proof.
  eapply multistep_nonhalt; [exact init|].
  apply (progress_nonhalt_cond tm (bool * list tok) (false, [Dg d1; Sw; Sw; Sw])
           (fun i => K (fst i) (snd i)) (fun i => JL (rev (snd i)) 0)).
  - intros [w ts] HI. destruct (step_ok w ts HI) as (w' & ts' & H1 & H2).
    exists (w', ts'). split; [exact H1 | exact H2].
  - cbn. lia.
Qed.

Print Assumptions nonhalt.