Require Import List Relation_Operators Operators_Properties Lia.
Import ListNotations.

Require Import Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.SR2ab.
Require Import Undecidability.StringRewriting.SSTS.

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

Require Import ssreflect ssrbool ssrfun.

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

Local Arguments rt_trans {A R x y z}.

Definition enc_pair '(x, y) : nat := (x + y) * (x + y) + y.

Lemma enc_pair_inj {xy x'y'} : enc_pair xy = enc_pair x'y' -> xy = x'y'.
Proof.
  move: xy x'y' => [x y] [x' y'] /=. rewrite pair_equal_spec.
  have : x + y <> x' + y' \/ x + y = x' + y' by lia.
  case; by nia.
Qed.

Opaque enc_pair.

Module Argument.
Section Reduction.
Context (srs : Srs) (a0: Symbol) (b0: Symbol) (Ha0b0: b0 <> a0).

Import SR2ab_facts (sym_eq_dec).

Definition enc (x: Symbol) : nat :=
  if sym_eq_dec x a0 then 0
  else if sym_eq_dec x b0 then 1
  else 2 + (
    match x with
    | (n, None) => enc_pair (n, 0)
    | (n, Some m) => enc_pair (n, 1 + m)
    end).

Definition ssts : Ssts := map (fun '((a, b), (c, d)) => ((enc a, enc b), (enc c, enc d))) srs.

Lemma sim_step {s t} : SR2ab.step srs s t -> SSTS.step ssts (map enc s) (map enc t).
Proof.
  case => > ?. rewrite ?map_app /=.
  apply: step_intro. rewrite /ssts in_map_iff.
  eexists. by constructor; last by eassumption.
Qed.

Lemma enc_inj {a b} : enc a = enc b -> a = b.
Proof.
  rewrite /enc. move: (sym_eq_dec a a0) (sym_eq_dec a b0) (sym_eq_dec b a0) (sym_eq_dec b b0).
  move=> [] ? [] ? [] ? [] ? /=; try congruence.
  move: (a) (b) => [? [?|]] [? [?|]] /= [] /enc_pair_inj []; by congruence.
Qed.

Lemma map_enc_inj {s t} : map enc s = map enc t -> s = t.
Proof.
  elim: s t; first by case.
  move=> ? ? IH [|? ?]; first done.
  by move=> /= [/enc_inj -> /IH ->].
Qed.

Lemma inv_sim_step {s t'} : SSTS.step ssts (map enc s) t' -> exists t, t' = map enc t /\ SR2ab.step srs s t.
Proof.
  move Hs': (map enc s) => s' Hs't'.
  case: Hs't' Hs' => u' v' a' b' c' d' H Hs.
  move: H. rewrite /ssts in_map_iff. move=> [[[a b]]] [c d] [[]] ? ? ? ?. subst.
  move=> H. exists (firstn (length u') s ++ c :: d :: skipn (length u' + 2) s). constructor.
  - rewrite map_app /= -firstn_map -skipn_map Hs.
    rewrite firstn_app (ltac:(lia) : length u' - length u' = 0) firstn_all.
    rewrite skipn_app (ltac:(lia) : length u' + 2 - length u' = 2) skipn_all2 /=; first by lia.
    by rewrite app_nil_r.
  - move: H => /SR2ab_facts.stepI. apply; last done.
    apply: map_enc_inj. rewrite Hs map_app /= -firstn_map -skipn_map Hs.
    rewrite firstn_app (ltac:(lia) : length u' - length u' = 0) firstn_all.
    rewrite skipn_app (ltac:(lia) : length u' + 2 - length u' = 2) skipn_all2 /=; first by lia.
    by rewrite app_nil_r.
Qed.

Lemma repeat_a0 {n} : repeat 0 n = map enc (repeat a0 n).
Proof.
  elim: n; first done.
  move=> n /= ->. congr cons.
  rewrite /enc. by case: (sym_eq_dec a0 a0).
Qed.

Lemma repeat_b0 {n} : repeat 1 n = map enc (repeat b0 n).
Proof using Ha0b0.
  elim: n; first done.
  move=> n /= ->. congr cons.
  rewrite /enc. case: (sym_eq_dec b0 a0); [done | by case: (sym_eq_dec b0 b0)].
Qed.

Lemma transport : SR2ab (srs, a0, b0) -> SSTS01 ssts.
Proof using Ha0b0.
  move=> [n Hn]. exists n. move: Hn. rewrite repeat_a0 repeat_b0.
  move: (repeat a0 _) (repeat b0 _) => s t. elim.
  - move=> > ?. apply: rt_step. by apply: sim_step.
  - move=> *. by apply rt_refl.
  - move=> *. apply: rt_trans; by eassumption.
Qed.

Lemma inverse_transport : SSTS01 ssts -> SR2ab (srs, a0, b0).
Proof using Ha0b0.
  move=> [n Hn]. exists n. move: Hn. rewrite repeat_a0 repeat_b0.
  move: (repeat a0 _) (repeat b0 _) => s t.
  move Hs': (map enc s) => s'. move Ht': (map enc t) => t' /(@clos_rt_rt1n_iff _ _) Hs't'.
  elim: Hs't' s t Hs' Ht'.
  - move=> ? s t *. subst. have -> : s = t by apply: map_enc_inj.
    by apply rt_refl.
  - move=> > IH1 _ IH2 *. subst. move: IH1 => /inv_sim_step [t] [? ?]. subst.
    apply /rt_trans; [apply: rt_step; by eassumption | by apply: IH2].
Qed.

End Reduction.
End Argument.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction : SR2ab ⪯ SSTS01.
Proof.
  exists (fun '(srs, a0, b0) =>
    if SR2ab_facts.sym_eq_dec b0 a0 then [((0, 0), (1, 1))] else Argument.ssts srs a0 b0).
  move=> [[srs a0] b0]. constructor.
  - case: (SR2ab_facts.sym_eq_dec b0 a0).
    + move=> *. exists 1. rewrite /=. apply: rt_step.
      apply: (step_intro _ (u := [])). by left.
    + move=> H /=. by apply: Argument.transport.
  - case: (SR2ab_facts.sym_eq_dec b0 a0).
    + move=> /= -> _. exists 0. by apply: rt_refl.
    + move=> /= H. by apply: Argument.inverse_transport.
Qed.