Require Import List Relation_Operators Operators_Properties Lia.
Import ListNotations.

Require Import Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.SR2ab.
Require Import Undecidability.CounterMachines.CM2.

Require Import Undecidability.StringRewriting.Util.List_facts.
Require Import Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.SR2ab_facts.
Require Import Undecidability.CounterMachines.Util.CM2_facts.

Require Import ssreflect ssrbool ssrfun.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

Local Arguments rt_trans {A R x y z}.
Local Arguments in_combine_l {A B l l' x y}.

Module Facts.
(* duplicates argument *)
Lemma copy {A : Prop} : A -> A * A.
Proof. done. Qed.

Lemma iter_plus {X: Type} {f: X -> X} {x: X} {n m: nat} :
  Nat.iter (n + m) f x = Nat.iter n f (Nat.iter m f x).
Proof. by rewrite /Nat.iter nat_rect_plus. Qed.

Lemma nth_error_Some_in_combine {X: Type} {l: list X} {i x}:
  nth_error l i = Some x ->
  In (i, x) (combine (seq 0 (length l)) l).
Proof.
  move Hk: (0) => k Hi. have ->: (i = i + k) by lia.
  elim: l i k {Hk} Hi; first by case.
  move=> y l IH [|i] k.
  - move=> /= [<-]. by left.
  - move=> /IH {}IH /=. right. by have ->: (S (i + k) = i + S k) by lia.
Qed.

Lemma inv_nth_error_Some_in_combine {X: Type} {l: list X} {i x}:
  In (i, x) (combine (seq 0 (length l)) l) -> nth_error l i = Some x.
Proof.
  move Hk: (0) => k. rewrite [in (_, _)](ltac:(lia) : (i = i + k)).
  elim: l i k {Hk}; first by case.
  move=> y l IH i k /= [].
  - move=> [? ->]. by have ->: i = 0 by lia.
  - move: i => [|i].
    + move=> /in_combine_l /in_seq. by lia.
    + have ->: S i + k = i + S k by lia.
      by move=> /IH.
Qed.
End Facts.

Module Argument.
Import Facts.
Local Arguments List.app : simpl never.
Local Arguments Nat.sub : simpl never.
Local Arguments repeat : simpl never.
Local Arguments app_inj_tail {A x y a b}.

Section Reduction.
(* given two-counter machine *)
Context (cm : Cm2).

Local Notation sb := ((0, @None nat)). (* blank *)
Local Notation sl := ((1, @None nat)). (* left marker *)
Local Notation sr := ((2, @None nat)). (* right marker *)
Local Notation sm := ((3, @None nat)). (* middle marker *)

Local Notation sz := ((4, @None nat)). (* 0 *)
Local Notation so := ((5, @Some nat 0)). (* 1 *)
Local Notation st := ((6, @None nat)). (* temporary marker *)

Local Notation sb' p := ((0, @Some nat p)). (* blank *)
Local Notation sl' p := ((1, @Some nat p)). (* left marker *)
Local Notation sr' p := ((2, @Some nat p)). (* right marker *)
Local Notation sm' p := ((3, @Some nat p)). (* middle marker *)

Definition states := map (fun i => if i is dec _ q then q else 0) cm.
Definition sum : list nat -> nat := fold_right Nat.add 0.

Definition state_bound := 1 + length cm + sum states.

Lemma state_boundP {p i} : nth_error cm p = Some i ->
  (if i is dec _ q then q else 0) + 1 + p < state_bound.
Proof.
  rewrite /state_bound /states.
  elim: (cm) p; first by case.
  move=> ? l IH [|p] /= => [[->] | /IH]; last by lia.
  by case: (i); lia.
Qed.

(* encode instruction i at position n *)
Definition enc_Instruction (ni: (nat * Instruction)) : Srs :=
  match ni with
  | (p, inc b) => if b then [((sr' p, sz), (sb, sr' (S p)))] else [((sz, sl' p), (sl' (S p), sb))]
  | (p, dec b q) =>
      if b then [((sm, sr' p), (sm, sr' (S p))); ((sb, sr' p), (sr' q, sz))]
      else [((sl' p, sm), (sl' (S p), sm)); ((sl' p, sb), (sz, sl' q))]
  end.

(* constructed string rewriting system *)
Definition srs : Srs :=
  (* initialization *)
  [((sz, sz), (st, sr)); (* 00 -> tr *)
   ((sz, st), (sl' 0, sm)) (* 0t -> l_0 m *)] ++
  (* simulation *)
  flat_map enc_Instruction (combine (seq 0 (length cm)) cm) ++
  (* state movement to the right *)
  flat_map (fun p => [
    ((sl' p, sb), (sl, sb' p)); ((sl' p, sm), (sl, sm' p));
    ((sb' p, sb), (sb, sb' p)); ((sb' p, sm), (sb, sm' p)); ((sb' p, sr), (sb, sr' p));
    ((sm' p, sb), (sm, sb' p)); ((sm' p, sr), (sm, sr' p))]) (seq 0 state_bound) ++
  (* state movement to the left *)
  flat_map (fun p => [
    ((sb, sr' p), (sb' p, sr)); ((sm, sr' p), (sm' p, sr));
    ((sb, sb' p), (sb' p, sb)); ((sm, sb' p), (sm' p, sb)); ((sl, sb' p), (sl' p, sb));
    ((sb, sm' p), (sb' p, sm)); ((sl, sm' p), (sl' p, sm))]) (seq 0 state_bound) ++
  (* finalization *)
  map (fun p => ((sz, sl' p), (so, so))) (seq (length cm) (state_bound - length cm)) ++
  [((sz, so), (so, so)); ((so, sb), (so, so)); ((so, sm), (so, so));
   ((so, sr), (so, so)); ((so, sz), (so, so))].

(* initialization, simulation, finalization *)
Inductive srs_spec (a b c d: Symbol) : Prop :=
  | srs_i0 : ((sz, sz), (st, sr)) = ((a, b), (c, d)) -> srs_spec a b c d
  | srs_i1 : ((sz, st), (sl' 0, sm)) = ((a, b), (c, d)) -> srs_spec a b c d
  | srs_sim0 {p} : ((sr' p, sz), (sb, sr' (S p))) = ((a, b), (c, d)) -> nth_error cm p = Some (inc true) -> srs_spec a b c d
  | srs_sim1 {p} : ((sz, sl' p), (sl' (S p), sb)) = ((a, b), (c, d)) -> nth_error cm p = Some (inc false) -> srs_spec a b c d
  | srs_sim2 {p q} : ((sm, sr' p), (sm, sr' (S p))) = ((a, b), (c, d)) -> nth_error cm p = Some (dec true q) -> srs_spec a b c d
  | srs_sim3 {p q} : ((sb, sr' p), (sr' q, sz))= ((a, b), (c, d)) -> nth_error cm p = Some (dec true q) -> srs_spec a b c d
  | srs_sim4 {p q} : ((sl' p, sm), (sl' (S p), sm)) = ((a, b), (c, d)) -> nth_error cm p = Some (dec false q) -> srs_spec a b c d
  | srs_sim5 {p q} : ((sl' p, sb), (sz, sl' q)) = ((a, b), (c, d)) -> nth_error cm p = Some (dec false q) -> srs_spec a b c d
  | srs_fin0 {p} : ((sz, sl' p), (so, so)) = ((a, b), (c, d)) -> length cm <= p < state_bound -> srs_spec a b c d
  | srs_fin1 : ((sz, so), (so, so)) = ((a, b), (c, d)) -> srs_spec a b c d
  | srs_fin2 : ((so, sb), (so, so)) = ((a, b), (c, d)) -> srs_spec a b c d
  | srs_fin3 : ((so, sm), (so, so)) = ((a, b), (c, d)) -> srs_spec a b c d
  | srs_fin4 : ((so, sr), (so, so)) = ((a, b), (c, d)) -> srs_spec a b c d
  | srs_fin5 : ((so, sz), (so, so)) = ((a, b), (c, d)) -> srs_spec a b c d.

(* opaque state movement *)
Inductive srs_mlr_spec (a b c d: Symbol) : Prop :=
  | srs_mr0 {p} : ((sl' p, sb), (sl, sb' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_mr1 {p} : ((sl' p, sm), (sl, sm' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_mr2 {p} : ((sb' p, sb), (sb, sb' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_mr3 {p} : ((sb' p, sm), (sb, sm' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_mr4 {p} : ((sb' p, sr), (sb, sr' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_mr5 {p} : ((sm' p, sb), (sm, sb' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_mr6 {p} : ((sm' p, sr), (sm, sr' p)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml0 {p} : ((sb, sr' p), (sb' p, sr)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml1 {p} : ((sm, sr' p), (sm' p, sr)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml2 {p} : ((sb, sb' p), (sb' p, sb)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml3 {p} : ((sm, sb' p), (sm' p, sb)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml4 {p} : ((sl, sb' p), (sl' p, sb)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml5 {p} : ((sb, sm' p), (sb' p, sm)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d
  | srs_ml6 {p} : ((sl, sm' p), (sl' p, sm)) = ((a, b), (c, d)) -> p < state_bound -> srs_mlr_spec a b c d.

Lemma srs_specI a b c d : In ((a, b), (c, d)) srs -> srs_spec a b c d \/ srs_mlr_spec a b c d.
Proof.
  rewrite /srs. case /in_app_iff.
  { firstorder (by eauto using srs_spec with nocore). }
  case /in_app_iff.
  { move=> /in_flat_map [[? i]] [/inv_nth_error_Some_in_combine].
    move: i => [] [] > /=; firstorder (by eauto using srs_spec with nocore). }
  case /in_app_iff.
  { move=> /in_flat_map [?] [/in_seq] [_ ?].
    firstorder (by eauto using srs_mlr_spec with nocore). }
  case /in_app_iff.
  { move=> /in_flat_map [?] [/in_seq] [_ ?].
    firstorder (by eauto using srs_mlr_spec with nocore). }
  case /in_app_iff.
  { move=> /in_map_iff [?] [?] /in_seq H. left.
    apply: srs_fin0; first by eassumption.
    move: H. rewrite /state_bound. by lia. }
  by firstorder (by eauto using srs_spec with nocore).
Qed.

Lemma In_srsI {a b c d} : srs_spec a b c d \/ srs_mlr_spec a b c d -> In ((a, b), (c, d)) srs.
Proof.
  case.
  - move=> [] > <- *.
    1-2: apply /In_appl; rewrite /=; by tauto.
    1-6: apply /In_appr /In_appl /in_flat_map; eexists;
      (constructor; [apply: nth_error_Some_in_combine; by eassumption | by move=> /=; tauto ]).
    1: apply /In_appr /In_appr /In_appr /In_appr /In_appl /in_map_iff; eexists;
      (constructor; [by reflexivity | apply /in_seq; by lia ]).
    1-5: do 5 (apply /In_appr); move=> /=; by tauto.
  - move=> [] p <- *.
    1-7: apply /In_appr /In_appr /In_appl /in_flat_map; exists p;
      (constructor; [apply /in_seq; by lia | by move=> /=; tauto ]).
    1-7: apply /In_appr /In_appr /In_appr /In_appl /in_flat_map; exists p;
      (constructor; [apply /in_seq; by lia | by move=> /=; tauto ]).
Qed.

Lemma srs_mlr_specE {a b c d} : srs_mlr_spec a b c d ->
  exists x y p,
  ((a, b), (c, d)) = (((x, Some p), (y, None)), ((x, None), (y, Some p))) \/
  ((a, b), (c, d)) = (((x, None), (y, Some p)), ((x, Some p), (y, None))).
Proof. move=> [] > [] ? ? ? ? _; subst; do 3 eexists; by tauto. Qed.

(* resolve In _ srs goals : by eauto with in_srs_db nocore. *)
Local Create HintDb in_srs_db.

Local Hint Resolve or_introl or_intror conj In_srsI : in_srs_db.
Local Hint Immediate erefl : in_srs_db.
Local Hint Constructors srs_spec srs_mlr_spec : in_srs_db.

Definition stepI_nil := (@step_intro srs []).

Lemma move_sb_right {p n} : p < state_bound ->
  multi_step srs ((sb' p) :: repeat sb n) ((repeat sb n) ++ [sb' p]).
Proof.
  move=> Hp. elim: n; first by apply: rt_refl.
  move=> n IH /=. apply: rt_trans;
    [apply: rt_step | apply: (multi_step_applI (u := [sb])); exact: IH].
  apply: stepI_nil. by eauto with in_srs_db nocore.
Qed.

Lemma move_sb_left {p n} : p < state_bound -> multi_step srs ((repeat sb n) ++ [sb' p]) ((sb' p) :: repeat sb n).
Proof.
  move=> Hp. elim: n; first by apply: rt_refl.
  move=> n IH /=. apply: rt_trans;
    [apply: (multi_step_applI (u := [sb])); exact: IH | apply: rt_step].
  apply: stepI_nil. by eauto with in_srs_db nocore.
Qed.

Section Transport.
(* number of steps until halting *)
Context (n_cm: nat).
Definition c0 := {| state := 0; value1 := 0; value2 := 0 |}.
Context (H_n_cm: halting cm (Nat.iter n_cm (CM2.step cm) c0)).

Lemma cm_values_ub n :
  value1 (Nat.iter n (CM2.step cm) c0) + value2 (Nat.iter n (CM2.step cm) c0) <= n_cm.
Proof using H_n_cm.
  have [|->] : n <= n_cm \/ n = ((n - n_cm) + n_cm) by lia.
  - move=> ?. have := values_ub cm c0 n.
    rewrite /c0 /=. by lia.
  - rewrite iter_plus halting_eq; first done.
    have := values_ub cm c0 n_cm.
    rewrite /c0 /=. by lia.
Qed.

Lemma cm_state_ub n : state (Nat.iter n (CM2.step cm) c0) < state_bound.
Proof.
  elim: n; first by (rewrite /= /state_bound; lia).
  move=> n /=. move: (Nat.iter _ _ c0) => [p a b] /=.
  move Hoi: (nth_error cm p) => oi. case: oi Hoi; last done.
  case.
  - by move=> > /state_boundP.
  - move: a b => [|?] [|?] [] > /state_boundP /=; by lia.
Qed.

Definition d := 5 + n_cm + n_cm. (* maximal space requirement *)

(* s is (0^(n-a) l_p _^a m _^b r 0^(n-b)) with a unique state annotation *)
Definition enc_Config : Config -> list Symbol :=
  fun '{| state := p; value1 := a; value2 := b |} =>
    (repeat sz (1 + n_cm-a)) ++ [sl' p] ++ (repeat sb a) ++ [sm] ++
    (repeat sb b) ++ [sr] ++ (repeat sz (1 + n_cm-b)).

(* s is (0^(n-a) l _^a m _^b r_p 0^(n-b)) with a unique state annotation *)
Definition enc_Config' : Config -> list Symbol :=
  fun '{| state := p; value1 := a; value2 := b |} =>
    (repeat sz (1 + n_cm-a)) ++ [sl] ++ (repeat sb a) ++ [sm] ++
    (repeat sb b) ++ [sr' p] ++ (repeat sz (1 + n_cm-b)).

Lemma multi_step_enc_c0 : multi_step srs (repeat sz d) (enc_Config c0).
Proof using.
  apply: (rt_trans (y := (repeat sz (1 + n_cm)) ++ [sz] ++ [st] ++ [sr] ++ (repeat sz (1 + n_cm)))).
  - have ->: d = 1 + n_cm + 1 + 1 + 1 + 1 + n_cm by (rewrite /d; lia).
    rewrite -?repeat_appP -?app_assoc. do ? apply: multi_step_applI.
    apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
  - apply /multi_step_applI /rt_step /stepI_nil. by eauto with in_srs_db nocore.
Qed.

Lemma move_sb_right' {p n x y} : p < state_bound -> ((x, y) = (1, 3) \/ (x, y) = (3, 2)) ->
  multi_step srs ([(x, Some p)] ++ repeat sb n ++ [(y, None)]) ([(x, None)] ++ repeat sb n ++ [(y, Some p)]).
Proof.
  move=> ? /= Hxy. case: n.
  - apply /rt_step /stepI_nil.
    move: Hxy => [] [-> ->]; by eauto with in_srs_db nocore.
  - move=> n. apply: (rt_trans (y := [(x, None)] ++ [sb' p] ++ (repeat sb n) ++ [(y, None)])).
    + have ->: repeat sb (S n) = [sb] ++ repeat sb n by done.
      rewrite /= -?app_assoc. apply /rt_step /stepI_nil.
      move: Hxy => [] [-> _]; by eauto with in_srs_db nocore.
    + rewrite -?app_assoc. apply: multi_step_applI.
      apply: (rt_trans (y := (repeat sb n) ++ [sb' p] ++ [(y, None)])).
      * rewrite ?app_assoc. apply: multi_step_apprI. by apply: move_sb_right.
      * have ->: S n = n + 1 by lia. rewrite -repeat_appP -?app_assoc.
        apply /multi_step_applI /rt_step /stepI_nil.
        move: Hxy => [] [_ ->]; by eauto with in_srs_db nocore.
Qed.

Lemma move_sb_left' {p n x y} : p < state_bound -> ((x, y) = (1, 3) \/ (x, y) = (3, 2)) ->
  multi_step srs ([(x, None)] ++ repeat sb n ++ [(y, Some p)]) ([(x, Some p)] ++ repeat sb n ++ [(y, None)]).
Proof.
  move=> ? /= Hxy. case: n.
  - apply /rt_step /stepI_nil.
    move: Hxy => [] [-> ->]; by eauto with in_srs_db nocore.
  - move=> n. apply: (rt_trans (y := [(x, None)] ++ (repeat sb n) ++ [sb' p] ++ [(y, None)])).
    + rewrite (ltac:(lia) : S n = n + 1) -repeat_appP -?app_assoc. do ? apply: multi_step_applI.
      apply /rt_step /stepI_nil.
      move: Hxy => [] [_ ->]; by eauto with in_srs_db nocore.
    + rewrite ?app_assoc. apply: multi_step_apprI.
      apply: (rt_trans (y := [(x, None)] ++ [sb' p] ++ (repeat sb n))).
      * rewrite -?app_assoc. apply: multi_step_applI. by apply: move_sb_left.
      * apply /rt_step /stepI_nil.
        move: Hxy => [] [-> _]; by eauto with in_srs_db nocore.
Qed.

Lemma move_right n : let c := (Nat.iter n (CM2.step cm) c0) in
  multi_step srs (enc_Config c) (enc_Config' c).
Proof.
  move=> c. subst c. have := cm_state_ub n.
  move: (Nat.iter n _ c0) => [p a b] /= ?.
  apply: multi_step_applI. rewrite ?app_assoc. apply: multi_step_apprI.
  apply: (rt_trans (y := [sl] ++ (repeat sb a) ++ [sm' p] ++ (repeat sb b) ++ [sr])).
  - rewrite ?app_assoc. do 2 apply: multi_step_apprI.
    apply: move_sb_right'; by tauto.
  - rewrite -?app_assoc. do 2 apply: multi_step_applI.
    apply: move_sb_right'; by tauto.
Qed.

Lemma move_left n : let c := (Nat.iter n (CM2.step cm) c0) in
  multi_step srs (enc_Config' c) (enc_Config c).
Proof.
  move=> c. subst c. have := cm_state_ub n.
  move: (Nat.iter n _ c0) => [p a b] /= ?.
  apply: multi_step_applI. rewrite ?app_assoc. apply: multi_step_apprI.
  apply: (rt_trans (y := [sl] ++ (repeat sb a) ++ [sm' p] ++ (repeat sb b) ++ [sr])).
  - rewrite -?app_assoc. do 2 apply: multi_step_applI.
    apply: move_sb_left'; by tauto.
  - rewrite ?app_assoc. do 2 apply: multi_step_apprI.
    apply: move_sb_left'; by tauto.
Qed.

Lemma simulate_cm_step {n} : let c := (Nat.iter n (CM2.step cm) c0) in
  multi_step srs (enc_Config c) (enc_Config (CM2.step cm c)).
Proof using H_n_cm.
  move=> c. subst c.
  have := cm_values_ub n.
  have := move_right n. have := move_left (1+n). move=> /=.
  case: (Nat.iter n _ _) => p a b /=.
  move Hoi: (nth_error cm p) => oi.
  case: oi Hoi; last by (move=> *; apply: rt_refl). case; case.
  (* inc b *)
  - move=> ? /= Hr Hl ?.
    apply: rt_trans; first by eassumption.
    apply: rt_trans; last by eassumption.
    have [-> ->]: S b = b + 1 /\ S n_cm - b = 1 + (S n_cm - (b + 1)) by lia.
    rewrite -?repeat_appP -?app_assoc. do 5 apply: multi_step_applI.
    apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
  (* inc a *)
  - move=> ? _ _ ? /=.
    have [-> ->]: S n_cm - a = (n_cm - a) + 1 /\ S a = 1 + a by lia.
    rewrite -?repeat_appP -?app_assoc. apply: multi_step_applI.
    apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
  (* dec b q *)
  - move=> q ? /= Hr Hl Hb.
    apply: rt_trans; first by eassumption.
    apply: rt_trans; last by eassumption.
    case: (b) Hb => [_ | b' Hb'] /=.
    + do 3 apply: multi_step_applI.
      apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
    + have [-> ->] : S b' = b' + 1 /\ S n_cm - b' = 1 + (S n_cm - (b' + 1)) by lia.
      rewrite -?repeat_appP -?app_assoc. do 5 apply: multi_step_applI.
      apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
  (* dec a q*)
  - move=> q ? _ _ Ha.
    case: (a) Ha => [_ | a' Ha'] /=.
    + apply /multi_step_applI /rt_step /stepI_nil.
      by eauto with in_srs_db nocore.
    + rewrite (ltac:(lia) : (S n_cm - a' = (n_cm - a') + 1)) -repeat_appP -?app_assoc.
      apply /multi_step_applI /rt_step /stepI_nil.
      by eauto with in_srs_db nocore.
Qed.

Lemma multi_step_repeat_solI n : multi_step srs (repeat sz n ++ [so]) (repeat so (n+1)).
Proof.
  elim: n; first by apply: rt_refl.
  move=> n IH. rewrite -repeat_appP.
  have ->: S n = n + 1 by lia.
  apply: (rt_trans (y := repeat sz n ++ [so] ++ [so]));
    last by (rewrite ?app_assoc; apply: multi_step_apprI).
  rewrite -repeat_appP -?app_assoc.
  apply /multi_step_applI /rt_step /stepI_nil.
  by eauto with in_srs_db nocore.
Qed.

Lemma multi_step_repeat_sorI {n x} : x = sb \/ x = sz ->
  multi_step srs ([so] ++ repeat x n) ([so] ++ repeat so n).
Proof.
  move=> Hx. elim: n; first by apply: rt_refl.
  move=> n IH.
  apply: (rt_trans (y := ([so] ++ [so] ++ repeat x n))); last by apply: multi_step_applI.
  apply /rt_step /stepI_nil.
  move: Hx => [] ->; by eauto with in_srs_db nocore.
Qed.

Lemma multi_step_repeat_sorI' {s t n x} : x = sb \/ x = sz ->
  multi_step srs ([so] ++ s) ([so] ++ t) ->
  multi_step srs ([so] ++ repeat x n ++ s) ([so] ++ repeat so n ++ t).
Proof.
  move=> /multi_step_repeat_sorI H1 H2.
  apply: (rt_trans (y := ([so] ++ repeat so n ++ s))).
  - rewrite ?app_assoc. by apply: multi_step_apprI.
  - have ->: [so] = repeat so 1 by done. rewrite ?app_assoc repeat_appP.
    have ->: 1 + n = n + 1 by lia. rewrite -repeat_appP -?app_assoc.
    by apply: multi_step_applI.
Qed.

Lemma simulate_cm_halting {n} : let c := (Nat.iter n (CM2.step cm) c0) in
  halting cm c -> multi_step srs (enc_Config c) (repeat so d).
Proof using H_n_cm.
  move=> c /haltingP. subst c.
  have := cm_values_ub n. have := cm_state_ub n.
  move: (Nat.iter _ _ c0) => [p a b] /= *.
  apply: (rt_trans (y := (repeat sz (n_cm - a)) ++ [so] ++ [so] ++ _)).
  - rewrite (ltac:(lia) : S n_cm - a = (n_cm - a) + 1) -repeat_appP -?app_assoc.
    apply /multi_step_applI /rt_step /stepI_nil.
    by eauto with in_srs_db nocore.
  - apply: (rt_trans (y := (repeat so (n_cm - a + 1) ++ [so] ++
      repeat sb a ++ [sm] ++ repeat sb b ++ [sr] ++ repeat sz (S n_cm - b)))).
    + rewrite ?app_assoc. do 6 apply: multi_step_apprI. by apply: multi_step_repeat_solI.
    + have ->: d = (n_cm - a + 1) + 1 + a + 1 + b + 1 + (S n_cm - b) by (rewrite /d; lia).
      rewrite -?repeat_appP -?app_assoc. do 2 apply: multi_step_applI.
      apply: multi_step_repeat_sorI'; first by left.
      apply: (rt_trans (y := ([so] ++ [so] ++ repeat sb b ++ [sr] ++ repeat sz (S n_cm - b)))).
      * apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
      * apply: multi_step_applI. apply: multi_step_repeat_sorI'; first by left.
        apply: (rt_trans (y := ([so] ++ [so] ++ repeat sz (S n_cm - b)))).
        ** apply /rt_step /stepI_nil. by eauto with in_srs_db nocore.
        ** apply: multi_step_applI. apply: multi_step_repeat_sorI. by right.
Qed.
End Transport.

Lemma transport : CM2_HALT cm -> SR2ab (srs, sz, so).
Proof.
  move=> [n /copy [Hn] /(simulate_cm_halting n Hn) H]. exists (@d n - 1).
  apply: rt_trans; last by eassumption.
  apply: rt_trans; first by apply: (multi_step_enc_c0).
  elim: (n in Nat.iter n); first by apply: rt_refl.
  move=> m IH {H}. apply: rt_trans; [by exact: IH | by apply: simulate_cm_step].
Qed.

Section InverseTransport.
Context (N: nat). (* number of 0s / 1s *)
Context (HN: multi_step srs (repeat sz (1+N)) (repeat so (1+N))). (* 0^N ->> 1^N *)

Local Definition rt_rt1n {A R x y} := @clos_rt_rt1n_iff A R x y.

(* s is (0^n1 l _^a m _^b r 0^n2) with a unique state annotation *)
Definition encodes : Config -> list Symbol -> Prop :=
  fun c s =>
  exists u v t, let '{| state := p; value1 := a; value2 := b |} := c in
    s = u ++ t ++ v /\
    map fst t = map fst ([sl] ++ repeat sb a ++ [sm] ++ repeat sb b ++ [sr]) /\
    filter (fun x => if x is None then false else true) (map snd t) = [Some p].

Lemma In_srs_stE {a b c d} : In ((a, b), (c, d)) srs ->
  ((sz, sz), (st, sr)) = ((a, b), (c, d)) \/
  ((sz, st), (sl' 0, sm)) = ((a, b), (c, d)) \/
  if a is (_, None) then (if b is (_, None) then False else True) else True.
Proof. move=> /srs_specI [] [] > [] ? ? ? ? *; subst; by tauto. Qed.

Lemma init_encodes : exists s, encodes c0 s /\ multi_step srs s (repeat so (1+N)).
Proof using HN.
  have [s] : exists s,
    multi_step srs s (repeat so (1+N)) /\
    Forall (fun x => snd x = None) s /\
    forall n, nth n s sz = st -> nth (1+n) s sz = sr.
  { eexists. constructor; [|constructor]; [by eassumption | apply /Forall_repeatI; by tauto |].
    move: (1+N) => m n H. exfalso. elim: n m H; first by case.
    move=> n IH [|m]; [done | by apply: IH]. }
  move Ht: (repeat so (1+N)) => t [/rt_rt1n Hst] [].
  elim: Hst Ht; first by move=> ? <- /ForallE [].
  move=> {}s {}t > Hst Ht IH /IH {IH}.
  case: Hst Ht => u v a b c d /In_srs_stE [|[]].
  - move=> [] <- <- <- <- _ IH.
    move=> /Forall_app [Hu] /ForallE [_] /ForallE [_ Ht] Huv.
    apply: IH.
    + apply /Forall_app. by do ? constructor.
    + move=> n. have := Huv n. elim: (u) n; first by move=> [|[|n]].
      clear. move=> x {}u IH [|n]; last by move/IH.
      move: (u) => [|? ?]; [by move=> H /H | done].
  - move=> [] <- <- <- <- /rt_rt1n Ht _ _ /(_ (1 + length u)).
    do 2 (rewrite app_nth2; first by lia).
    rewrite (ltac:(lia) : 1 + length u - length u = 1).
    rewrite (ltac:(lia) : 1 + (1 + length u) - length u = 2).
    move=> /(_ ltac:(done)) Hv. eexists. constructor; last by eassumption.
    move: (v) Hv => [|? v']; first done.
    move=> /= ->. exists u, v', [sl' 0; sm; sr].
    constructor; [done | by constructor].
  - move=> H _ _ /Forall_app [_] /ForallE [+] /ForallE [+] _.
    by move: a b H => [? [?|]] [? [?|]].
Qed.

(* possibilities to split two symbols among one app *)
Lemma eq2_app {u v a b} {s t: list Symbol} : u ++ a :: b :: v = s ++ t ->
  (exists v1, v = v1 ++ t /\ s = u ++ a :: b :: v1) \/
  (s = u ++ [a] /\ t = b :: v) \/
  (exists u2, u = s ++ u2 /\ t = u2 ++ a :: b :: v).
Proof.
  elim: u s.
  - move=> [|y1 [|y2 s]].
    + rewrite ?app_nil_l. move=> <-. right. right. by exists [].
    + move=> [] <- <- /=. right. by left.
    + move=> [] <- <- ->. left. by exists s.
  - move=> x1 u IH [|y1 s].
    + rewrite ?app_nil_l. move=> <-. right. right. by exists (x1 :: u).
    + move=> [] <- /IH [|[|]].
      * move=> [?] [-> ->]. left. by eexists.
      * move=> [-> ->]. right. by left.
      * move=> [?] [-> ->]. right. right. by eexists.
Qed.

(* possibilities to split two symbols among one twp apps *)
Lemma eq2_app_app {u a b v u' v'} {s: list Symbol} : length s > 1 ->
  u ++ a :: b :: v = u' ++ s ++ v' ->
  (exists u'2, v = u'2 ++ s ++ v') \/
  (exists s2, u' = u ++ [a] /\ s = b :: s2 /\ v = s2 ++ v') \/
  (exists s1 s2, s = s1 ++ [a] ++ [b] ++ s2 /\ u = u' ++ s1 /\ v = s2 ++ v') \/
  (exists s1, u = u' ++ s1 /\ s = s1 ++ [a] /\ v' = b :: v) \/
  (exists v'1, u = u' ++ s ++ v'1).
Proof.
  move=> Hs /eq2_app [|[|]].
  - move=> [?] [-> ->]. left. by eexists.
  - move=> [->]. move: s Hs => [|? s] /=; first by lia.
    move=> _ [] <- <-. right. left. by eexists.
  - move=> [?] [->] /esym /eq2_app [|[|]].
    + move=> [?] [-> ->]. right. right. left. by do 2 eexists.
    + move=> [-> ->]. do 3 right. left. by eexists.
    + move=> [?] [-> ->]. do 4 right. by eexists.
Qed.

(* specification of inner Cm2 step *)
Inductive srs_step_spec (u v: list Symbol) (a b: Symbol) (n m: nat) : Prop :=
  | srs_step0 : a.1 = sl.1 -> b.1 = sm.1 -> u = [] -> n = 0 -> srs_step_spec u v a b n m
  | srs_step1 : a.1 = sl.1 -> b.1 = sb.1 -> u = [] -> n = 1 + (n - 1) -> srs_step_spec u v a b n m
  | srs_step2 : a.1 = sm.1 -> b.1 = sr.1 -> v = [] -> m = 0 -> srs_step_spec u v a b n m
  | srs_step3 : a.1 = sb.1 -> b.1 = sr.1 -> v = [] -> m = 1 + (m - 1) -> srs_step_spec u v a b n m.

Lemma srs_step_specI {u v a b n m} :
  map fst (u ++ [a] ++ [b] ++ v) = map fst ([sl] ++ repeat sb n ++ [sm] ++ repeat sb m ++ [sr]) ->
  srs_step_spec u v a b n m \/
  (a.1 = sb.1 /\ b.1 = sb.1) \/ (a.1 = sb.1 /\ b.1 = sm.1) \/ (a.1 = sm.1 /\ b.1 = sb.1).
Proof.
  move: u => [|? u].
  { move: n => [|n].
    - move=> [] *. left. by apply: srs_step0.
    - move=> [] *. left. apply: srs_step1; by [|lia]. }
  move=> [] _. rewrite -/(_ ++ _).
  elim /rev_ind: v.
  { rewrite app_nil_r ?map_app /=.
    rewrite ?app_assoc. move=> /app_inj_tail [].
    have [->|->] : m = 0 \/ m = (m - 1) + 1 by lia.
    - rewrite app_nil_r. move=> /app_inj_tail [] *. left. by apply: srs_step2.
    - rewrite -repeat_appP map_app ?app_assoc.
      move=> /app_inj_tail [] *. left. apply: srs_step3; by [|lia]. }
  move=> ? v _. rewrite ?map_app ?app_assoc.
  move=> /app_inj_tail [+] _. move=> + /ltac:(right).
  elim: u n.
  { move=> [|[|n]].
    - move: m => [|m [] *]; [done | by tauto ].
    - move=> [] *. by tauto.
    - move=> [] *. by tauto. }
  move=> ? u IH [|n]; last by move=> [_] /IH.
  move=> [_] {IH}. rewrite -?/(_ ++ _). elim: m u; first by case.
  move=> m IH [|? u]; last by move=> [_] /IH.
  move: m {IH} => [|m] []; [done | by tauto].
Qed.

(* each srs step is sound *)
Lemma simulate_srs_step {c s t} : SR2ab.step srs s t -> encodes c s ->
  halting cm c \/ encodes c t \/ encodes (CM2.step cm c) t.
Proof.
  move: c => [p a b] [] u v a' b' c' d' H [u'] [v'] [{}t].
  rewrite -?/([_] ++ [_] ++ v). move=> [+] [H1t H2t] => /eq2_app_app.
  have : length t > 1.
  { move: H1t => /(congr1 (@length _)).
    rewrite ?map_app ?app_length ?map_length /=. move=> ->. by lia. }
  move=> Ht /(_ Ht) {Ht}.
  case; [|case; [|case; [|case]]].
  - move=> [u'2 ->]. right. left.
    exists (u ++ c' :: d' :: u'2), v', t.
    constructor; [by rewrite -?app_assoc | done].
  - move=> [s2] [?] [? ?]. subst. move: H1t H2t => [].
    move: H => /srs_specI [|] [] > [] ? ? ? ?; subst; try done; [|].
    + move=> Hi _ H1s2 [<- H2s2]. right. right.
      rewrite /= Hi. eexists u, v', (_ :: _ :: s2).
      constructor; [done | constructor; by rewrite /= ?H1s2 ?H2s2].
    + move=> ? _ _ [<-] _ *. left.
      apply /haltingP => /=. by lia.
  - move=> [s1] [s2] [?] [? ?]. subst.
    move: H H1t H2t => /srs_specI [].
    + move=> H + + /ltac:(right; right). move=> /copy [/srs_step_specI] [].
      * move=> H'. move: H' H => [] ? ? ? ? [] > [] ? ? ? ?; subst; try done; [ | | | ].
        ** rewrite app_nil_r /=. move=> + [H1] [<-] => -> H2.
           eexists u', v', (_ :: _ :: _). constructor; [done | by rewrite /= H1 H2].
        ** rewrite app_nil_r /= ?map_app. move: (a) => [|?]; first done.
           move=> + [] H1 [<-] H2 => ->.
           eexists (u' ++ [sz]), v', (_ :: _).
           rewrite -?app_assoc. constructor; [done | by rewrite /= ?map_app H1 H2].
        ** rewrite ?map_app filter_app /= app_nil_r.
           move=> + + /(app_inj_tail (y := [])) [H2] [<-].
           move=> ->. rewrite ?app_assoc app_nil_r.
           move=> /app_inj_tail [/app_inj_tail] [H1] _ _.
           eexists u', v', (_ ++ [_; _]).
           rewrite -?app_assoc. constructor; first done.
           by rewrite ?map_app filter_app /= H1 H2.
        ** rewrite [in repeat sb b](ltac:(lia) : b = (b - 1) + 1) -repeat_appP.
           rewrite ?map_app ?filter_app ?app_assoc ?app_nil_r /=.
           move=> + + /(app_inj_tail (y := [])) [H2] [<-].
           move=> ->. move=> /app_inj_tail [/app_inj_tail] [H1] _ _.
           eexists u', ([sz] ++ v'), (_ ++ [_]).
           rewrite (ltac:(lia) : b = 1 + (b - 1)) -?app_assoc /=.
           constructor; first done.
           by rewrite ?map_app filter_app /= H1 H2 -?app_assoc.
      * move: H => + + _ /ltac:(exfalso).
        move=> [] > [] *; subst; by firstorder done.
    + move=> + + + /ltac:(right; left; exists u', v', (s1 ++ c' :: d' :: s2)).
      move=> /srs_mlr_specE [x] [y] [q] [] [] ? ? ? ? H1t H2t;
        subst; rewrite -?app_assoc.
      * constructor; first done.
        constructor; first by rewrite -H1t ?map_app.
        move: H2t. by rewrite ?map_app ?filter_app /=.
      * constructor; first done.
        constructor; first by rewrite -H1t ?map_app.
        move: H2t. by rewrite ?map_app ?filter_app /=.
  - move=> [s1] [?] [? ?]. subst.
    move: (H1t). rewrite ?map_app ?app_assoc. move=> /app_inj_tail [_].
    move: H H1t H2t => /srs_specI [|] [] > [] ? ? ? ?; subst; try done; [].
    move=> Hi H1s1. rewrite map_app filter_app.
    move=> /(app_inj_tail (y := [])) [H2s2] [<-] _.
    right. right. rewrite /= Hi. eexists u', v, (s1 ++ [_; _]).
    rewrite -?app_assoc. constructor; [done | constructor].
    * move: H1s1. rewrite ?map_app ?app_assoc. move=> /app_inj_tail [-> _].
      by rewrite (ltac:(lia) : 1 + b = b + 1) -[repeat _ (b + 1)]repeat_appP map_app -?app_assoc.
    * by rewrite map_app filter_app /= H2s2.
  - move=> [v'1 ->]. right. left.
    exists u', (v'1 ++ c' :: d' :: v), t.
    constructor; [by rewrite -?app_assoc | done].
Qed.

Lemma halting_cmI : exists n, halting cm (Nat.iter n (CM2.step cm) c0).
Proof using HN.
  have [s [H1s H2s]] := init_encodes.
  move Ht: (repeat so (1+N)) (c0) H2s H1s => t c Hst.
  have {}Ht : Forall (fun x => fst so = x) (map fst t).
  { subst t. elim: (N); by constructor. }
  move: Hst Ht c. move=> /rt_rt1n. elim.
  - move=> {}s Hs [? ? ?] /= [?] [?] [{}t] [?] [H]. subst s.
    move: Hs. rewrite ?map_app ?Forall_app H.
    by move=> [_] [/ForallE] [].
  - move=> > /simulate_srs_step H _ IH /IH {}IH c /H {H} [|[]].
    + move=> ?. by exists 0.
    + by move=> /IH.
    + move=> /IH [n Hn]. exists (n + 1). by rewrite iter_plus.
Qed.

End InverseTransport.

Lemma inverse_transport : SR2ab (srs, sz, so) -> CM2_HALT cm.
Proof. move=> [n Hn]. apply: halting_cmI. by eassumption. Qed.

End Reduction.
End Argument.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction : CM2_HALT SR2ab.
Proof.
  exists (fun cm => (Argument.srs cm, (4, None), (5, Some 0))).
  intro cm. constructor.
  - exact (Argument.transport cm).
  - exact (Argument.inverse_transport cm).
Qed.