From Undecidability Require TM.TM TM.Util.TM_facts.
From Undecidability Require Import TM.SBTM TM.Util.SBTM_facts.
Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes.

Require Import PeanoNat Lia.

#[local] Unset Implicit Arguments.
#[local] Unset Strict Implicit.

Require Import List ssreflect ssrbool ssrfun.
Import ListNotations SBTMNotations.

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

#[local] Notation "| a |" := (Vector.cons _ a 0 (Vector.nil _)).

Section Construction.
  Context (M : SBTM) (q0 : state M).

  Definition encode_tape (t : tape) : TM.tape (finType_CS bool) :=
    match t with
    | (ls, a, rs) => TM.midtape ls a rs
    end.

  #[local] Notation state' := (option (Fin.t ((num_states M)))).

  Definition finTypeC_state' : finType :=
    @finType_CS state' _ (CompoundFinTypes.finTypeC_Option _).

  Definition halt' (q : state') : bool := if q is None then true else false.

  Definition get_symbol (ob : option (finType_CS bool)) : bool :=
    match ob with
    | None => false
    | Some b => b
    end.

  Definition encode_direction (d : direction) :=
    match d with
    | go_left => TM.Lmove
    | go_right => TM.Rmove
    end.

  Definition M' : TM.TM (finType_CS bool) 1.
  Proof using M q0.
    refine (@TM.Build_TM _ _ finTypeC_state' (fun '(q, bs) => _) (Some q0) halt').
    refine (
      match q with
      | Some qM => _
      | None => (None, | (None, TM.Nmove) | )
      end).
    refine (
      match trans' M (qM, get_symbol (Vector.hd bs)) with
      | None => (None, | (None, TM.Nmove) | )
      | Some (q', a', d') => (Some q', | (Some a',encode_direction d') | )
      end).
  Defined.

  #[local] Notation TM_step x := (@TM_facts.step _ _ M' x).
  #[local] Notation TM_config := (@TM_facts.mconfig (finType_CS bool) (TM.state M') 1).

  Definition encode_config : config M -> TM_config :=
    fun '(q, t) => TM_facts.mk_mconfig (Some q) (| encode_tape t |).

  Definition canonize_tape (t : TM.tape (finType_CS bool)) :=
    match t with
    | TM.niltape => TM.midtape [] false []
    | TM.leftof r rs => TM.midtape [] false (r :: rs)
    | TM.rightof l ls => TM.midtape (l :: ls) false []
    | _ => t
    end.

  Lemma get_symbol_canonize_tape {t1 t2} :
    canonize_tape t1 = canonize_tape t2 ->
    get_symbol (TM.current t1) = get_symbol (TM.current t2).
  Proof.
    move: t1 t2 => [ | ?? | ?? | ???] [] > /=; congruence.
  Qed.

  Lemma doAct_canonize_tape {t1 t2} a d :
    canonize_tape t1 = canonize_tape t2 ->
    canonize_tape (TM_facts.doAct t1 (Some a, encode_direction d)) =
    canonize_tape (TM_facts.doAct t2 (Some a, encode_direction d)).
  Proof.
    move: d t1 t2.
    move=> [] [ | ?? | ?? | [|??]?[|??] ] [ | ?? | ?? | [|??]?[|??] ] /=; cbn; congruence.
  Qed.

  Lemma TM_step_canonize_tape oq oq1 t1 t'1 oq2 t2 t'2 :
    canonize_tape t1 = canonize_tape t2 ->
    TM_step (TM_facts.mk_mconfig oq (| t1 |)) = TM_facts.mk_mconfig oq1 (| t'1 |) ->
    TM_step (TM_facts.mk_mconfig oq (| t2 |)) = TM_facts.mk_mconfig oq2 (| t'2 |) ->
    oq1 = oq2 /\ canonize_tape t'1 = canonize_tape t'2.
  Proof.
    move=> Ht1t2.
    rewrite /TM_facts.step /= -(get_symbol_canonize_tape Ht1t2).
    case: oq => [q|].
    - move: (trans' M _) => [[[q' a'] d']|] /=.
      + move=> [] <- <- [] <- <-. split; first done.
        by apply: doAct_canonize_tape.
      + by move=> [] <- <- [] <- <-.
    - by move=> [] <- <- [] <- <-.
  Qed.

  Lemma TM_loopM_canonize_tape (oq : TM.state M') t1 t2 k q' t'1 :
    canonize_tape t1 = canonize_tape t2 ->
    TM_facts.loopM (TM_facts.mk_mconfig oq (| t1 |)) k = Some (TM_facts.mk_mconfig q' t'1) ->
    { t'2 | TM_facts.loopM (TM_facts.mk_mconfig oq (| t2 |)) k = Some (TM_facts.mk_mconfig q' t'2) }.
  Proof.
    elim: k oq t1 t2.
    { move=> > _ /=. case: (halt' _) => [|]; last done.
      move=> [] /= -> _. by eexists. }
    move=> k IH oq t1 t2 Ht1t2 /=.
    case: (halt' _) => [|] /=. { move=> [] -> _. by eexists. }
    move E1: (TM_step _) => [q1 ts1]. move E2: (TM_step _) => [q2 ts2].
    move: E1 E2.
    rewrite (Vector.eta ts1). move: (VectorDef.tl ts1). apply: Vector.case0.
    rewrite (Vector.eta ts2). move: (VectorDef.tl ts2). apply: Vector.case0.
    move: (Ht1t2) => /TM_step_canonize_tape /[apply] /[apply].
    move=> [<-] /IH. by apply.
  Qed.

  Lemma simulation_step q t q' t' : step M (q, t) = Some (q', t') ->
    { t'' |
      TM_step (encode_config (q, t)) = TM_facts.mk_mconfig (Some q') (| t'' |) /\
      encode_tape t' = canonize_tape t'' }.
  Proof.
    rewrite /step /TM_facts.step /=.
    move: t => [[ls a] rs] /=. case: (trans' M _) => [[[? ?] d]|] /=; last done.
    move=> [] -> <-. case: d => /=.
    - case: ls => [|??] /=; eexists; split; reflexivity.
    - case: rs => [|??] /=; eexists; split; reflexivity.
  Qed.

  Lemma simulation_halt q t : step M (q, t) = None ->
    TM_step (encode_config (q, t)) = TM_facts.mk_mconfig None (| encode_tape t |).
  Proof.
    rewrite /step /TM_facts.step /=.
    move: t => [[ls a] rs] /=.
    by case: (trans' M _) => [[[? ?] d]|] /=.
  Qed.

  Lemma simulation q t k :
    steps M k (q, t) = None ->
    exists q' ts', TM.eval M' (Some q) (| encode_tape t |) q' ts'.
  Proof.
    elim: k q t; first done.
    move=> k IH q t.
    rewrite (steps_plus 1 k). case E: (steps M 1 _) => [[q' t']|].
    - move: E => /simulation_step [t'' [HM' Ht't'']] /IH.
      move=> [q'''] [t'''] /TM_facts.TM_eval_iff [k'].
      rewrite Ht't''. move=> /TM_loopM_canonize_tape => /(_ t'').
      move=> /(_ ltac:(by case: (t''))). move=> [{}t''' ?].
      exists q''', t'''. apply /TM_facts.TM_eval_iff. exists (S k').
      by rewrite /= HM'.
    - move=> _. exists None, (| encode_tape t |).
      apply /TM_facts.TM_eval_iff. exists 1.
      move: E.
      rewrite /= /step /TM_facts.step /=.
      move: t => [[ls a] rs] /=.
      by case: (trans' M (q, a)) => [[[??]?]|].
  Qed.

  Lemma inverse_simulation q t q' ts' :
    TM.eval M' (Some q) (| encode_tape t |) q' ts' ->
    exists k, steps M k (q, t) = None.
  Proof.
    move=> /TM_facts.TM_eval_iff => - [k Hk]. exists k.
    elim: k q t q' ts' Hk; first done.
    move=> k IH q t q' ts' Hk. rewrite (steps_plus 1 k).
    case Hqt: (steps M 1 (q, t)) => [[q'' t'']|]; last done.
    move: Hqt => /simulation_step [t'''] [H'qt Et''t'''].
    move: Hk => /=. rewrite H'qt.
    have : canonize_tape t''' = canonize_tape (encode_tape t'').
    { rewrite Et''t'''. by case: (t'''). }
    by move=> /TM_loopM_canonize_tape /[apply] => - [?] /IH.
  Qed.

End Construction.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction :
  SBTM_HALT ⪯ TM.HaltTM 1.
Proof.
  exists ((fun '(existT _ M (q, t)) =>
    existT2 _ _ (finType_CS bool) (M' M q) (| encode_tape t |)) ).
  move=> [M [q t]] /=. split.
  - by move=> [k] /simulation => /(_ q).
  - by move=> [?] [?] /inverse_simulation.
Qed.