From Undecidability.TM.Util Require Export Prelim Relations.
Require Import Undecidability.Shared.Libs.PSL.Vectors.Vectors.
Require Export Undecidability.TM.TM.

Section Fix_Sigma.

  Variable sig : Type.

  Notation tape := (tape sig).




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

  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.




  Global Instance move_eq_dec : eq_dec move.
  Proof.
    intros. hnf. decide equality.
  Defined.
  Global Instance move_finC : finTypeC (EqType move).
  Proof.
    apply (FinTypeC (enum := [Lmove; Rmove; Nmove])).
    intros []; now cbv.
  Defined.

  Definition tape_move_right' ls a rs : tape :=
    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 : tape :=
    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
    | Rmove => tape_move_right t
    | Lmove => tape_move_left t
    | Nmove => t
    end.


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

  Lemma tapeToList_move_L (t : tape) :
    tapeToList (tape_move_left t) = tapeToList t.
  Proof. apply (tapeToList_move t Lmove). 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.


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

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

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

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

End Fix_Sigma.


Ltac destruct_tapes := unfold tapes in *; destruct_vector.

Create HintDb tape.
Create HintDb vector.

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.

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


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

  Definition nop_action := Vector.const (@None sig, Nmove) 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.

Arguments nop_action {_ _}.


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 | Nmove => Nmove | Lmove => Rmove | Rmove => Lmove 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.


Section Tape_Local.

  Variable sig : Type.

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

  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.


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.


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.

Section MatchTapes.
  Variable sig : Type.


  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.


  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.

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

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

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

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

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

  Lemma tape_write_current (t : tape sig) s :
    current (tape_write t s) = fold_opt (@Some _) (current t) s.
  Proof. destruct s; auto. 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.

Hint Rewrite tape_move_niltape tape_write_left tape_write_right tape_write_current_Some tape_write_current_None tape_write_current : tape.

Section Semantics.

  Variable sig : finType.

  Notation TM := (TM sig).
  Definition pTM (F: Type) (n:nat) := { M : TM n & state M -> F }.


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


  Definition step {n} (M:TM n) : mconfig (state M) n -> mconfig (state 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 : TM n) : mconfig (state M) n -> bool := fun c => halt (cstate c).

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

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


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


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

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



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

  Definition TerminatesIn {n : nat} (M : TM 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").

  Lemma TerminatesIn_monotone {n : nat} (M : TM 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 : TM 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.

  Definition RealiseIn n (F : Type) (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 : Type) (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 : Type) (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 : Type) (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 : Type) (pM : { M : TM n & state 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; lia. eauto.
    - intros H.
      split.
      + intros t i cout Hc.
        destruct (H t) as (? & ? & ?).
        replace cout with 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 : Type) (pM : pTM F n) R k :
    pM ⊨c(k) R -> pM ⊨ R.
  Proof. now intros (?&?) % Realise_total. Qed.

  Lemma RealiseIn_TerminatesIn n (F : Type) (pM : { M : TM n & state 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 : Type) (pM : pTM F n) R1 R2 :
    Realise pM R2 -> Realise pM R1 -> Realise pM (R1 ∩ R2).
  Proof.
    intros HwR HR t. firstorder.
  Qed.


  Section Canonical_Correctness.
    Variable (n : nat).
    Variable (F : Type).
    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 : TM 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 "'(' M ';' labelling ')'" := (existT (fun x => state x -> _) M labelling).

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


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

Instance inhabited_TM_Q (n : nat) (sig : finType) (M : TM sig n) : inhabitedC (state 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 => once 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).
  Goal let _ := default : state (projT1 pM) in True. Proof. exact I. Qed.
  Goal let _ := default : F in True. Proof. exact I. Qed.
End Test_def.

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

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


Smpl Create TM_Correct.

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


Lemma Vector_map2_ext {A B C} (f g : A -> B -> C) n (v1 : Vector.t A n) (v2 : Vector.t B n) :
  (forall a b, f a b = g a b) ->
  Vector.map2 f v1 v2 = Vector.map2 g v1 v2.
Proof.
  intros H.
  pattern n, v1, v2; revert n v1 v2.
  eapply Vector.rect2.
  - reflexivity.
  - intros n v1 v2 IH a b. cbn. now rewrite H, IH.
Qed.

Lemma TM_eval_iff (Σ : finType) n (M : TM Σ n) q t q' t' :
  TM.eval M q t q' t' <-> exists n, loopM (M := M) (mk_mconfig q t) n = Some (mk_mconfig q' t').
Proof.
  split.
  - induction 1 as [ | q t q' a q'' t' H0 H1 H2 [m IH]].
    + exists 0. cbn. unfold haltConf. cbn. now rewrite H.
    + exists (S m). cbn. unfold haltConf. cbn. rewrite H0.
      unfold step. cbn. unfold current_chars.
      rewrite H1. erewrite Vector_map2_ext.
      * now rewrite IH.
      * intros [] [[] []]; reflexivity.
  - intros [k H].
    induction k in q, t, H, q', t' |- *; cbn in H; unfold haltConf in H; cbn in H.
    + destruct halt eqn:E; inv H. now econstructor.
    + destruct halt eqn:E; inv H.
      * now econstructor.
      * unfold step in H1. cbn in H1.
        destruct trans eqn:E2.
        econstructor; [ eassumption .. | ].
        eapply IHk. erewrite Vector_map2_ext.
        -- now rewrite H1.
        -- intros [] [[] []]; reflexivity.
Qed.