Case Study 3: Multi-Tape Turing Machines

Definition of TMs

Copied from https://github.com/uds-psl/CoqTM/blob/b82fc64550949e26df2d3d5a8c39be46a128f116/theories/TM/TM.v Copyright (c) 2017-2018 Maximilian Wuttke under MIT License
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.

Require Export TM.Prelim.
Require Import Shared.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.
  Qed.

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

(* Apply a function to each symbol on the tape *)
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.

  (* Correctness of 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.

  (*
  Lemma mapTapes_nth {n : nat} (ts : tapes tau n) (k : Fin.t n) :
    (mapTapes ts)@k = mapTape (ts@k).
  Proof. unfold mapTapes. eapply VectorSpec.nth_map; eauto. 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 Rewrite mapTapes_nth       : 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.

  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_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_right' ls (x : sig) rs :
    left (tape_move_left' ls x rs) = tl ls.
  Proof. now destruct ls; cbn. Qed.

  Lemma tape_left_move_left' ls (x : sig) rs :
    right (tape_move_right' ls x rs) = tl rs.
  Proof. now destruct rs; cbn. 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 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.

  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_right_move_left' : tape.
Hint Rewrite tape_left_move_right' : tape.
Hint Rewrite tape_right_move_right' : tape.
Hint Rewrite tape_left_move_left' : tape.
Hint Rewrite tape_local_move_right' : tape.
Hint Rewrite tape_local_l_move_left' : tape.
Hint Rewrite mirror_tape_move_left' : tape.
Hint Rewrite mirror_tape_move_right' : tape.

(* **** Configurations of TMs *)

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

(* *** Definition of Multi-Tape Turing Machines *)
Section Semantics.

  Variable sig : finType.

  Record mTM (n:nat) : Type :=
    {
      states : finType; (* states of the TM *)
      trans : states * (Vector.t (option sig) n) -> states * (Vector.t ((option sig) * move) n); (* the transition function *)
      start: states; (* the start state *)
      halt : states -> bool (* decidable subset of halting states *)
    }.

Labelled Multi-Tape Turing Machines
  Definition pTM (F: Type) (n:nat) := { M : mTM n & states M -> F }.

  (* **** Machine execution *)

  Definition step {n} (M:mTM n) : mconfig sig (states M) n -> mconfig sig (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 sig (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).

End Semantics.