Definition of Multi-Tape Turing Machines

Definitions of tapes and (unlabelled) multi-tape Turing machines from Asperti, Riciotti "A formalization of multi-tape Turing machines" (2015) and the accompanying Matita code.

From Undecidability Require Export TM.Prelim TM.Relations.
Require Import PslBase.Vectors.Vectors.

Section Fix_Sigma.

Variable sig : Type.

Definition of the tape

A tape is essentially a triple 〈left,current,right〉 where, however, the current symbol could be missing. This may happen for three different reasons: both tapes are empty, we are on the left extremity of a non-empty tape (left overflow), or we are on the right extremity of a non-empty tape (right overflow).

Note that the alphabet has type Type, not finType.

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

  Definition tapes n := Vector.t tape n.

  Definition tapeToList (t : tape) : list sig :=
    match t with
    | niltape => []
    | leftof s r => s :: r
    | rightof s l => List.rev (s :: l)
    | midtape l c r => (List.rev l) ++ [c] ++ r
    end.

  Definition sizeOfTape t := |tapeToList t|.

  Definition sizeOfmTapes n (v : tapes n) :=
    Vector.fold_left max 0 (Vector.map sizeOfTape v).

  Definition current :=
    fun (t : tape) =>
      match t with
      | midtape _ c _ => Some c
      | _ => None
      end.

  Definition left :=
    fun (t : tape) =>
      match t with
      | niltape => []
      | leftof _ _ => []
      | rightof s l => s :: l
      | midtape l _ _ => l
      end.

  Definition right :=
    fun (t : tape) =>
      match t with
      | niltape => []
      | leftof s r => s :: r
      | rightof _ _ => []
      | midtape _ _ r => r
      end.

Lemmas for midtape

  Lemma tape_midtape_current_right t rs s :
    current t = Some s ->
    right t = rs ->
    t = midtape (left t) s rs.
  Proof. destruct t; cbn; congruence. Qed.

  Lemma tape_midtape_current_left t ls s :
    current t = Some s ->
    left t = ls ->
    t = midtape ls s (right t).
  Proof. destruct t; cbn; congruence. Qed.

  Lemma tape_is_midtape t ls s rs :
    left t = ls ->
    current t = Some s ->
    right t = rs ->
    t = midtape ls s rs.
  Proof. destruct t; cbn; congruence. Qed.

Definition of moves

Inductive move : Type := L : move | R : move | N : move.

Declare discreteness of move

  Global Instance move_eq_dec : eq_dec move.
  Proof.
    intros. hnf. decide equality.
  Defined.

Declare finiteness of move

  Global Instance move_finC : finTypeC (EqType move).
  Proof.
    apply (FinTypeC (enum := [L ; R ; N ])).
    intros []; now cbv.
  Defined.

We outsource the second match of tape_move_right in the midtape case to another named definition. This has the advantage that the cbn tactic will not reduce tape_move_left (midtape ls m rs) to a long term that contains match. It reduces to tape_move_left' ls m rs instead. Furthermore, there are rewrite lemmas available for tape_move_left'.

  Definition tape_move_right' ls a rs :=
    match rs with
    | nil => rightof a ls
    | r::rs' => midtape (a ::ls) r rs'
    end.

  Definition tape_move_right :=
    fun (t : tape) =>
      match t with
      | niltape => niltape
      | rightof _ _ =>t
      | leftof a rs =>midtape [ ] a rs
      | midtape ls a rs => tape_move_right' ls a rs
      end.

  Definition tape_move_left' ls a rs :=
    match ls with
    | nil => leftof a rs
    | l::ls' => midtape ls' l (a ::rs)
    end.

  Definition tape_move_left :=
    fun (t : tape) =>
      match t with
      | niltape => niltape
      | leftof _ _ => t
      | rightof a ls => midtape ls a [ ]
      | midtape ls a rs => tape_move_left' ls a rs
      end.

  Definition tape_move (t : tape) (m : move) :=
    match m with
    | R => tape_move_right t
    | L => tape_move_left t
    | N => t
    end.

Rewriting Lemmas

  Lemma tapeToList_move (t : tape) (D : move) :
    tapeToList (tape_move t D) = tapeToList t.
  Proof.
    destruct t, D; cbn; auto.
    - revert s l0. induction l; intros; cbn in *; simpl_list; auto.
    - revert s l. induction l0; intros; cbn in *; simpl_list; auto.
  Qed.

  Lemma tapeToList_move_R (t : tape) :
    tapeToList (tape_move_right t) = tapeToList t.
  Proof. apply (tapeToList_move t R). Qed.

  Lemma tapeToList_move_L (t : tape) :
    tapeToList (tape_move_left t) = tapeToList t.
  Proof. apply (tapeToList_move t L). Qed.

  Lemma tape_move_right_left (t : tape) (s : sig) :
    current t = Some s ->
    tape_move_left (tape_move_right t) = t.
  Proof.
    intros H1. destruct t; cbn in *; inv H1; auto; destruct l; auto; destruct l0; auto.
  Qed.

  Lemma tape_move_left_right (t : tape) (s : sig) :
    current t = Some s ->
    tape_move_right (tape_move_left t) = t.
  Proof.
    intros H1. destruct t; cbn in *; inv H1; auto; destruct l; auto; destruct l0; auto.
  Qed.

Machine step

Writing on the tape

  Definition tape_write (t : tape) (s : option sig) :=
    match s with
    | None => t
    | Some s' => midtape (left t) s' (right t)
    end.

A single step of the machine

Definition doAct (t : tape) (mv : option sig * move) :=
tape_move (tape_write t (fst mv)) (snd mv).

One step on each tape

Definition doAct_multi (n : nat) (ts : tapes n) (actions : Vector.t (option sig * move) n) :=
Vector.map2 doAct ts actions.

Read characters on all tapes

Definition current_chars (n : nat) (tapes : tapes n) := Vector.map current tapes.

End Fix_Sigma.

Rewriting tactics

Tactic to destruct a vector of tapes of known size

Ltac destruct_tapes := unfold tapes in *; destruct_vector.

Simplification Database for tapes and vectors

Create HintDb tape.
Create HintDb vector.

We use rewrite_strat instead of autorewrite, because it is faster.

Tactic Notation "simpl_tape" :=
  repeat rewrite_strat (topdown (choice (hints tape) (hints vector))).
Tactic Notation "simpl_tape" "in" ident(H) :=
  repeat rewrite_strat (topdown (choice (hints tape) (hints vector))) in H.
Tactic Notation "simpl_tape" "in" "*" :=
  repeat multimatch goal with
         | [ H : _ |- _ ] => simpl_tape in H
         end;
  simpl_tape.

Tactic Notation "simpl_vector" :=
  repeat rewrite_strat (topdown (hints vector)).
Tactic Notation "simpl_vector" "in" ident(H) :=
  repeat rewrite_strat (topdown (hints vector)) in H.
Tactic Notation "simpl_vector" "in" "*" :=
  repeat multimatch goal with
         | [ H : _ |- _ ] => simpl_vector in H
         end;
  simpl_vector.

Hint Rewrite tapeToList_move : tape.
Hint Rewrite tapeToList_move_R : tape.
Hint Rewrite tapeToList_move_L : tape.
Hint Rewrite tape_move_right_left using eauto : tape.
Hint Rewrite tape_move_left_right using eauto : tape.

Arguments current_chars : simpl never.
Hint Unfold current_chars : tape.

Lemma nth_map' (A B : Type) (f : A -> B) (n : nat) (v : Vector.t A n) (k : Fin.t n) :
  (VectorDef.map f v)[@k] = f v[@k].
Proof. erewrite VectorSpec.nth_map; eauto. Qed.

Lemma nth_map2' (A B C : Type) (f : A -> B -> C) (n : nat) (v1 : Vector.t A n) (v2 : Vector.t B n) (k : Fin.t n) :
  (VectorDef.map2 f v1 v2)[@k] = f v1[@k] v2[@k].
Proof. erewrite VectorSpec.nth_map2; eauto. Qed.

Hint Rewrite @nth_map' : vector.
Hint Rewrite @nth_map2' : vector.
Hint Rewrite @nth_tabulate : vector.
Hint Rewrite VectorSpec.const_nth : vector.

Set Notation scopes for tapes, so that the alphabet of the tape is parsed as a type (e.g. X+Y is parsed as the sum type, not the addition of X and Y)

Arguments tapes (sig % type) (n % nat).

Nop Action

(∅, N)^n

Section Nop_Action.
  Variable n : nat.
  Variable sig : finType.

  Definition nop_action := Vector.const (@None sig , N ) n.

  Lemma doAct_nop tapes :
    doAct_multi tapes nop_action = tapes.
  Proof.
    unfold nop_action, doAct_multi.
    apply Vector.eq_nth_iff; intros ? i <-.
    erewrite Vector.nth_map2; eauto.
    rewrite Vector.const_nth.
    cbn. reflexivity.
  Qed.

End Nop_Action.

Make n and sig contextual implicit

Arguments nop_action {_ _}.

Mirror tapes

Section MirrorTape.
  Variable (n : nat) (sig : Type).

  Definition mirror_tape (t : tape sig) : tape sig :=
    match t with
    | niltape _ => niltape _
    | leftof r rs => rightof r rs
    | rightof l ls => leftof l ls
    | midtape ls m rs => midtape rs m ls
    end.

  Lemma mirror_tape_left (t : tape sig) :
    left (mirror_tape t) = right t.
  Proof. now destruct t. Qed.

  Lemma mirror_tape_right (t : tape sig) :
    right (mirror_tape t) = left t.
  Proof. now destruct t. Qed.

  Lemma mirror_tape_current (t : tape sig) :
    current (mirror_tape t) = current t.
  Proof. now destruct t. Qed.

  Lemma mirror_tape_involution (t : tape sig) :
    mirror_tape (mirror_tape t) = t.
  Proof. destruct t; cbn; congruence. Qed.

  Lemma mirror_tape_injective (t1 t2 : tape sig) :
    mirror_tape t1 = mirror_tape t2 ->
    t1 = t2.
  Proof. destruct t1, t2; intros H; cbn in *; congruence. Qed.

  Lemma mirror_tape_move_left (t : tape sig) :
    mirror_tape (tape_move_left t) = tape_move_right (mirror_tape t).
  Proof. destruct t; cbn; auto. destruct l; cbn; auto. Qed.

  Lemma mirror_tape_move_right (t : tape sig) :
    mirror_tape (tape_move_right t) = tape_move_left (mirror_tape t).
  Proof. destruct t; cbn; auto. destruct l0; cbn; auto. Qed.

  Lemma mirror_tape_inv_midtape t r1 r2 x :
    mirror_tape t = midtape r1 x r2 -> t = midtape r2 x r1.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_leftof t rs x :
    mirror_tape t = leftof rs x -> t = rightof rs x.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_rightof t ls x :
    mirror_tape t = rightof ls x -> t = leftof ls x.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_niltape t :
    mirror_tape t = niltape _ -> t = niltape _.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_midtape' t r1 r2 x :
    midtape r1 x r2 = mirror_tape t -> t = midtape r2 x r1.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_leftof' t rs x :
    leftof rs x = mirror_tape t -> t = rightof rs x.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_rightof' t ls x :
    rightof ls x = mirror_tape t -> t = leftof ls x.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Lemma mirror_tape_inv_niltape' t :
    niltape _ = mirror_tape t -> t = niltape _.
  Proof. intros. destruct t; cbn in *; congruence. Qed.

  Definition mirror_tapes (t : tapes sig n) : tapes sig n := Vector.map mirror_tape t.

  Lemma mirror_tapes_involution (t : tapes sig n) :
    mirror_tapes (mirror_tapes t) = t.
  Proof.
    unfold mirror_tapes. apply Vector.eq_nth_iff. intros ? ? ->.
    erewrite !Vector.nth_map; eauto. apply mirror_tape_involution.
  Qed.

  Lemma mirror_tapes_injective (t1 t2 : tapes sig n) :
    mirror_tapes t1 = mirror_tapes t2 ->
    t1 = t2.
  Proof.
    intros H. unfold mirror_tapes in *. apply Vector.eq_nth_iff. intros ? ? ->.
    eapply Vector.eq_nth_iff with (p1 := p2) in H; eauto.
    erewrite !Vector.nth_map in H; eauto. now apply mirror_tape_injective.
  Qed.

  Definition mirror_move (D : move) : move := match D with | N => N | L => R | R => L end.

  Lemma mirror_move_involution (D : move) : mirror_move (mirror_move D) = D.
  Proof. now destruct D. Qed.

  Lemma mirror_tapes_nth (tapes : tapes sig n) (k : Fin.t n) :
    (mirror_tapes tapes)[@k] = mirror_tape (tapes[@k]).
  Proof. intros. eapply VectorSpec.nth_map; eauto. Qed.

End MirrorTape.

Arguments mirror_tapes : simpl never.
Hint Unfold mirror_tapes : tape.

Hint Rewrite mirror_tape_left : tape.
Hint Rewrite mirror_tape_right : tape.
Hint Rewrite mirror_tape_current : tape.
Hint Rewrite mirror_tape_involution : tape.
Hint Rewrite mirror_tape_move_left : tape.
Hint Rewrite mirror_tape_move_right : tape.
Hint Rewrite mirror_tapes_involution : tape.
Hint Rewrite mirror_tapes_nth : tape.

Helping functions for tapes

Section Tape_Local.

Variable sig : Type.

The current symbol :: right symbols

  Definition tape_local (t : tape sig) : list sig :=
    match t with
    | niltape _ => []
    | leftof a l => []
    | rightof _ _ => []
    | midtape _ a l => a :: l
    end.

The current symbol :: left symbols

  Definition tape_local_l (t : tape sig) : list sig :=
    match t with
    | niltape _ => []
    | leftof a l => []
    | rightof _ _ => []
    | midtape r a l => a :: r
    end.

  Lemma tape_local_mirror (t : tape sig) :
    tape_local_l (mirror_tape t) = tape_local t.
  Proof. destruct t; cbn; auto. Qed.

  Lemma tape_local_mirror' (t : tape sig) :
    tape_local (mirror_tape t) = tape_local_l t.
  Proof. destruct t; cbn; auto. Qed.

  Lemma tape_local_current_cons (x : sig) (xs : list sig) (t : tape sig) :
    tape_local t = x :: xs -> current t = Some x.
  Proof. destruct t eqn:E; cbn; congruence. Qed.

  Lemma tape_local_l_current_cons (x : sig) (xs : list sig) (t : tape sig) :
    tape_local_l t = x :: xs -> current t = Some x.
  Proof. destruct t eqn:E; cbn; congruence. Qed.

  Lemma tape_local_right (x : sig) (xs : list sig) (t : tape sig) :
    tape_local t = x :: xs -> right t = xs.
  Proof. destruct t eqn:E; cbn; congruence. Qed.

  Lemma tape_local_l_left (x : sig) (xs : list sig) (t : tape sig) :
    tape_local_l t = x :: xs -> left t = xs.
  Proof. destruct t eqn:E; cbn; congruence. Qed.

  Lemma tape_local_cons_iff (t : tape sig) (x : sig) (xs : list sig) :
    tape_local t = x :: xs <-> current t = Some x /\ right t = xs.
  Proof.
    split; intros H.
    - destruct t; cbn in *; inv H. eauto.
    - destruct t; cbn in *; inv H; inv H0. eauto.
  Qed.

  Lemma tape_local_l_cons_iff (t : tape sig) (x : sig) (xs : list sig) :
    tape_local_l t = x :: xs <-> current t = Some x /\ left t = xs.
  Proof.
    split; intros H.
    - destruct t; cbn in *; inv H. eauto.
    - destruct t; cbn in *; inv H; inv H0. eauto.
  Qed.

  Lemma tape_local_nil (t : tape sig) :
    tape_local t = [] <-> current t = None.
  Proof.
    destruct t; cbn; intuition; auto; congruence.
  Qed.

  Lemma tape_local_move_right (t : tape sig) (x : sig) (xs : list sig) :
    tape_local t = x :: xs -> tape_local (tape_move_right t) = xs.
  Proof.
    intro H. destruct t eqn:E; cbn in *; try congruence.
    inv H. destruct xs; cbn; auto.
  Qed.

  Lemma tape_local_l_move_left (t : tape sig) (x : sig) (xs : list sig) :
    tape_local_l t = x :: xs -> tape_local_l (tape_move_left t) = xs.
  Proof.
    intro H. destruct t eqn:E; cbn in *; try congruence.
    inv H. destruct xs; cbn; auto.
  Qed.

  Lemma tape_left_move_right (t : tape sig) (x : sig) :
    current t = Some x -> left (tape_move_right t) = x :: left t.
  Proof. intros H. destruct t; cbn in *; try congruence. inv H. destruct l0; cbn; reflexivity. Qed.

  Lemma tape_right_move_left (t : tape sig) (x : sig) :
    current t = Some x -> right (tape_move_left t) = x :: right t.
  Proof. intros H. destruct t; cbn in *; try congruence. inv H. destruct l; cbn; reflexivity. Qed.

  Lemma midtape_tape_local_cons t r2 x :
    tape_local t = x :: r2 <-> t = midtape (left t) x r2.
  Proof.
    split.
    - intros H1. destruct t; cbn in *; congruence.
    - intros H1. destruct t; cbn in *; inv H1. auto.
  Qed.

  Lemma midtape_tape_local_cons_left t r1 r2 x :
    left t = r1 /\ tape_local t = x :: r2 <-> t = midtape r1 x r2.
  Proof. rewrite midtape_tape_local_cons. intuition subst; cbn; auto. Qed.

  Lemma midtape_tape_local_l_cons t r1 x :
    tape_local_l t = x :: r1 <-> t = midtape r1 x (right t).
  Proof.
    split.
    - intros H1. destruct t; cbn in *; congruence.
    - intros H1. destruct t; cbn in *; inv H1. auto.
  Qed.

  Lemma midtape_tape_local_l_cons_right t r1 r2 x :
    tape_local_l t = x :: r1 /\ right t = r2 <-> t = midtape r1 x r2.
  Proof. rewrite midtape_tape_local_l_cons. intuition subst; cbn; auto. Qed.

End Tape_Local.

Hint Rewrite tape_local_mirror : tape.
Hint Rewrite tape_local_mirror' : tape.
Hint Rewrite tape_local_current_cons using auto : tape.
Hint Rewrite tape_local_l_current_cons using auto : tape.
Hint Rewrite tape_local_right using auto : tape.
Hint Rewrite tape_local_l_left using auto : tape.
Hint Rewrite tape_left_move_right using auto : tape.
Hint Rewrite tape_right_move_left using auto : tape.

Mapping tapes

Section MapTape.
  Variable sig tau : Type.
  Variable g : tau -> sig.

  Definition mapTape : tape tau -> tape sig.
  Proof.
    destruct 1 eqn:E1.
    - apply niltape.
    - apply leftof. apply (g t). apply (List.map g l).
    - apply rightof. apply (g t). apply (List.map g l).
    - apply midtape. apply (List.map g l). apply (g t). apply (List.map g l0).
  Defined.

  Definition mapTapes {n : nat} : Vector.t (tape tau) n -> Vector.t (tape sig) n := Vector.map mapTape.

  Lemma mapTape_current t :
    current (mapTape t) = map_opt g (current t).
  Proof. destruct t; cbn; reflexivity. Qed.

  Lemma mapTape_left t :
    left (mapTape t) = List.map g (left t).
  Proof. destruct t; cbn; reflexivity. Qed.

  Lemma mapTape_right t :
    right (mapTape t) = List.map g (right t).
  Proof. destruct t; cbn; reflexivity. Qed.

  Lemma mapTape_move_left t :
    tape_move_left (mapTape t) = mapTape (tape_move_left t).
  Proof. destruct t; cbn; auto. destruct l; cbn; auto. Qed.

  Lemma mapTape_move_right t :
    tape_move_right (mapTape t) = mapTape (tape_move_right t).
  Proof. destruct t; cbn; auto. destruct l0; cbn; auto. Qed.

  Lemma mapTape_inv_niltap t :
    mapTape t = niltape _ ->
    t = niltape _.
  Proof. intros. destruct t; inv H. repeat econstructor. Qed.

  Lemma mapTape_inv_rightof t l ls :
    mapTape t = rightof l ls ->
    exists l' ls', t = rightof l' ls' /\
              l = g l' /\
              ls = map g ls'.
  Proof. intros. destruct t; inv H. repeat econstructor. Qed.

  Lemma mapTape_inv_leftof t r rs :
    mapTape t = leftof r rs ->
    exists r' rs', t = leftof r' rs' /\
              r = g r' /\
              rs = map g rs'.
  Proof. intros. destruct t; inv H. repeat econstructor. Qed.

  Lemma mapTape_inv_midtape t ls m rs :
    mapTape t = midtape ls m rs ->
    exists ls' m' rs', t = midtape ls' m' rs' /\
                  ls = map g ls' /\
                  m = g m' /\
                  rs = map g rs'.
  Proof. intros. destruct t; inv H. repeat econstructor. Qed.

End MapTape.

Rewriting Hints

Hint Rewrite mapTape_current : tape.
Hint Rewrite mapTape_left : tape.
Hint Rewrite mapTape_right : tape.
Hint Rewrite mapTape_move_left : tape.
Hint Rewrite mapTape_move_right : tape.
Hint Unfold mapTapes : tape.

Lemma mapTape_mapTape (sig tau gamma : Type) (f : sig -> tau) (g : tau -> gamma) (t : tape sig) :
  mapTape g (mapTape f t) = mapTape (fun x => g (f x)) t.
Proof. destruct t; cbn; auto; try simpl_tape; now rewrite !map_map. Qed.

Lemma mapTape_ext (sig tau : Type) (f g : sig -> tau) (t : tape sig) :
  (forall a, f a = g a ) -> mapTape f t = mapTape g t.
Proof. intros H. destruct t; cbn; auto; simpl_tape; rewrite H; f_equal; eapply map_ext; eauto. Qed.

Lemma mapTape_id (sig : Type) (t : tape sig) :
  mapTape (fun x => x) t = t.
Proof. destruct t; cbn; auto; f_equal; apply map_id. Qed.
Hint Rewrite mapTape_mapTape : tape.
Hint Rewrite mapTape_id : tape.

Lemma mapTape_local (sig tau : Type) (f : sig -> tau) t :
  tape_local (mapTape f t) = List.map f (tape_local t).
Proof. destruct t; cbn; reflexivity. Qed.
Hint Rewrite mapTape_local : tape.

Lemmas about tape_move_left' and tape_move_right'

Section MatchTapes.
Variable sig : Type.

Left movement

  Lemma tape_left_move_left' ls (x : sig) rs :
    left (tape_move_left' ls x rs) = tl ls.
  Proof. now destruct ls; cbn. Qed.

  Lemma tape_left_move_left (t : tape sig) :
    left (tape_move_left t) = tl (left t).
  Proof. destruct t; cbn; auto. apply tape_left_move_left'. Qed.

  Lemma tape_left_move_right' ls (x : sig) rs :
    left (tape_move_right' ls x rs) = x :: ls.
  Proof. destruct rs; cbn; reflexivity. Qed.

  Lemma tape_right_move_left' ls (x : sig) rs :
    right (tape_move_left' ls x rs) = x :: rs.
  Proof. destruct ls; cbn; reflexivity. Qed.

  Lemma tape_local_l_move_left' rs (x : sig) ls :
    tape_local_l (tape_move_left' rs x ls) = rs.
  Proof. destruct rs; cbn; reflexivity. Qed.

  Lemma mirror_tape_move_left' rs (x : sig) ls :
    mirror_tape (tape_move_left' rs x ls) = tape_move_right' ls x rs.
  Proof. now destruct rs; cbn. Qed.

Right movement

  Lemma tape_right_move_right' ls (x : sig) rs :
    right (tape_move_right' ls x rs) = tl rs.
  Proof. now destruct rs; cbn. Qed.

  Lemma tape_right_move_right (t : tape sig) :
    right (tape_move_right t) = tl (right t).
  Proof. destruct t; cbn; auto. apply tape_right_move_right'. Qed.

  Lemma tape_local_move_right' rs (x : sig) ls :
    tape_local (tape_move_right' rs x ls) = ls.
  Proof. destruct ls; cbn; reflexivity. Qed.

  Lemma mirror_tape_move_right' rs (x : sig) ls :
    mirror_tape (tape_move_right' rs x ls) = tape_move_left' ls x rs.
  Proof. now destruct ls; cbn. Qed.

End MatchTapes.

Hint Rewrite tape_left_move_left' : tape.
Hint Rewrite tape_left_move_left : tape.
Hint Rewrite tape_left_move_right' : tape.
Hint Rewrite tape_right_move_left' : tape.
Hint Rewrite tape_local_l_move_left' : tape.
Hint Rewrite mirror_tape_move_left' : tape.

Hint Rewrite tape_right_move_right' : tape.
Hint Rewrite tape_right_move_right : tape.
Hint Rewrite tape_right_move_left' : tape.
Hint Rewrite tape_right_move_right' : tape.
Hint Rewrite tape_local_move_right' : tape.
Hint Rewrite mirror_tape_move_right' : tape.

Definition of Multi-Tape Turing Machines

Section Semantics.

  Variable sig : finType.

  Record mTM (n:nat) : Type :=
    {
      states : finType;
      trans : states * (Vector.t (option sig) n ) -> states * (Vector.t ((option sig ) * move) n );
      start: states;
      halt : states -> bool
    }.

Labelled Multi-Tape Turing Machines

Definition pTM (F: Type) (n:nat) := { M : mTM n & states M -> F }.

Configurations of TMs

  Record mconfig (states:finType) (n:nat): Type :=
    mk_mconfig
      {
        cstate : states;
        ctapes : tapes sig n
      }.

Machine execution

  Definition step {n} (M:mTM n) : mconfig (states M) n -> mconfig (states M) n :=
    fun c =>
      let (news,actions) := trans (cstate c , current_chars (ctapes c)) in
      mk_mconfig news (doAct_multi (ctapes c) actions).

  Definition haltConf {n} (M : mTM n) : mconfig (states M) n -> bool := fun c => halt (cstate c).

Run the machine i steps until it halts

Definition loopM n (M : mTM n) := loop (@step _ M) (@haltConf _ M).

Initial configuration

Definition initc n (M : mTM n) tapes :=
mk_mconfig (n := n) (@start n M) tapes.

Realisation

Parametrised relations

Definition pRel (sig : Type) (F: Type) (n : nat) := Rel (tapes sig n) (F * tapes sig n).

A (labelled) machine M realises a (labelled) relation R, if: for every tape vectors t, if M with t terminates in a configuration c, then R (t), (projT2 M (cstate c), ctapes c). That means that the pair of the input tape vectors, the labelof the state in that the machine terminated, and the output tape, must be in the relation R.

  Definition Realise n F (pM : pTM n F) (R : pRel sig n F) :=
    forall t k outc, loopM (initc (projT1 pM) t) k = Some outc -> R t (projT2 pM (cstate outc), ctapes outc ).

  Notation "M '⊨' R" := (Realise M R) (no associativity, at level 30, format "M '⊨' R").

Realisation is monotone

  Lemma Realise_monotone n (F : finType) (pM : pTM F n) R R' :
    pM ⊨ R' -> R' <<=2 R -> pM ⊨ R.
  Proof. firstorder. Qed.

Termination/Runtime

A machine is said to "terminate in" a relation T : Rel (tapes sig n) nat, if for every pair of input tape vectors t and step numbers k such that T t k, there exists an output configuration cout that M reaches from t in k steps.

  Definition tRel sig n := Rel (tapes sig n) nat.

  Definition TerminatesIn {n : nat} (M : mTM n) (T : tRel sig n) :=
    forall tin k, T tin k -> exists conf, loopM (initc M tin) k = Some conf.

  Arguments TerminatesIn { _ } _.
  Notation "M ↓ T" := (TerminatesIn M T) (no associativity, at level 60, format "M '↓' T").

Termination is anti-monotone

  Lemma TerminatesIn_monotone {n : nat} (M : mTM n) (T T' : tRel sig n) :
    M ↓ T' -> (T <<=2 T') -> M ↓ T.
  Proof. intros H1 H2. firstorder. Qed.

  Lemma TerminatesIn_extend {n : nat} (M : mTM n) (T : tRel sig n) :
    M ↓ T ->
    M ↓ (fun tin k => exists k', k' <= k /\ T tin k').
  Proof.
    intros HTerm. hnf in *. intros tin k. intros (k'&Hk'&HT).
    specialize HTerm with (1 := HT) as (oconf&HLoop).
    exists oconf. eapply loop_monotone; eauto.
  Qed.

Realisation plus termination in constant time

  Definition RealiseIn n (F : finType) (pM : pTM F n) (R : pRel sig F n) (k : nat) :=
    forall input, exists outc, loopM (initc (projT1 pM) input) k = Some outc /\ R input ((projT2 pM (cstate outc)), ctapes outc ).
  Notation "M '⊨c(' k ')' R" := (RealiseIn M R k) (no associativity, at level 45, format "M '⊨c(' k ')' R").

  Lemma RealiseIn_monotone n (F : finType) (pM : pTM F n) (R R' : pRel sig F n) k k' :
    pM ⊨c (k') R' -> k' <= k -> R' <<=2 R -> pM ⊨c (k ) R.
  Proof.
    unfold RealiseIn. intros H1 H2 H3 input.
    specialize (H1 input) as (outc & H1). exists outc.
    split.
    - unfold loopM. eapply loop_monotone; eauto. intuition.
    - intuition.
  Qed.

  Lemma RealiseIn_monotone' n (F : finType) (pM : pTM F n) (R : pRel sig F n) k k' :
    pM ⊨c (k') R -> k' <= k -> pM ⊨c (k ) R.
  Proof.
    intros H1 H2. eapply RealiseIn_monotone. eapply H1. assumption. firstorder.
  Qed.

  Lemma RealiseIn_split n (F : finType) (pM : pTM F n) R1 R2 (k : nat) :
    pM ⊨c (k ) R1 /\ pM ⊨c (k ) R2 <-> pM ⊨c (k ) R1 ∩ R2.
  Proof.
    split; swap 1 2; [ intros H | intros (H1&H2)]; repeat intros ?. hnf; firstorder eauto.
    specialize (H1 input) as (outc &H1&H1'). specialize (H2 input) as (outc2&H2&H2').
    pose proof loop_injective H1 H2 as <-. exists outc. split; hnf; eauto.
  Qed.

  Lemma Realise_total n (F : finType) (pM : { M : mTM n & states M -> F }) R k :
    pM ⊨ R /\ projT1 pM ↓ (fun _ i => k <= i ) <-> pM ⊨c (k ) R.
  Proof.
    split.
    - intros (HR & Ht) t. edestruct (Ht t k). cbn; omega. eauto.
    - intros H.
      split.
      + intros t i cout Hc.
        destruct (H t) as (? & ? & ?).
        cutrewrite (cout = x).
        eassumption.
        unfold loopM in *.
        eapply loop_injective; eauto.
      + intros t i Hi.
        edestruct (H t) as (? & ? & ?).
        exists x. eapply loop_monotone; eauto.
  Qed.

  Lemma RealiseIn_Realise n (F : finType) (pM : pTM F n) R k :
    pM ⊨c (k ) R -> pM ⊨ R.
  Proof. now intros (?&?) % Realise_total. Qed.

  Lemma RealiseIn_TerminatesIn n (F : finType) (pM : { M : mTM n & states M -> F }) R k :
    pM ⊨c (k ) R -> projT1 pM ↓ (fun tin l => k <= l ).
  Proof.
    intros HRel. hnf. intros tin l HSteps. hnf in HRel. specialize (HRel tin) as (outc&HLoop&Rloop).
    exists outc. eapply loop_monotone; eauto.
  Qed.

  Lemma Realise_strengthen n (F : finType) (pM : pTM F n) R1 R2 :
    Realise pM R2 -> Realise pM R1 -> Realise pM (R1 ∩ R2).
  Proof.
    intros HwR HR t. firstorder.
  Qed.

Canonical relations

  Section Canonical_Correctness.
    Variable (n : nat).
    Variable (F : finType).
    Variable (pM : pTM F n).

    Definition Canonical_Rel : pRel sig F n :=
      fun t1 '(y, t2) =>
        exists outc k, loopM (M := projT1 pM) (initc (projT1 pM) t1) k = Some outc /\
                  ctapes outc = t2 /\ projT2 pM (cstate outc) = y.

    Fact Canonical_Realise :
      pM ⊨ Canonical_Rel.
    Proof. hnf. firstorder eauto. Qed.

    Lemma R_canonical_functional : functional Canonical_Rel.
    Proof.
      hnf. intros x (y1&z1) (y2&z2) (c1&k1&H1&<-&H1') (c2&k2&H2&<-&H2').
      pose proof loop_injective H1 H2 as ->. congruence.
    Qed.

  End Canonical_Correctness.

  Section Canonical_Termination.
    Variable (n : nat).
    Variable (M : mTM n).

    Definition Canonical_T : tRel sig n :=
      fun t k => exists outc, loopM (M := M) (initc M t) k = Some outc.

    Lemma Canonical_TerminatesIn :
      M ↓ Canonical_T.
    Proof. firstorder. Qed.

  End Canonical_Termination.

End Semantics.

Notation for parametrised Turing machines

Notation "'(' M ';' labelling ')'" := (existT (fun x => states x -> _) M labelling).

Notations for semantic of concrete Turing machines

Notation "M '⊨' R" := (Realise M R) (no associativity, at level 60, format "M '⊨' R").
Notation "M '⊨c(' k ')' R" := (RealiseIn M R k) (no associativity, at level 45, format "M '⊨c(' k ')' R").
Notation "M '↓' t" := (TerminatesIn M t) (no associativity, at level 60, format "M '↓' t").

inhabitedC instances for states and labels

Instance inhabited_move : inhabitedC move := ltac:(repeat constructor).

Instance inhabited_TM_Q (n : nat) (sig : finType) (M : mTM sig n) : inhabitedC (states M).
Proof. constructor. apply start. Qed.

Lemma inhabited_pTM_lab (n : nat) (sig : finType) (F : Type) (pM : pTM sig F n) : inhabitedC F.
Proof. constructor. apply (projT2 pM). apply default. Qed.

Hint Extern 4 => lazymatch goal with
                | [ pM : pTM ?sig ?F ?n |- inhabitedC ?F ] => apply (inhabited_pTM_lab pM)
                end : typeclass_instances.

Section Test_def.
  Variable (n : nat) (sig : finType) (F : Type).
  Variable (pM : pTM sig F n).
  Check default : states (projT1 pM).
  Check default : F.
End Test_def.

Auxiliary function to actually execute a machine

Definition execTM (sig : finType) (n : nat) (M : mTM sig n) (tapes : tapes sig n) (k : nat) :=
option_map (@ctapes _ _ _) (loopM (initc M tapes) k).

Definition execTM_p (sig : finType) (n : nat) (F : finType) (pM : { M : mTM sig n & states M -> F }) (tapes : tapes sig n) (k : nat) :=
option_map (fun x => (ctapes x , projT2 pM (cstate x))) (loopM (initc (projT1 pM) tapes) k ).

Automation of the generation of relations

Smpl Create TM_Correct.

Ltac TM_Correct_step := smpl TM_Correct.
Ltac TM_Correct := repeat TM_Correct_step.