Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef.
Require Import Vector List.

Unset Implicit Arguments.



Section Fix_Sigma.

  Variable Σ : Type.


  Inductive tape : Type :=
  | niltape : tape
  | leftof : Σ -> list Σ -> tape
  | rightof : Σ -> list Σ -> tape
  | midtape : list Σ -> Σ -> list Σ -> tape.


  Definition current (t : tape) : option Σ :=
    match t with
    | midtape _ a _ => Some a
    | _ => None
    end.

  Inductive move : Type := Lmove : move | Rmove : move | Nmove : move.


  Definition mv (m : move) (t : tape) :=
    match m, t with
    | Lmove, rightof l ls => midtape ls l nil
    | Lmove, midtape nil m rs => leftof m rs
    | Lmove, midtape (l :: ls) m rs => midtape ls l (m :: rs)
    | Rmove, leftof r rs => midtape nil r rs
    | Rmove, midtape ls m nil => rightof m ls
    | Rmove, midtape ls m (r :: rs) => midtape (m :: ls) r rs
    | _, _ => t
    end.


  Definition wr (s : option Σ) (t : tape) : tape :=
    match s, t with
    | None, t => t
    | Some a, niltape => midtape nil a nil
    | Some a, leftof r rs => midtape nil a (r :: rs)
    | Some a, midtape ls b rs => midtape ls a rs
    | Some a, rightof l ls => midtape (l :: ls) a nil
    end.

End Fix_Sigma.


Arguments niltape _, {_}.
Arguments leftof _ _ _, {_} _ _.
Arguments rightof _ _ _, {_} _ _.
Arguments midtape _ _ _ _, {_} _ _ _.

Arguments current {_} _.

Arguments wr {_} _ _.
Arguments mv {_} _.

Section Fix_Alphabet.

  Variable Σ : finType.


  Variable n : nat.

  Record TM : Type :=
    {
    
    state : finType;
    
    trans : state * (Vector.t (option Σ) n) -> state * (Vector.t ((option Σ) * move) n);
    
    start: state;
    
    halt : state -> bool
    }.

  Inductive eval (M : TM) (q : state M) (t : Vector.t (tape Σ) n) : state M -> Vector.t (tape Σ) n -> Prop :=
  | eval_halt :
      halt M q = true ->
      eval M q t q t
  | eval_step q' a q'' t' :
      halt M q = false ->
      trans M (q, Vector.map current t) = (q', a) ->
      eval M q' (Vector.map2 (fun tp '(c,m) => mv m (wr c tp)) t a) q'' t' ->
      eval M q t q'' t'.

End Fix_Alphabet.

Arguments state {_ _} m : rename.
Arguments trans {_ _} m _, {_ _ m} _ : rename.
Arguments start {_ _} m : rename.
Arguments halt {_ _} m _, {_ _ m} _ : rename.

Arguments eval {_ _} _ _ _ _ _.

Arguments Build_TM {_ _ _} _ _ _.

Definition HaltsTM {Σ: finType} {n: nat} (M : TM Σ n) (t : Vector.t (tape Σ) n) :=
  exists q' t', eval M (start M) t q' t'.
Arguments HaltsTM _ _ _ _, {_ _} _ _.

Definition HaltTM (n : nat) : {Σ : finType & TM Σ n & Vector.t (tape Σ) n} -> Prop :=
  fun '(existT2 _ _ Σ M t) => HaltsTM M t.

Definition HaltMTM : {'(n,Σ) : nat * finType & TM Σ n & Vector.t (tape Σ) n} -> Prop :=
  fun '(existT2 _ _ (n, Σ) M t) => HaltsTM M t.

Import ListNotations Vector.VectorNotations.

Definition encNatTM {Σ : Type} (s b : Σ) (n : nat) :=
  @midtape Σ [] b (repeat s n).

Definition TM_computable {k} (R : Vector.t nat k -> nat -> Prop) :=
  exists n : nat, exists Σ : finType, exists s b : Σ, s <> b /\
  exists M : TM Σ (1 + k + n),
  forall v : Vector.t nat k,
  (forall m, R v m <-> exists q t, TM.eval M (start M) ((niltape :: Vector.map (encNatTM s b) v) ++ Vector.const niltape n) q t
                                /\ Vector.hd t = encNatTM s b m) /\
  (forall q t, TM.eval M (start M) ((niltape :: Vector.map (encNatTM s b) v) ++ Vector.const niltape n) q t ->
          exists m, Vector.hd t = encNatTM s b m).