From Undecidability Require Import TM.Util.Prelim.
From Undecidability Require Import TM.Util.TM_facts.
From Undecidability Require Import TM.Basic.Basic.
From Undecidability Require Import TM.Combinators.Combinators.
From Undecidability Require Import TM.Lifting.Lifting.

From Undecidability Require Import TM.Compound.TMTac.

Set Default Proof Using "Type".



Section Nop.
  Variable sig : finType.
  Variable n : .

  Definition Nop : pTM sig unit n := LiftTapes Null (Vector.nil _).

  Definition Nop_Rel : pRel sig unit n :=
    ignoreParam ( t t' t' = t).

  Lemma Nop_Sem : Nop c(0) Nop_Rel.
  Proof.
    eapply RealiseIn_monotone.
    { unfold Nop. TM_Correct. }
    { reflexivity. }
    {
      intros tin ((), tout) (_&HInj). cbn in *.
      apply Vector.eq_nth_iff; intros i ? . apply HInj. vector_not_in.
    }
  Qed.

End Nop.

Arguments Nop_Rel {sig n} x y/.
Arguments Nop {sig n}.
Arguments Nop : simpl never.


Section Diverge.
  Variable sig : finType.
  Variable n : .

  Definition Diverge : pTM sig unit n := While (Return Nop None).

  Definition Diverge_Rel : pRel sig unit n :=
    ignoreParam ( t t' False).

  Lemma Diverge_Realise : Diverge Diverge_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Diverge. TM_Correct. eapply RealiseIn_Realise. apply Nop_Sem. }
    { eapply WhileInduction; intros; cbn in *; TMSimp; auto. }
  Qed.


End Diverge.

Arguments Diverge_Rel {sig n} x y/.
Arguments Diverge {sig n}.
Arguments Diverge : simpl never.


Section MovePar.
  Variable sig : finType.
  Variable ( : move).

  Definition MovePar_R : pRel sig unit 2 :=
    ignoreParam( (t t' : tapes sig 2)
                  t'[@] = tape_move t[@]
                  t'[@] = tape_move t[@] ).

  Definition MovePar : pTM sig unit 2 :=
    LiftTapes (Move ) [||];; LiftTapes (Move ) [||].


  Lemma MovePar_Sem : MovePar c(3) MovePar_R.
  Proof.
    eapply RealiseIn_monotone.
    { unfold MovePar. TM_Correct. }
    { reflexivity. }
    { hnf in *. intros tin (yout&tout) H. now TMSimp. }
  Qed.


End MovePar.

Arguments MovePar_R { sig } ( ) x y /.
Arguments MovePar {sig} ( ).
Arguments MovePar : simpl never.


Section Copy.
  Variable sig : finType.

  Variable f : sig sig.

  Definition CopyChar : pTM sig unit 2 :=
    Switch (LiftTapes ReadChar [||])
          ( s : option sig
             match s with
             | None Nop
             | Some s LiftTapes (Write (f s)) [||]
             end).

  Definition CopyChar_Rel : pRel sig unit 2 :=
    ignoreParam (
         tin tout
          tout[@] = tin[@]
          tout[@] = tape_write tin[@] (map_opt f (current tin[@]))
      ).

  Lemma CopyChar_Sem : CopyChar c(3) CopyChar_Rel.
  Proof.
    eapply RealiseIn_monotone.
    {
      unfold CopyChar. eapply Switch_RealiseIn; cbn.
      - apply LiftTapes_RealiseIn. vector_dupfree. apply ReadChar_Sem.
      - instantiate (2 := o : option sig match o with Some s _ | None _ end).
        intros [ s | ]; cbn.
        + eapply LiftTapes_RealiseIn. vector_dupfree. apply Write_Sem.
        + eapply RealiseIn_monotone'. apply Nop_Sem. .
    }
    { . }
    {
      intros tin ((), tout) H. cbn in *. TMSimp.
      destruct (current _) eqn:E; TMSimp; auto.
    }
  Qed.


End Copy.

Arguments CopyChar_Rel { sig } ( f ) x y /.
Arguments CopyChar { sig }.
Arguments CopyChar : simpl never.


Section ReadChar.

  Variable sig : finType.
  Variable (n : ) (k : Fin.t n).

  Definition ReadChar_at : pTM sig (option sig) n :=
    LiftTapes ReadChar [|k|].

  Definition ReadChar_at_Rel : pRel sig (option sig) n :=
     tin '(yout, tout)
      yout = current tin[@k]
      tout = tin.

  Lemma ReadChar_at_Sem :
    ReadChar_at c(1) ReadChar_at_Rel.
  Proof.
    eapply RealiseIn_monotone.
    { unfold ReadChar_at. TM_Correct. }
    { cbn. reflexivity. }
    {
      intros tin (yout, tout) H.
      hnf. TMSimp; clear_trivial_eqs. split; auto.
      eapply VectorSpec.eq_nth_iff; intros p ? .
      decide (p = k) as [|HnEq]; TMSimp; auto.
      - apply . vector_not_in.
    }
  Qed.


End ReadChar.

Arguments ReadChar_at : simpl never.
Arguments ReadChar_at {sig n} k.
Arguments ReadChar_at_Rel { sig n } ( k ) x y /.


Ltac smpl_TM_Multi :=
  once lazymatch goal with
  | [ |- Nop _ ] eapply RealiseIn_Realise; apply Nop_Sem
  | [ |- Nop c(_) _ ] eapply Nop_Sem
  | [ |- (Nop) _ ] eapply RealiseIn_TerminatesIn; apply Nop_Sem

  | [ |- Diverge _ ] apply Diverge_Realise

  | [ |- MovePar _ _ _ ] eapply RealiseIn_Realise; eapply MovePar_Sem
  | [ |- MovePar _ _ c(_) _ ] eapply MovePar_Sem
  | [ |- (MovePar _ _) _ ] eapply RealiseIn_TerminatesIn; eapply MovePar_Sem

  | [ |- CopyChar _ _ ] eapply RealiseIn_Realise; eapply CopyChar_Sem
  | [ |- CopyChar _ c(_) _ ] eapply CopyChar_Sem
  | [ |- (CopyChar _) _ ] eapply RealiseIn_TerminatesIn; eapply CopyChar_Sem

  | [ |- ReadChar_at _ _ ] eapply RealiseIn_Realise; eapply ReadChar_at_Sem
  | [ |- ReadChar_at _ c(_) _ ] eapply ReadChar_at_Sem
  | [ |- (ReadChar_at _) _ ] eapply RealiseIn_TerminatesIn; eapply ReadChar_at_Sem
  end.

Smpl Add smpl_TM_Multi : TM_Correct.