From Undecidability Require Import ProgrammingTools.
From Undecidability Require Import ArithPrelim.

From Undecidability Require Import TM.Compound.Shift.

From Undecidability Require Import EncodeTapes.
Require Import FunInd.

Local Set Printing Coercions.

Local Arguments Vector.to_list {A n} (!v).

Local Arguments plus : simpl never.
Local Arguments mult : simpl never.



Lemma tape_move_niltape (sig : Type) (m : move) :
  tape_move (niltape sig) m = niltape sig.
Proof. now destruct m. Qed.

Lemma tape_write_left (sig : Type) (t : tape sig) s :
  left (tape_write t s) = left t.
Proof. destruct s; auto. Qed.

Lemma tape_write_right (sig : Type) (t : tape sig) s :
  right (tape_write t s) = right t.
Proof. destruct s; auto. Qed.

Lemma tape_write_current_Some (sig : Type) (t : tape sig) s :
  current (tape_write t (Some s)) = Some s.
Proof. auto. Qed.

Lemma tape_write_current_None (sig : Type) (t : tape sig) :
  current (tape_write t None) = current t.
Proof. auto. Qed.

Lemma tape_write_current (sig : Type) (t : tape sig) s :
  current (tape_write t s) = fold_opt (@Some _) (current t) s.
Proof. destruct s; auto. Qed.

Hint Rewrite tape_move_niltape tape_write_left tape_write_right tape_write_current_Some tape_write_current_None tape_write_current : tape.

Lemma removelast_cons (X : Type) (xs : list X) (x : X) :
  xs <> nil ->
  removelast (x :: xs) = x :: removelast xs.
Proof.
  destruct xs as [ | x' xs']; cbn.
  - congruence.
  - intros _. auto.
Qed.

Lemma vector_to_list_inj (X : Type) (n : nat) (xs ys : Vector.t X n) :
  vector_to_list xs = vector_to_list ys -> xs = ys.
Proof.
  revert ys. induction xs as [ | x n xs IH]; intros; cbn in *.
  - destruct_vector. reflexivity.
  - destruct_vector. cbn in *. inv H. f_equal. auto.
Qed.

Definition fin_to_nat (n : nat) (i : Fin.t n) : nat := proj1_sig (Fin.to_nat i).
Module FinCoercion.
  Coercion fin_to_nat : Fin.t >-> nat.
  Export Set Printing Coercions.
End FinCoercion.

Import FinCoercion.

Section Fin.

  Lemma fin_to_nat_lt (n : nat) (i : Fin.t n) : fin_to_nat i < n.
  Proof. unfold fin_to_nat. destruct (Fin.to_nat i). cbn. auto. Qed.

  Lemma fin_to_nat_O (n : nat) :
    fin_to_nat (@Fin.F1 n) = 0.
  Proof. reflexivity. Qed.

  Lemma fin_to_nat_S (n : nat) (i : Fin.t n) :
    fin_to_nat (Fin.FS i) = S (fin_to_nat i).
  Proof.
    unfold fin_to_nat. destruct i as [ | n i].
    - cbn. reflexivity.
    - cbn in *. destruct (Fin.to_nat i) as [k ?]. cbn in *. reflexivity.
  Qed.

  Lemma fin_is_0 (n : nat) (i : Fin.t (S n)) :
    fin_to_nat i = 0 -> i = Fin0.
  Proof.
    intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; auto.
    rewrite fin_to_nat_S in H. omega.
  Qed.

  Lemma fin_is_1 (n : nat) (i : Fin.t (S (S n))) :
    fin_to_nat i = 1 -> i = Fin1.
  Proof.
    intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; auto.
    rewrite fin_to_nat_S in H. inv H. now apply fin_is_0 in H1 as ->.
  Qed.

  Lemma fin_is_2 (n : nat) (i : Fin.t (S (S (S n)))) :
    fin_to_nat i = 1 -> i = Fin1.
  Proof.
    intros H. pose proof fin_destruct_S i as [ (i'&->) | ->]; cbn in *; auto.
    rewrite fin_to_nat_S in H. inv H. now apply fin_is_0 in H1 as ->.
  Qed.

  Fixpoint finMax (n : nat) {struct n} : n <> 0 -> Fin.t n.
  Proof.
    destruct n as [ | n'].
    - abstract congruence.
    - decide (n' = 0) as [ H | H].       + intros _. apply Fin.F1.
      + intros _. apply Fin.FS. apply (finMax n'). auto.
  Defined.

  Definition finMax' (n : nat) : Fin.t (S n).
  Proof.
    apply finMax. apply Nat.neq_succ_0.
  Defined.

  Lemma finMax_ext (n : nat) (H1 H2 : n <> 0) : finMax H1 = finMax H2.
  Proof.
    induction n as [ | n' IH].
    - congruence.
    - cbn. decide (n' = 0) as [H | H]; f_equal.
  Qed.

  Lemma finMax_val (n : nat) (H : n <> 0) : fin_to_nat (finMax H) = n - 1.
  Proof.
    unfold fin_to_nat. induction n as [ | n' IH ].
    - congruence.
    - cbn. decide (n' = 0) as [ -> | H']; cbn.
      + reflexivity.
      + replace (n' - 0) with n' by omega.
        specialize IH with (H := H').
        destruct (Fin.to_nat (finMax H')) as [k ?]; cbn in *. omega.
  Qed.

  Definition finMin (n : nat) : n <> 0 -> Fin.t n.
  Proof.
    refine (match n as n' return n' <> 0 -> Fin.t n' with
            | 0 => fun H => False_rec _ _
            | S n' => fun _ => Fin.F1
            end); auto.
  Defined.

  Lemma finMin_O (n : nat) (H : S n <> 0) : finMin H = Fin.F1.
  Proof. cbn. reflexivity. Qed.

  Lemma finMin_ext (n : nat) (H1 H2 : n <> 0) : finMin H1 = finMin H2.
  Proof.
    destruct n.
    - congruence.
    - auto.
  Qed.

  Lemma finMin_val (n : nat) (H : n <> 0) : fin_to_nat (finMin H) = 0.
  Proof.
    unfold fin_to_nat. destruct n as [ | n'].
    - congruence.
    - cbn. reflexivity.
  Qed.

  Lemma finSucc_help (i : Fin.t 1) : i = Fin0.
  Proof. now destruct_fin i. Qed.

  Lemma finSucc_help' (n : nat) (i1 i2 : Fin.t n) :
    Fin.FS i1 <> Fin.FS i2 -> i1 <> i2.
  Proof. now intros H1 ->. Qed.

  Fixpoint finSucc (n : nat) (i : Fin.t n) {struct n} : forall (H : n <> 0), i <> finMax H -> Fin.t n.
  Proof.
    destruct n as [ | n'].
    - intros. abstract congruence.
    - cbn. decide (n' = 0) as [ HDec | HDec]; cbn.
      + intros _ Hi. exfalso. apply Hi. subst. apply finSucc_help.
      + intros _.
        revert n' i HDec. refine (@Fin.caseS (fun n' i => forall (HDec : n' <> 0), i <> Fin.FS (finMax HDec) -> Fin.t (S n')) _ _).
        * intros. apply Fin.FS. apply finMin. apply HDec.
        * intros. apply Fin.FS. eapply finSucc. eapply finSucc_help'. apply H.
  Defined.

  Definition finSucc' (n : nat) (i : Fin.t (S n)) (H : i <> finMax' n) : Fin.t (S n).
  Proof. unshelve eapply finSucc with (i := i). apply Nat.neq_succ_0. apply H. Defined.

  Fixpoint finSucc_opt (n : nat) (i : Fin.t n) {struct i} : option (Fin.t n).
  Proof.
    destruct i.
    - destruct n.
      + apply None.
      + apply Some. apply Fin.FS. apply Fin.F1.
    - destruct n.
      + destruct_fin i.
      + destruct (finSucc_opt _ i) as [ rec | ].
        * apply Some. apply Fin.FS. apply rec.
        * apply None.
  Defined.

  Lemma finSucc_opt_Some (n : nat) (i : Fin.t n) :
    S (fin_to_nat i) < n ->
    exists i', finSucc_opt i = Some i'.
  Proof.
    induction i; intros; cbn in *.
    - destruct n. omega. eauto.
    - destruct n; cbn. omega.
      rewrite !fin_to_nat_S in *.
      spec_assert IHi as (i'&IH) by omega. rewrite IH. eauto.
  Qed.

  Lemma finSucc_opt_Some' (n : nat) (i i' : Fin.t n) :
    finSucc_opt i = Some i' ->
    fin_to_nat i' = S (fin_to_nat i).
  Proof.
    revert i'. induction i; cbn; intros.
    - destruct n; inv H. cbn. reflexivity.
    - destruct n; cbn in *. destruct_fin i.
      destruct (finSucc_opt i) as [ i'' | ] eqn:E; inv H.
      rewrite fin_to_nat_S. rewrite IHi; auto.
      now rewrite fin_to_nat_S.
  Qed.

  Lemma finSucc_opt_None (n : nat) (i : Fin.t n) :
    S (fin_to_nat i) = n ->
    finSucc_opt i = None.
  Proof.
    induction i; intros; cbn in *.
    - inv H. reflexivity.
    - rewrite fin_to_nat_S in *. inv H. spec_assert IHi by assumption.
      destruct n; cbn. omega. rewrite IHi. reflexivity.
  Qed.

  Lemma finSucc_opt_None' (n : nat) (i : Fin.t n) :
    finSucc_opt i = None ->
    S (fin_to_nat i) = n.
  Proof.
    induction i; cbn; intros.
    - destruct n; now inv H.
    - destruct n. destruct_fin i.
      destruct (finSucc_opt i) as [ i' | ]; inv H.
      now rewrite fin_to_nat_S, IHi.
  Qed.

  Definition finMin_opt (n : nat) : option (Fin.t n).
  Proof.
    destruct n.
    - apply None.
    - apply Some. apply Fin.F1.
  Defined.

  Lemma finMin_opt_None (n : nat) :
    finMin_opt n = None -> n = 0.
  Proof. destruct n; cbn; congruence. Qed.

  Lemma finMin_opt_Some (n : nat) i :
    finMin_opt n = Some i -> exists n', n = S n'.
  Proof. destruct n; cbn; intros H; inv H; eauto. Qed.

  Lemma finMin_opt_Some_val (n : nat) i :
    finMin_opt n = Some i -> fin_to_nat i = 0.
  Proof. destruct n; cbn; intros H; inv H; auto. Qed.


  Lemma finSucc_correct (n : nat) (i : Fin.t n) (H1 : n <> 0) (H2 : i <> finMax H1) :
    fin_to_nat (finSucc H2) = S (fin_to_nat i).
  Proof.
     revert i H1 H2. induction n as [ | n' IH]; intros; cbn in *.
    - congruence.
    - decide (n' = 0) as [-> | HDec]; cbn.
      + exfalso. apply H2. apply finSucc_help.
      + pose proof fin_destruct_S i as [ (i'&->) | -> ]; cbn -[Fin.to_nat]; swap 1 2.
        * change (S (proj1_sig (Fin.to_nat Fin0))) with 1.
          rewrite fin_to_nat_S. f_equal. rewrite finMin_val. reflexivity.
        * rewrite !fin_to_nat_S. f_equal. now rewrite IH.
  Qed.


End Fin.

Fixpoint map_vect_list (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X) {struct ls} : list X :=
  match ls with
  | nil => nil
  | x :: ls' =>
    match vs with
    | [||] => ls
    | y ::: vs' =>
      f x y :: map_vect_list f vs' ls'
    end
  end.

Lemma map_vect_list_length (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X) :
  length (map_vect_list f vs ls) = length ls.
Proof.
  revert n vs. induction ls as [ | x ls IH]; cbn; intros.
  - reflexivity.
  - destruct vs as [ | y n vs]; cbn; f_equal; auto.
Qed.

Lemma map_vect_list_app (X Y : Type) (f : X -> Y -> X) (n : nat) (vs : Vector.t Y n) (ls : list X)
      (x : X) (i : Fin.t n) :
  fin_to_nat i = length ls ->
  map_vect_list f vs (ls ++ [x]) =
  map_vect_list f vs ls ++ [f x vs[@i]].
Proof.
  revert n vs i. induction ls as [ | x' ls IH]; cbn; intros.
  - destruct vs. destruct_fin i.
    enough (i = Fin.F1) as -> by auto.
    pose proof fin_destruct_S i as [ (i'&->) | ]; cbn in *; auto.
    rewrite fin_to_nat_S in *. omega.
  - destruct vs as [ | v n vs]; cbn in *.
    + destruct_fin i.
    + f_equal.
      pose proof fin_destruct_S i as [ (i'&->) | -> ]; cbn in *.
      * rewrite fin_to_nat_S in *. apply IH. omega.
      * omega.
Qed.

Lemma map_vect_list_eq (X Y : Type) (n1 : nat) (f : X -> Y -> X) (vs : Vector.t Y n1) (xs : Vector.t X n1) :
  map_vect_list f vs (vector_to_list xs) = vector_to_list (Vector.map2 f xs vs).
Proof.
  revert xs. induction vs as [ | v n1 vs IH]; intros; cbn in *.
  - destruct_vector. cbn. reflexivity.
  - pose proof destruct_vector_cons xs as (x'&xs'&->). cbn.
    f_equal. auto.
Qed.

Lemma destruct_tapes1 (sig : Type) (t : tapes sig 1) :
  exists t', t = [| t' |].
Proof. destruct_tapes. eauto. Qed.

Section BookKeepingForRead.

  Variable sig : Type.

  Fixpoint knowsFirstSymbols {n' : nat} (readSymbols : Vector.t (option sig) n') (tps : list (tape sig)) {struct readSymbols} : Prop :=
    match readSymbols, tps with
    | Vector.nil _, nil => True /\ True /\ True
    | Vector.nil _, _::_ => True /\ True
    | x ::: readSymbols, nil => True
    | x ::: readSymbols', tp :: tps' =>
      current tp = x /\ knowsFirstSymbols readSymbols' tps'
    end.

  Lemma knowsFirstSymbols_nil {n : nat} (readSymbols : Vector.t (option sig) n) :
    knowsFirstSymbols readSymbols nil.
  Proof.
    destruct n.
    - destruct_vector. cbn. tauto.
    - destruct_vector. cbn. tauto.
  Qed.

  Definition insertKnownSymbol {n : nat} (readSymbols : Vector.t (option sig) n) (i : Fin.t n) (s : option sig) : Vector.t (option sig) n :=
    Vector.replace readSymbols i s.

  Fixpoint insertKnownSymbols {n : nat} (readSymbols : Vector.t (option sig) n) (i : Fin.t n) (newSymbols : list (option sig)) :
    Vector.t (option sig) n :=
    match newSymbols with
    | nil => readSymbols
    | s :: newSymbols' =>
      match finSucc_opt i with
      | Some i' => insertKnownSymbols (insertKnownSymbol readSymbols i s) i' newSymbols'
      | None => insertKnownSymbol readSymbols i s
      end
    end.

  Lemma insertKnownSymbol_correct (n : nat) (readSymbols : Vector.t (option sig) n) (i : Fin.t n) tps tp :
    length tps = fin_to_nat i ->
    knowsFirstSymbols readSymbols tps ->
    knowsFirstSymbols (insertKnownSymbol readSymbols i (current tp)) (tps ++ [tp]).
  Proof.
    revert i tps tp. induction readSymbols as [ | x n readSymbols IH]; intros; cbn in *.
    - destruct_fin i.
    - pose proof fin_destruct_S i as [ ( i0 & -> ) | -> ]; cbn in *.
      + rewrite fin_to_nat_S in *. destruct tps; cbn in *; inv H. destruct H0 as [H0 H0']. split; auto.
      + destruct tps; cbn in *; inv H. split; auto. apply knowsFirstSymbols_nil.
  Qed.

  Lemma insertKnownSymbols_correct (n : nat) (readSymbols : Vector.t (option sig) n) (i : Fin.t n) tps1 tps2 :
    length tps1 = fin_to_nat i ->
    length tps1 + length tps2 = n ->
    knowsFirstSymbols readSymbols tps1 ->
    knowsFirstSymbols (insertKnownSymbols readSymbols i (map (@current _) tps2)) (tps1 ++ tps2).
  Proof.
    revert n i tps1 readSymbols. induction tps2 as [ | tp' tps2 IH]; cbn; intros.
    - now rewrite app_nil_r.
    - subst.
      destruct (finSucc_opt i) as [ i' | ] eqn:E.
      + pose proof finSucc_opt_Some' E as E'.
        rewrite app_comm_cons'. apply IH; simpl_list; cbn. omega. omega.
        apply insertKnownSymbol_correct; auto.
      + apply finSucc_opt_None' in E.
        assert (| tps2 | = 0) by omega.
        destruct tps2; cbn in *; inv H0.
        apply insertKnownSymbol_correct; auto.
  Qed.


  Lemma knowsFirstSymbols_all n (tps : list (tape sig)) (symbols : Vector.t (option sig) n) :
    length tps = n ->
    knowsFirstSymbols symbols tps ->
    vector_to_list symbols = map (@current _) tps.
  Proof.
    revert tps. induction symbols; cbn; intros.
    - destruct tps; cbn in *; auto.
    - destruct tps; cbn in *; inv H. destruct H0 as [ <- ?]. f_equal. auto.
  Qed.

  Lemma knowsFirstSymbols_all' n (T : tapes sig n) (symbols : Vector.t (option sig) n) :
    knowsFirstSymbols symbols (vector_to_list T) ->
    symbols = current_chars T.
  Proof.
    induction T as [ | tp n T IH]; intros; cbn in *.
    - destruct_vector. reflexivity.
    - destruct_vector. unfold current_chars. cbn in *. destruct H as [ <- H]. f_equal. auto.
  Qed.

  Lemma insertKnownSymbols_correct_cons n (T : tapes sig (S n)) (min minSucc : Fin.t (S n)) :
    fin_to_nat min = 0 ->
    fin_to_nat minSucc = 1 ->
    insertKnownSymbols (insertKnownSymbol (Vector.const None (S n)) min (current (Vector.hd T))) minSucc
                       (map (@current _) (vector_to_list (Vector.tl T))) =
    current_chars T.
  Proof.
    intros HMin_val HMinSucc_val.
    unshelve epose proof @insertKnownSymbols_correct (S n) (Vector.const None (S n)) min nil (vector_to_list T) _ _ _.
    - cbn. auto.
    - cbn. apply vector_to_list_length.
    - cbn. tauto.
    - cbn in *. apply knowsFirstSymbols_all' in H. rewrite <- H.
      assert (min = Fin.F1) as -> by now apply fin_is_0. cbn.
      destruct n as [ | n'].
      + destruct_fin minSucc; auto. omega.
      + assert (minSucc = Fin.FS Fin.F1) as -> by now apply fin_is_1.
        destruct_tapes. cbn. auto.
  Qed.



End BookKeepingForRead.

Section ToSingleTape.

  Variable (sig F : finType).
  Variable n : nat.
  Notation nMax := (finMax' n).
  Local Arguments finMax' : simpl never.

  Notation sigSim := (FinType(EqType(boundary + sigList (sigTape sig)))).

  Implicit Types (T : tapes sig n).

  Definition contains_tapes (t : tape sigSim) T :=
    t = midtape nil (inl START) (map inr (encode_tapes T) ++ [inl STOP]).
  Notation "t ≃ T" := (contains_tapes t T) (at level 70, no associativity).

  Hypothesis pM : pTM sig F n.

  Section GoToCurrent.

    Definition atStart (t : tape sigSim) (tps : list (tape sig)) : Prop :=
      t = midtape nil (inl START) (map inr (encode_list _ tps) ++ [inl STOP]).

    Definition atCons (t : tape sigSim) (tps1 tps2 : list (tape sig)) (tp : tape sig) : Prop :=
      t = midtape (map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
                  (inr (sigList_cons))
                  (map inr (map sigList_X (encode_tape tp)) ++ map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atNil (t : tape sigSim) (tps : list (tape sig)) : Prop :=
      t = midtape (map inr (rev (removelast (encode_list _ tps))) ++ [inl START]) (inr (sigList_nil)) [inl STOP].

    Definition atCons_current_niltape (t : tape sigSim) (tps1 tps2 : list (tape sig)) : Prop :=
      t = midtape
            (inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X NilBlank))
            (map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current_leftof (t : tape sigSim) (tps1 tps2 : list (tape sig)) (r : sig) (rs : list sig) :=
      t = midtape
            (inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X (LeftBlank true)))
            (inr (sigList_X (UnmarkedSymbol r)) ::
                 map (fun s => inr (sigList_X (UnmarkedSymbol s))) rs ++ inr (sigList_X (RightBlank false)) ::
                 map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current_midtape (t : tape sigSim) (tps1 tps2 : list (tape sig)) (ls : list sig) (m : sig) (rs : list sig) :=
      t = midtape
            (map (fun s => inr (sigList_X (UnmarkedSymbol s))) ls ++
                 inr (sigList_X (LeftBlank false)) :: inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X (MarkedSymbol m)))
            (map (fun s => inr (sigList_X (UnmarkedSymbol s))) rs ++ inr (sigList_X (RightBlank false)) ::
                 map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current_rightof (t : tape sigSim) (tps1 tps2 : list (tape sig)) (l :sig) (ls : list sig) :=
      t = midtape
            (inr (sigList_X (UnmarkedSymbol l)) ::
                 map (fun s => inr (sigList_X (UnmarkedSymbol s))) ls ++
                 inr (sigList_X (LeftBlank false)) :: inr (sigList_cons) :: map inr (rev (removelast (encode_list _ tps1))) ++ [inl START])
            (inr (sigList_X (RightBlank true)))
            (map inr (encode_list _ tps2) ++ [inl STOP]).

    Definition atCons_current (t : tape sigSim) (tps1 tps2 : list (tape sig)) (tp : tape sig) :=
      match tp with
      | niltape _ => atCons_current_niltape t tps1 tps2
      | leftof r rs => atCons_current_leftof t tps1 tps2 r rs
      | midtape ls m rs => atCons_current_midtape t tps1 tps2 ls m rs
      | rightof l ls => atCons_current_rightof t tps1 tps2 l ls
      end.

    Definition tape_dir (t : tape sig) : option move :=
      match t with
      | niltape _ => None
      | leftof _ _ => Some L
      | midtape _ _ _ => Some N
      | rightof _ _ => Some R
      end.

    Definition isMarked' (s : sigSim) : bool :=
      match s with
      | inr (sigList_X s) => isMarked s
      | _ => false
      end.

    Definition IsCons_Rel : pRel sigSim bool 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tps2 tp,
            atCons tin[@Fin0] tps1 tps2 tp ->
            atCons tout[@Fin0] tps1 tps2 tp /\
            yout = true) /\
        (forall tps,
            atNil tin[@Fin0] tps ->
            atNil tout[@Fin0] tps /\
            yout = false).

    Definition IsCons : pTM sigSim bool 1 :=
      Switch ReadChar
             (fun (s : option sigSim) =>
                match s with
                | Some (inr (sigList_cons)) => Return Nop true
                | Some (inr (sigList_nil)) => Return Nop false
                | _ => Return Nop default
                end).

    Definition IsCons_steps := 2.

    Lemma IsCons_Sem : IsCons ⊨c(IsCons_steps) IsCons_Rel.
    Proof.
      unfold IsCons_steps. eapply RealiseIn_monotone.
      { unfold IsCons. TM_Correct. }
      { Unshelve. 4-5: reflexivity. all: reflexivity. }
      {
        intros tin (yout, tout) H. split.
        { intros tps1 tps2 tp HCons. unfold atCons in *. TMSimp. auto. }
        { intros tps HNil. unfold atNil in *. TMSimp. auto. }
      }
    Qed.

    Definition GoToCurrent_Rel : pRel sigSim (option move) 1 :=
      fun tin '(yout, tout) =>
        forall (tps1 tps2 : list (tape sig)) (tp : tape sig),
          atCons tin[@Fin0] tps1 tps2 tp ->
          atCons_current tout[@Fin0] tps1 tps2 tp /\
          yout = tape_dir tp.

    Definition GoToCurrent : pTM sigSim (option move) 1 :=
      MoveToSymbol isMarked' id;;
      Switch ReadChar
      (fun (c : option sigSim) =>
         match c with
         | Some (inr (sigList_X (RightBlank true))) => Return Nop (Some R)
         | Some (inr (sigList_X (LeftBlank true))) => Return Nop (Some L)
         | Some (inr (sigList_X (MarkedSymbol _))) => Return Nop (Some N)
         | Some (inr (sigList_X NilBlank)) => Return Nop (None)
         | _ => Return Nop None
         end).

    Lemma GoToCurrent_Realise : GoToCurrent ⊨ GoToCurrent_Rel.
    Proof.
      eapply Realise_monotone.
      { unfold GoToCurrent. TM_Correct. }
      {
        intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons in *. TMSimp.
        pose proof (destruct_tapes1 tmid) as (tmid'&->). pose proof (destruct_tapes1 tout) as (tout'&->). TMSimp. rename H1 into H. clear HCons.
        destruct tp as [ | r rs | l ls | ls m rs]; cbn in *; TMSimp.
        -
          do 2 ( rewrite MoveToSymbol_Fun_equation in *; cbn in * ). TMSimp.
          split; eauto. hnf. reflexivity.
        -
          do 2 ( rewrite MoveToSymbol_Fun_equation in *; cbn in * ). TMSimp.
          split; auto. hnf. cbn. f_equal. rewrite !List.map_map, !map_app, <- !app_assoc, !List.map_map. cbn. reflexivity.
        -
          replace (inr (sigList_X (LeftBlank false)) ::
                       map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true])) ++
                       map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
              ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l])))
                 ++ inr (sigList_X (RightBlank true)) :: (map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]))
            in H by (now simpl_list; cbn; rewrite <- !app_assoc).
          rewrite MoveToSymbol_correct_midtape in H; cbn; auto.
          + cbn in *. TMSimp. split; auto. hnf. f_equal.
            rewrite !map_id, !List.map_map. cbv [id].
            rewrite !map_app; cbn. rewrite !List.map_map. rewrite rev_app_distr. cbn. rewrite !map_rev, rev_involutive, <- app_assoc. reflexivity.
          + rewrite !map_app, !List.map_map. cbn. intros ? [<- | [(?&<-&?)%in_map_iff | [<- | ?]] % in_app_iff ]; cbn; auto.
        -
          replace (inr (sigList_X (LeftBlank false)) ::
                       map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
              ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls))))
                 ++ inr (sigList_X (MarkedSymbol m)) ::
                 (map inr (map sigList_X (map UnmarkedSymbol rs ++ [RightBlank false])) ++
                      map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])) in H.
          rewrite MoveToSymbol_correct_midtape in H; cbn; auto.
          + cbn in *. TMSimp. split; auto. hnf.
            rewrite !map_id, !List.map_map. cbv [id].
            rewrite !map_app; cbn. rewrite !List.map_map, <- !app_assoc. rewrite map_rev, rev_involutive. f_equal.
          + rewrite !List.map_map. intros ? [ <- | (?&<-&?) % in_map_iff]; cbn; auto.
          + simpl_list. cbn. f_equal. f_equal. f_equal. rewrite !map_app, <- !app_assoc. cbn. f_equal.
      }
    Qed.

    Definition GoToCurrent_steps' (tp : tape sig) :=
      match tp with
       | niltape _ => 8
       | leftof r rs => 8
       | rightof l ls => 16 + 4 * length ls
       | midtape ls m rs => 16 + 4 * length ls
       end.

    Definition GoToCurrent_steps (tp : tape sig) :=
       GoToCurrent_steps' tp + 3.

    Definition GoToCurrent_T : tRel sigSim 1 :=
      fun tin k => exists tps1 tps2 tp, atCons tin[@Fin0] tps1 tps2 tp /\ GoToCurrent_steps tp <= k.

    Lemma GoToCurrent_Terminates : projT1 GoToCurrent ↓ GoToCurrent_T.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold GoToCurrent. TM_Correct. }
      { intros tin k (tps1&tps2&tp&HCons&Hk). unfold GoToCurrent_steps in Hk.
        exists (GoToCurrent_steps' tp), 2. cbn.
        repeat split. 2: omega.
        {
          destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp; clear HCons tin.
          - do 2 ( rewrite MoveToSymbol_steps_equation; cbn in * ). reflexivity.
          - do 2 ( rewrite MoveToSymbol_steps_equation; cbn in * ). reflexivity.
          -
            replace (inr (sigList_X (LeftBlank false)) ::
                         map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true])) ++
                         map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
                ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l])))
                   ++ inr (sigList_X (RightBlank true)) :: (map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]))
              by (now simpl_list; cbn; rewrite <- !app_assoc).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. rewrite Nat.mul_succ_r. cbn. omega.
          -
            replace (inr (sigList_X (LeftBlank false)) ::
                         map inr (map sigList_X (map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false])) ++ map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP]) with
                ((inr (sigList_X (LeftBlank false)) :: map inr (map sigList_X (map UnmarkedSymbol (rev ls))))
                   ++ inr (sigList_X (MarkedSymbol m)) ::
                   (map inr (map sigList_X (map UnmarkedSymbol rs ++ [RightBlank false])) ++
                        map inr (encode_list (Encode_tape (eqType_X (type sig))) tps2) ++ [inl STOP])).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            + simpl_list. cbn. omega.
            + simpl_list. cbn. f_equal. f_equal. f_equal. rewrite !map_app, <- !app_assoc. cbn. f_equal.
        }
        { intros ? [] ?. exists 1, 0. repeat split. omega. omega. intros ? ? (->&->). destruct *; reflexivity. }
      }
    Qed.

  End GoToCurrent.

  Section GoToNext.

    Definition GoToNext_Rel : pRel sigSim bool 1 :=
      fun tin '(yout, tout) =>
        forall tps1 tps2 tp,
          atCons_current tin[@Fin0] tps1 tps2 tp ->
          match yout, tps2 with
          | true, tp' :: tps2' =>
            atCons tout[@Fin0] (tps1 ++ [tp]) tps2' tp'
          | false, nil =>
            atNil tout[@Fin0] (tps1 ++ [tp])
          | _, _ => False
          end.

    Definition isNilCons : sigSim -> bool :=
      fun s => match s with
            | inr sigList_nil => true
            | inr sigList_cons => true
            | _ => false
            end.

    Definition GoToNext : pTM sigSim bool 1 :=
      MoveToSymbol isNilCons id;; IsCons.

    Lemma GoToNext_Realise : GoToNext ⊨ GoToNext_Rel.
    Proof.
      eapply Realise_monotone.
      { unfold GoToNext. TM_Correct. eapply RealiseIn_Realise. apply IsCons_Sem. }
      {
        intros tin (yout, tout) H. intros tps1 tps2 tp HCons. unfold atCons_current in *. TMSimp.
        pose proof (destruct_tapes1 tin) as (tin'&->). pose proof (destruct_tapes1 tmid) as (tmid'&->). pose proof (destruct_tapes1 tout) as (tout'&->). TMSimp. rename H1 into H.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp; rename H into HNil, H0 into HCons.
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [niltape _])). spec_assert HNil as [HNil ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn). hnf.
            cbv [id]. hnf. f_equal. rewrite encode_list_app. rewrite removelast_app by apply encode_list_neq_nil.
            cbn. rewrite rev_app_distr. cbn. f_equal.
          - specialize (HCons (tps1 ++ [niltape _]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn).
            cbv [id]. hnf. f_equal.
            + rewrite encode_list_app; cbn. rewrite removelast_app by congruence.
              cbn. rewrite rev_app_distr. cbn. f_equal.
            + rewrite !List.map_map. rewrite !map_app, <- !app_assoc. now rewrite !List.map_map. }
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [leftof r rs])). spec_assert HNil as [HNil ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_correct_midtape; cbn in *; auto.
            + rewrite !map_id; cbv [id]. hnf. f_equal.
              simpl_list. cbn. rewrite encode_list_app. cbn.
              rewrite !map_app. cbn. rewrite !removelast_app by congruence. rewrite !removelast_cons by congruence.
              rewrite removelast_cons.
              2: { intros H. symmetry in H. now apply app_cons_not_nil in H. }
              rewrite removelast_app by congruence. cbn. rewrite app_nil_r.
              rewrite rev_app_distr. cbn. rewrite <- !app_assoc.
              rewrite !rev_app_distr, <- !app_assoc. cbn. rewrite !map_rev.
              rewrite map_app, <- !app_assoc. cbn. rewrite !map_rev, !List.map_map. f_equal.
            + intros ? [ <- | [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff ]; cbn; auto.
          - specialize (HCons (tps1 ++ [leftof r rs]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_correct_midtape; cbn in *; auto.
            + rewrite !map_id; cbv [id]. hnf. f_equal.
              * simpl_list. cbn. rewrite encode_list_app. cbn.
                rewrite !map_app. cbn. rewrite !removelast_app by congruence. rewrite !removelast_cons by congruence.
                rewrite removelast_cons.
                2: { intros H. symmetry in H. now apply app_cons_not_nil in H. }
                rewrite removelast_app by congruence. cbn. rewrite app_nil_r.
                rewrite rev_app_distr. cbn. rewrite <- !app_assoc.
                rewrite !rev_app_distr, <- !app_assoc. cbn. rewrite !map_rev.
                rewrite map_app, <- !app_assoc. cbn. rewrite !map_rev, !List.map_map. f_equal.
              * now simpl_list.
            + intros ? [ <- | [ (?&<-&?) % in_map_iff | [ <- | ] ] % in_app_iff ]; cbn; auto.
        }
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [rightof l ls])). spec_assert HNil as [HNil ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn).
            cbv [id]. hnf. f_equal.
            rewrite encode_list_app. cbn. rewrite removelast_app by congruence.
            rewrite !removelast_cons. 3: congruence.
            2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
            rewrite map_app, !List.map_map, <- !app_assoc. cbn.
            rewrite removelast_app by congruence. cbn.
            rewrite rev_app_distr; cbn. rewrite <- !app_assoc. cbn. rewrite !map_app, <- !app_assoc.
            rewrite !rev_app_distr. cbn. rewrite !map_rev, rev_involutive. rewrite !List.map_map. reflexivity.
          - specialize (HCons (tps1 ++ [rightof l ls]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            do 2 (rewrite MoveToSymbol_Fun_equation; cbn).
            cbv [id]. hnf. f_equal.
            + rewrite encode_list_app. cbn. rewrite removelast_app by congruence.
              rewrite !removelast_cons. 3: congruence.
              2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
              rewrite map_app, !List.map_map, <- !app_assoc. cbn.
              rewrite removelast_app by congruence. cbn.
              rewrite rev_app_distr; cbn. rewrite <- !app_assoc. cbn. rewrite !map_app, <- !app_assoc.
              rewrite !rev_app_distr. cbn. rewrite !map_rev, rev_involutive. rewrite !List.map_map. reflexivity.
            + now simpl_list.
        }
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - specialize (HNil (tps1 ++ [midtape ls m rs])). spec_assert HNil as [HNil ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_correct_midtape; cbn; auto.
            + cbn in *. TMSimp. rewrite map_id; cbv [id]. hnf. f_equal.
              rewrite encode_list_app. cbn. rewrite !map_app.
              rewrite removelast_app by congruence.
              rewrite !removelast_cons. 3: congruence.
              2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
              rewrite removelast_app by congruence. cbn. rewrite !map_rev.
              simpl_list. cbn. rewrite <- !app_assoc. cbn. rewrite !map_app. cbn. rewrite !map_rev.
              repeat first [ progress cbn | rewrite rev_app_distr | rewrite map_app | rewrite <- app_assoc | rewrite rev_involutive | rewrite map_map ].
              f_equal.
            + intros ? [ (?&<-&?) % in_map_iff | [<- | ] ] % in_app_iff; cbn; auto.
          - specialize (HCons (tps1 ++ [midtape ls m rs]) tps2' tp'). spec_assert HCons as [HCons ->]; auto.
            rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_correct_midtape; cbn; auto.
            + cbn in *. TMSimp. rewrite map_id; cbv [id]. hnf. f_equal.
              rewrite encode_list_app. cbn. rewrite !map_app.
              * rewrite removelast_app by congruence.
                rewrite !removelast_cons. 3: congruence.
                2: { intros H; symmetry in H; now apply app_cons_not_nil in H. }
                rewrite removelast_app by congruence. cbn. rewrite !map_rev.
                simpl_list. cbn. rewrite <- !app_assoc. cbn. rewrite !map_app. cbn. rewrite !map_rev.
                repeat first [ progress cbn | rewrite rev_app_distr | rewrite map_app | rewrite <- app_assoc | rewrite rev_involutive | rewrite map_map ].
                f_equal.
              * now simpl_list.
            + intros ? [ (?&<-&?) % in_map_iff | [<- | ] ] % in_app_iff; cbn; auto.
        }
      }
    Qed.

    Definition GoToNext_steps' (t : tape sig) :=
      match t with
      | niltape _ => 8
      | leftof r rs => 16 + 4 * length rs
      | rightof r rs => 8
      | midtape ls m rs => 16 + 4 * length rs
      end.

    Definition GoToNext_steps (tp : tape sig) :=
        GoToNext_steps' tp + 3.

    Definition GoToNext_T : tRel sigSim 1 :=
      fun tin k => exists tps1 tps2 tp, atCons_current tin[@Fin0] tps1 tps2 tp /\ GoToNext_steps tp <= k.

    Lemma GoToNext_Terminates : projT1 GoToNext ↓ GoToNext_T.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold GoToNext. TM_Correct. eapply RealiseIn_TerminatesIn. apply IsCons_Sem. }
      { intros tin k (tps1&tps2&tp&HCons&Hk). hnf in HCons. unfold GoToNext_steps in Hk.
        exists (GoToNext_steps' tp), 2. repeat split. 2: omega. 2: intros _ _ _; reflexivity.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp; clear tin HCons.
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
        }
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. omega.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite app_comm_cons with (a := inr (sigList_X (UnmarkedSymbol r))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. omega.
        }
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
          - do 2 (rewrite MoveToSymbol_steps_equation; cbn). reflexivity.
        }
        {
          destruct tps2 as [ | tp' tps2']; cbn in *.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. omega.
          - rewrite app_comm_cons' with (a := inr (sigList_X (RightBlank false))).
            rewrite MoveToSymbol_steps_midtape; cbn; auto.
            simpl_list. cbn. omega.
        }
      }
    Qed.

  End GoToNext.

  Section ReadCurrentSymbols.

    Local Arguments insertKnownSymbol : simpl never.

    Definition ReadCurrent : pTM sigSim (option sig) 1 :=
      Switch ReadChar
             (fun (s : option sigSim) =>
                match s with
                | Some (inr (sigList_X (MarkedSymbol s))) => Return Nop (Some s)
                | _ => Return Nop None
                end).

    Definition ReadCurrent_Rel : pRel sigSim (option sig) 1 :=
      fun tin '(yout, tout) =>
        forall tps1 tps2 tp,
          atCons_current tin[@Fin0] tps1 tps2 tp ->
          atCons_current tout[@Fin0] tps1 tps2 tp /\
          yout = current tp.

    Definition ReadCurrent_steps := 2.

    Lemma ReadCurrent_Sem : ReadCurrent ⊨c(ReadCurrent_steps) ReadCurrent_Rel.
    Proof.
      unfold ReadCurrent_steps. eapply RealiseIn_monotone.
      { unfold ReadCurrent. TM_Correct. }
      { Unshelve. 4,5: reflexivity. all: reflexivity. }
      { intros tin (yout, tout) H. intros tps1 tps2 tp HCons.
        unfold atCons_current in *. TMSimp.
        destruct tp as [ | r rs | l ls | ls m rs ]; cbn in *; hnf in HCons; TMSimp.
        all: (split; hnf; auto).
      }
    Qed.

    Definition ReadCurrentSymbols_Step_Rel (st : Vector.t (option sig) n * Fin.t n) :
      pRel sigSim (Vector.t (option sig) n * Fin.t n + Vector.t (option sig) n) 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tps2 tp ,
            (length tps1 =? fin_to_nat (snd st)) = true ->
            (length tps1 + (1 + length tps2) =? n) = true ->
            atCons tin[@Fin0] tps1 tps2 tp ->
            knowsFirstSymbols (fst st) tps1 ->
            match tps2 with
            | nil =>
              atNil tout[@Fin0] (tps1 ++ [tp]) /\
              yout = inr (insertKnownSymbol (fst st) (snd st) (current tp))
            | tp' :: tps2' =>
              atCons tout[@Fin0] (tps1 ++ [tp]) tps2' tp' /\
              match finSucc_opt (snd st) with
              | Some i' =>
                yout = inl (insertKnownSymbol (fst st) (snd st) (current tp), i')
              | None => False
              end
            end) /\
        (forall tps,
            atNil tin[@Fin0] tps ->
            atNil tout[@Fin0] tps /\
            yout = inr (fst st)).

    Definition ReadCurrentSymbols_Step : forall (st : Vector.t (option sig) n * Fin.t n),
        pTM sigSim (Vector.t (option sig) n * Fin.t n + Vector.t (option sig) n) 1 :=
      fun '(readSymbols, i) =>
        If IsCons
           (GoToCurrent;;
            Switch (ReadCurrent)
                   (fun (c : option sig) =>
                      Return (GoToNext)
                             (match finSucc_opt i with
                              | None =>
                                inr (insertKnownSymbol readSymbols i c)
                              | Some i' =>
                                inl (insertKnownSymbol readSymbols i c, i')
                              end)))
           (Return Nop (inr readSymbols)).

    Lemma ReadCurrentSymbols_Step_Realise : forall st, ReadCurrentSymbols_Step st ⊨ ReadCurrentSymbols_Step_Rel st.
    Proof.
      intros (readSymbols,i). eapply Realise_monotone.
      { unfold ReadCurrentSymbols_Step. TM_Correct_step; [ | TM_Correct_step | TM_Correct].
        - eapply RealiseIn_Realise. apply IsCons_Sem.
        - apply GoToCurrent_Realise.
        - apply Switch_Realise.
          + eapply RealiseIn_Realise. apply ReadCurrent_Sem.
          + intros c. apply Return_Realise. apply GoToNext_Realise. }
      {
        intros tin (yout, tout). TMSimp. split.
        {
          intros tps1 tps2 tp HL1 HL2 HCons HKnown.
          destruct H; TMSimp.
          {
            rename H into HIsCons_cons, H0 into HGotoCurrent, H1 into IsCons_nil, H2 into HReadCurrent, H4 into HGoToNext.
            specialize HIsCons_cons with (1 := HCons) as (HIsCons_cons&_).
            specialize HGotoCurrent with (1 := HIsCons_cons) as (HGotoCurrent&->).
            specialize HReadCurrent with (1 := HGotoCurrent) as (HReadCurrent&->).
            specialize HGoToNext with (1 := HReadCurrent).
            destruct ymid1, tps2 as [ | tp' tps2']; auto.
            { split; auto.
              destruct (finSucc_opt i) as [i'| ] eqn:Ei.
              - reflexivity.
              - exfalso. apply finSucc_opt_None' in Ei. apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. cbn in *. omega.
            }
            { split; auto.
              enough (finSucc_opt i = None) as -> by reflexivity.
              apply finSucc_opt_None.
              apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2. cbn in *. omega.
            }
          }
          { specialize H with (1 := HCons) as (_&H); congruence. }
        }
        {
          intros tps HNil.
          destruct H; TMSimp.
          { specialize H1 with (1 := HNil) as (_&H1); congruence. }
          { now specialize H0 with (1 := HNil) as (H0&_). }
        }
      }
    Qed.

    Definition ReadCurrentSymbols_Step_steps_cons tp :=
      3 + IsCons_steps + GoToCurrent_steps tp + ReadCurrent_steps + GoToNext_steps tp.

    Definition ReadCurrentSymbols_Step_steps_nil := 1 + IsCons_steps.

    Definition ReadCurrentSymbols_Step_T : tRel sigSim 1 :=
      fun tin k =>
        (exists tps1 tps2 tp, atCons tin[@Fin0] tps1 tps2 tp /\ ReadCurrentSymbols_Step_steps_cons tp <= k) \/
        (exists tps, atNil tin[@Fin0] tps /\ ReadCurrentSymbols_Step_steps_nil <= k).

    Lemma ReadCurrentSymbols_Step_Terminates st : projT1 (ReadCurrentSymbols_Step st) ↓ ReadCurrentSymbols_Step_T.
    Proof.
      destruct st as [readSymbols i]. eapply TerminatesIn_monotone.
      { unfold ReadCurrentSymbols_Step. TM_Correct_step.
        { eapply RealiseIn_Realise. apply IsCons_Sem. }
        { eapply RealiseIn_TerminatesIn. apply IsCons_Sem. }
        { TM_Correct_step. apply GoToCurrent_Realise. apply GoToCurrent_Terminates.
          apply Switch_TerminatesIn.
          - eapply RealiseIn_Realise. apply ReadCurrent_Sem.
          - eapply RealiseIn_TerminatesIn. apply ReadCurrent_Sem.
          - intros st. apply Return_Terminates. apply GoToNext_Terminates. }
        { TM_Correct. }
      }
      {
        intros tin k. intros [ (tps1&tps2&tp&HCons&Hk) | (tps&HNil&Hk) ].
        { unfold ReadCurrentSymbols_Step_steps_cons in Hk.
          exists (IsCons_steps), (2 + GoToCurrent_steps tp + ReadCurrent_steps + GoToNext_steps tp). repeat split; try omega.
          intros tmid ymid (HIsCons_cons&HIsCons_nil). specialize HIsCons_cons with (1 := HCons) as (HIsCons&->).
          exists (GoToCurrent_steps tp), (1 + ReadCurrent_steps + GoToNext_steps tp). repeat split; try omega. hnf; eauto.
          intros tmid0 ymid0 HGoToCurrent. cbn in HGoToCurrent. specialize HGoToCurrent with (1 := HIsCons) as (HGoToCurrent&->).
          exists (ReadCurrent_steps), (GoToNext_steps tp). repeat split; try omega.
          intros tmid1 ymid1 HReadCurrent. cbn in HReadCurrent. specialize HReadCurrent with (1 := HGoToCurrent) as (HReadCurrent&->). hnf. eauto.
        }
        { unfold ReadCurrentSymbols_Step_steps_nil in Hk.
          exists (IsCons_steps), 0. repeat split; try omega.
          intros tmid ymid (HIsCons_cons&HIsCons_nil). specialize HIsCons_nil with (1 := HNil) as (HIsNil&->). reflexivity.
        }
      }
    Qed.

    Definition ReadCurrentSymbols_Loop := StateWhile ReadCurrentSymbols_Step.

    Definition ReadCurrentSymbols_Loop_Rel (st : Vector.t (option sig) n * Fin.t n) :
      pRel sigSim (Vector.t (option sig) n) 1 :=
      fun tin '(yout, tout) =>
        (forall tps1 tp tps2,
            (length tps1 =? fin_to_nat (snd st)) = true ->
            (length tps1 + (1 + length tps2) =? n) = true ->
            atCons tin[@Fin0] tps1 tps2 tp ->
            knowsFirstSymbols (fst st) tps1 ->
            atNil tout[@Fin0] (tps1 ++ tp :: tps2) /\
            yout = insertKnownSymbols (fst st) (snd st) (current tp :: map (@current _) tps2)) /\
        (forall tps,
            (length tps =? n) = true ->
            atNil tin[@Fin0] tps ->
            knowsFirstSymbols (fst st) tps ->
            atNil tout[@Fin0] tps /\
            yout = (fst st)).

    Lemma ReadCurrentSymbols_Loop_Realise st : ReadCurrentSymbols_Loop st ⊨ ReadCurrentSymbols_Loop_Rel st.
    Proof.
      eapply Realise_monotone.
      { unfold ReadCurrentSymbols_Loop. TM_Correct. apply ReadCurrentSymbols_Step_Realise. }
      { revert st. apply StateWhileInduction; intros; rename l into st.
        {
          destruct st as [ readSymbols i]; cbn in *.
          destruct HLastStep as [HLastStepCons HLastStepNil].
          cbn. split; [intros tps1 tp tps2 HL1 HL2 HCons HRead | intros tps HL HNil HRead]; TMSimp.
          {
            specialize HLastStepCons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
            destruct tps2 as [ | tp' tps2']; cbn in *.
            - destruct HLastStepCons as [HLastStepCons HLastStepCons']; inv HLastStepCons'.
              split; auto.
              destruct (finSucc_opt i) as [i'| ]; auto.
            - destruct HLastStepCons as [ HLastStepCons HLastStepCons'].
              destruct (finSucc_opt i) as [i' | ]; auto. congruence.
          }
          { specialize HLastStepNil with (1 := HNil). destruct HLastStepNil as [H1 H2]. inv H2. split; auto. }
        }
        {
          destruct st as [ readSymbols i]; cbn in *.
          destruct HStar as [HStar_cons HStar_nil]. destruct HLastStep as [HLastStep_cons HLastStep_nil]. cbn in *.
          cbn. split; [intros tps1 tp tps2 HL1 HL2 HCons HRead | intros tps HL HNil HRead].
          {
            specialize HStar_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
            destruct tps2 as [ | tp' tps2']; cbn in *.
            - destruct HStar_cons as [HStar1 HStar2]. inv HStar2.
            - destruct HStar_cons as [HStar1 HStar2].
              destruct (finSucc_opt i) as [i' | ] eqn:E; auto. inv HStar2.
              specialize HLastStep_cons with (3 := HStar1).
              apply Nat.eqb_eq in HL1. apply Nat.eqb_eq in HL2.
              spec_assert HLastStep_cons.
              { simpl_list; cbn. apply Nat.eqb_eq. apply finSucc_opt_Some' in E. omega. }
              spec_assert HLastStep_cons.
              { simpl_list; cbn. apply Nat.eqb_eq. apply finSucc_opt_Some' in E. omega. }
              spec_assert HLastStep_cons as [HLastStep_cons ->].
              { cbn. apply insertKnownSymbol_correct; auto. }
              cbn in *. rewrite <- app_assoc in HLastStep_cons. split; auto.
          }
          { specialize HStar_nil with (1 := HNil) as [HStar1 HStar2]; inv HStar2. }
        }
      }
    Qed.

    Definition ReadCurrentSymbols_Loop_steps_nil := ReadCurrentSymbols_Step_steps_nil.

    Fixpoint ReadCurrentSymbols_Loop_steps_cons tps2 tp :=
      match tps2 with
      | nil => ReadCurrentSymbols_Step_steps_cons tp
      | tp' :: tps2' => 1 + ReadCurrentSymbols_Step_steps_cons tp + ReadCurrentSymbols_Loop_steps_cons tps2' tp'
      end.

    Definition ReadCurrentSymbols_Loop_T (st : Vector.t (option sig) n * Fin.t n) : tRel sigSim 1 :=
      fun tin k =>
        (exists tps1 tps2 tp,
            (length tps1 =? fin_to_nat (snd st)) = true /\
            (length tps1 + (1 + length tps2) =? n) = true /\
            knowsFirstSymbols (fst st) tps1 /\
            atCons tin[@Fin0] tps1 tps2 tp /\ ReadCurrentSymbols_Loop_steps_cons tps2 tp <= k) \/
        (exists tps, atNil tin[@Fin0] tps /\ ReadCurrentSymbols_Loop_steps_nil <= k).

    Lemma ReadCurrentSymbols_Loop_Terminates st : projT1 (ReadCurrentSymbols_Loop st) ↓ ReadCurrentSymbols_Loop_T st.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold ReadCurrentSymbols_Loop. TM_Correct.
        - apply ReadCurrentSymbols_Step_Realise.
        - apply ReadCurrentSymbols_Step_Terminates. }
      {
        revert st. apply StateWhileCoInduction. intros (readSymbols&i). intros. unfold ReadCurrentSymbols_Loop_T in *. unfold ReadCurrentSymbols_Step_T in *.
        destruct HT as [ (tps1&tps2&tp&HL1&HL2&HRead&HCons&Hk) | (tps&HNil&Hk)].
        {
           eexists. repeat split. left. eauto.
           intros ymid tmid (HStep_cons&HStep_nil). clear HStep_nil. cbn in *. destruct ymid as [ (readSymbols'&i') | result ].
           -
             specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
             destruct tps2 as [ | tp' tps2']; cbn in *.
             + TMSimp congruence.
             + destruct HStep_cons as (HStep_cons1&HStep_cons2). destruct (finSucc_opt i) as [ i'' | ] eqn:Ei; inv HStep_cons2; rename i'' into i'.
               eexists. split. 2: apply Hk. left. exists (tps1 ++ [tp]), (tps2'), tp'. repeat split.
               * simpl_list. cbn. apply finSucc_opt_Some' in Ei. apply Nat.eqb_eq. apply Nat.eqb_eq in HL1. omega.
               * simpl_list. cbn. apply finSucc_opt_Some' in Ei. apply Nat.eqb_eq. apply Nat.eqb_eq in HL2. omega.
               * apply insertKnownSymbol_correct. now apply Nat.eqb_eq. assumption.
               * assumption.
               * reflexivity.
           -
             specialize HStep_cons with (1 := HL1) (2 := HL2) (3 := HCons) (4 := HRead).
             destruct tps2 as [ | tp' tps2']; cbn in *.
             + omega.
             + omega.
        }
        {
          eexists. repeat split. right. eauto.
          intros ymid tmid (HStep_cons&HStep_nil). clear HStep_cons. cbn in *. destruct ymid as [ (readSymbols'&i') | result ].
          - specialize HStep_nil with (1 := HNil) as (?&?). congruence.
          - reflexivity.
        }
      }
    Qed.

    Definition ReadCurrentSymbols :=
      match (finMin_opt n) with
      | None => Return (Move R) (Vector.const None n)
      | Some min =>
        Move R;; ReadCurrentSymbols_Loop (Vector.const None n, min)
      end.

    Definition ReadCurrentSymbols_Rel : pRel sigSim (Vector.t (option sig) n) 1 :=
      fun tin '(yout, tout) =>
        forall T,
          tin[@Fin0] ≃ T ->
          atNil tout[@Fin0] (vector_to_list T) /\
          yout = current_chars T.

    Lemma ReadCurrentSymbols_Realise : ReadCurrentSymbols ⊨ ReadCurrentSymbols_Rel.
    Proof.
      unfold ReadCurrentSymbols.
      destruct (finMin_opt n) as [min| ] eqn:E; swap 1 2.
      {
        eapply Realise_monotone.
        { TM_Correct. }
        { intros tin (yout, tout) H. intros T HEncT. unfold contains_tapes in *. TMSimp.
          clear_except E. apply finMin_opt_None in E as ->. destruct_tapes. cbn.
          split; cbn; auto. hnf. reflexivity.
        }
      }
      {
        eapply Realise_monotone.
        { TM_Correct. apply ReadCurrentSymbols_Loop_Realise. }
        { intros tin (yout, tout) H. intros T HEncT. unfold contains_tapes in *. TMSimp.
          clear tmid H. rename H0 into HLoop_cons, H1 into HLoop_nil. clear HLoop_nil.
          pose proof finMin_opt_Some E as (n'&E'). pose (T' := Vector.cast T E').
          pose proof finMin_opt_Some_val E as E_val.
          specialize (HLoop_cons nil (Vector.hd T') (vector_to_list (Vector.tl T'))). cbn in *.
          rewrite E_val in HLoop_cons. subst. specialize HLoop_cons with (1 := eq_refl). spec_assert HLoop_cons.
          { rewrite vector_to_list_length. apply Nat.eqb_eq. reflexivity. } spec_assert HLoop_cons.
          { hnf. cbn. clear_all. destruct_tapes. cbn. f_equal. simpl_list. now rewrite vector_cast_refl. }
          spec_assert HLoop_cons as [HLoop_cons1 ->] by (cbn; tauto).
          rewrite vector_to_list_eta in HLoop_cons1. subst T'. rewrite vector_cast_refl in *. split; auto.
          destruct (finSucc_opt min) as [minSucc | ] eqn:E2.
          - pose proof finSucc_opt_Some' E2 as E2_val. rewrite E_val in E2_val.
            now apply insertKnownSymbols_correct_cons.
          - apply finSucc_opt_None' in E2.
            apply Nat.succ_inj in E2. assert (n' = 0) as -> by omega. cbn.
            compute [insertKnownSymbol]. destruct_fin min. cbn.
            destruct_tapes. cbn. unfold current_chars. cbn. reflexivity.
        }
      }
    Qed.

    Definition ReadCurrentSymbols_steps (n : nat) (T : tapes sig n) :=
      match T with
      | [||] => ReadCurrentSymbols_Loop_steps_nil
      | tp ::: T' => 2 + ReadCurrentSymbols_Loop_steps_cons (vector_to_list T') tp
      end.

    Definition ReadCurrentSymbols_T : tRel sigSim 1 :=
      fun tin k => exists T, tin[@Fin0] ≃ T /\ ReadCurrentSymbols_steps T <= k.

    Lemma ReadCurrentSymbols_Terminates : projT1 ReadCurrentSymbols ↓ ReadCurrentSymbols_T.
    Proof.
      unfold ReadCurrentSymbols.
      destruct (finMin_opt n) as [min| ] eqn:E.
      { eapply TerminatesIn_monotone.
        { TM_Correct. eapply ReadCurrentSymbols_Loop_Terminates. }
        {
          intros tin k (T&HEncT&Hk).
          pose proof finMin_opt_Some E as (n'&E'). pose proof finMin_opt_Some_val E as E_val.
          pose (T' := Vector.cast T E').
          exists 1, (ReadCurrentSymbols_Loop_steps_cons (vector_to_list (Vector.tl T')) (Vector.hd T')). repeat split; try omega.
          { rewrite <- Hk. clear_all. subst n T'. rewrite !vector_cast_refl. destruct_tapes. cbn. reflexivity. }
          {
            intros tmid [] HMove. cbn in HMove. hnf. left. exists (nil), (vector_to_list (Vector.tl T')), (Vector.hd T'). cbn. rewrite E_val. cbn. repeat split; auto.
            - rewrite vector_to_list_length. apply Nat.eqb_eq. omega.
            - apply knowsFirstSymbols_nil.
            - rewrite HMove. hnf in HEncT. cbn in *. rewrite HEncT. clear_all. subst n T'. cbn. rewrite !vector_cast_refl.
              destruct_tapes. cbn. hnf. f_equal. now rewrite !map_app, !List.map_map, <- !app_assoc.
          }
        }
      }
      { eapply TerminatesIn_monotone.
        { TM_Correct. }
        {
          intros tin k (T&HEnc&Hk). rewrite <- Hk. apply finMin_opt_None in E. clear_except E. subst. destruct_tapes. cbn. unfold ReadCurrentSymbols_Loop_steps_nil, ReadCurrentSymbols_Step_steps_nil. omega.
        }
      }
    Qed.

  End ReadCurrentSymbols.

  Section MoveToStart.

    Definition MoveToStart_Rel : pRel sigSim unit 1 :=
      ignoreParam
        (fun tin tout =>
           forall tps, atNil tin[@Fin0] tps ->
                  atStart tout[@Fin0] tps).

    Definition isStart : sigSim -> bool :=
      fun s => match s with
            | inl START => true
            | _ => false
            end.

    Definition MoveToStart : pTM sigSim unit 1 :=
      MoveToSymbol_L isStart id.

    Lemma MoveToStart_Realise : MoveToStart ⊨ MoveToStart_Rel.
    Proof.
      eapply Realise_monotone.
      { unfold MoveToStart. TM_Correct. }
      {
        intros tin (yout, tout) H. intros tps HNil. unfold atNil, atStart in *. TMSimp. clear_all.
        rewrite MoveToSymbol_L_correct_midtape; cbn; auto.
        - rewrite !map_id; cbv [id]. rewrite map_rev, rev_involutive.
          f_equal.
          change [inr (@sigList_nil (sigTape sig)); inl STOP]
            with (List.map inr [ @sigList_nil (sigTape sig)] ++ [inl STOP]).
          rewrite app_assoc, <- map_app. f_equal. f_equal.
          apply encode_list_remove.
        - intros ? (?&<-&?) % in_map_iff. cbn. reflexivity.
      }
    Qed.


    Definition MoveToStart_steps (tps : list (tape sig)) :=
      8 + 4 * length (encode_list _ tps).

    Definition MoveToStart_T : tRel sigSim 1 :=
      fun tin k => exists tps, atNil tin[@Fin0] tps /\ MoveToStart_steps tps <= k.

    Lemma removelast_length (X : Type) (xs : list X) :
      length (removelast xs) = length xs - 1.
    Proof.
      induction xs as [ | x xs IH].
      - cbn. reflexivity.
      - cbn. destruct xs as [ | x' xs]; cbn in *.
        + reflexivity.
        + f_equal. rewrite IH. omega.
    Qed.

    Lemma MoveToStart_Terminates : projT1 MoveToStart ↓ MoveToStart_T.
    Proof.
      eapply TerminatesIn_monotone.
      { unfold MoveToStart. TM_Correct. }
      {
        intros tin k (tps&HNil&Hk). hnf in HNil. TMSimp. clear HNil tin. rewrite MoveToSymbol_L_steps_midtape; cbn; auto. simpl_list. cbn.
        rewrite <- Hk. rewrite removelast_length. unfold MoveToStart_steps. omega.
      }
    Qed.

    Lemma atStart_contains (t : tape sigSim) (tps : list (tape sig)) (T : tapes sig n) :
      length tps = n ->
      atStart t tps ->
      vector_to_list T = tps ->
      t ≃ T.
    Proof.
      intros HL HStart HToList. unfold contains_tapes, atStart in *. subst.
      f_equal. f_equal. f_equal. unfold encode_tapes. f_equal. auto.
    Qed.

  End MoveToStart.

  Section DoActions.

    Variable (acts : Vector.t (option sig * move) n).

    Definition isReturnMarker (s : sigSim) : bool :=
      match s with
      | inl UNKNOWN => true
      | _ => false
      end.