From Coq Require List Vector.

From Undecidability.L Require Import L Datatypes.Lists Datatypes.LNat.
From Undecidability.TM Require Import TM Util.TM_facts.

Import ListNotations Vector.VectorNotations.

Definition encBoolsListTM {Σ : Type} (s b : Σ) (l : list bool) :=
  (map (fun (x : bool) => (if x then s else b)) l).

Definition encBoolsTM {Σ : Type} (s b : Σ) (l : list bool) :=
  @midtape Σ [] b (encBoolsListTM s b l).

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

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

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).

Definition TM₁_bool_computable {k} (Σ : finType) (R : Vector.t (list bool) k -> (list bool) -> Prop) :=
  exists s1 s2 b : Σ, s1 <> s2 /\ s1 <> b /\ s2 <> b /\
  exists M : TM Σ 1,
  forall v : Vector.t (list bool) k,
  (forall m, R v m <-> exists q, TM.eval M (start M) [midtape [] b (Vector.fold_right (fun l s => encBoolsListTM s1 s2 l ++ s)%list v List.nil)] q [encBoolsTM s1 s2 m]) /\
  (forall q t, TM.eval M (start M) [midtape [] b (Vector.fold_right (fun l s => encBoolsListTM s1 s2 l ++ s)%list v List.nil)] q t ->
          exists m, t = [encBoolsTM s1 s2 m]).

Definition encBoolsL (l : list bool) := list_enc l.

Definition L_bool_computable {k} (R : Vector.t (list bool) k -> (list bool) -> Prop) :=
  exists s, forall v : Vector.t (list bool) k,
      (forall m, R v m <-> L.eval (Vector.fold_left (fun s n => L.app s (encBoolsL n)) s v) (encBoolsL m)) /\
      (forall o, L.eval (Vector.fold_left (fun s n => L.app s (encBoolsL n)) s v) o -> exists m, o = encBoolsL m).

Definition encNatL (n : nat) := nat_enc n.

Definition L_computable {k} (R : Vector.t nat k -> nat -> Prop) :=
  exists s, forall v : Vector.t nat k,
      (forall m, R v m <-> L.eval (Vector.fold_left (fun s n => L.app s (encNatL n)) s v) (encNatL m)) /\
      (forall o, L.eval (Vector.fold_left (fun s n => L.app s (encNatL n)) s v) o -> exists m, o = encNatL m).