Require Import List Bool Nat.
Require Coq.Vectors.Fin.
Import ListNotations.

Definition tape : Type := list bool * option bool * list bool.

Definition left '( (ls, m, rs) : tape) : list bool := ls.

Definition right '((ls, m, rs) : tape) := rs.

Definition curr '((ls, m, rs) : tape) := m.

Definition wr (o : option bool) (t : tape) :=
  match o with
  | Some c => (left t, Some c, right t)
  | None => t
  end.

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

Definition mv (m : move) (t : tape) :=
  match m with
  | Lmove => match left t, curr t with
             | l :: ls, None => (ls, Some l, right t)
             | l :: ls, Some c => (ls, Some l, c :: right t)
             | [], Some c => ([], None, c :: right t)
             | _, _ => t
             end
  | Rmove => match curr t, right t with
             | None, r :: rs => (left t, Some r, rs)
             | Some c, r :: rs => (c :: left t, Some r, rs)
             | Some c, [] => (c :: left t, None, [])
             | _ , _ => t
             end
  | Nmove => t
  end.

Record SBTM := { num_states : nat ; trans : Fin.t (S num_states) * option bool -> option (Fin.t (S num_states) * option bool * move)}.

Notation state M := (Fin.t (S (num_states M))).

Inductive eval (M : SBTM) : state M -> tape -> state M -> tape -> Prop :=
| eval_halt q t :
    trans M (q, (curr t)) = None ->
    eval M q t q t
| eval_step q t q' w m q'' t' :
    trans M (q, curr t) = Some (q', w, m) ->
    eval M q' (mv m (wr w t)) q'' t' ->
    eval M q t q'' t'.

Definition HaltSBTM '( (M, t) : SBTM * tape) :=
  exists q' t', eval M (Fin.F1) t q' t'.

Definition HaltSBTMu : { M : SBTM & {q : state M | forall c, trans M (q,c) = None /\ forall q', trans M (q',c) = None -> q' = q }} * tape -> Prop := fun '((existT _ M (exist _ q H)), t) => exists t', eval M Fin.F1 t q t'.