From Undecidability Require Import TM.Util.TM_facts TM.Basic.Mono TM.Combinators.Combinators TM.Compound.Multi.
Require Import List.
From Undecidability Require Import TMTac.
From Coq Require Import List.

Set Default Goal Selector "!".

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

Section Write_String.

  Variable sig : finType.
  Variable D : move.

  Fixpoint WriteString (l : list sig) : pTM sig unit 1 :=
    match l with
    | [] => Nop
    | [x] => Write x
    | x :: xs => WriteMove x D;; WriteString xs
    end.

  Fixpoint WriteString_Fun (sig' : Type) (t : tape sig') (str : list sig') :=
    match str with
    | nil => t
    | [x] => tape_write t (Some x)
    | x :: str' => WriteString_Fun (doAct t (Some x, D)) str'
    end.

  Lemma WriteString_Fun_eq (sig' : Type) (t : tape sig') (str : list sig') :
    WriteString_Fun t str =
    match str with
    | nil => t
    | [x] => tape_write t (Some x)
    | x :: str' => WriteString_Fun (doAct t (Some x, D)) str'
    end.
  Proof. destruct str; auto. Qed.

  Lemma Write_String_nil (sig' : Type) (t : tape sig') :
    WriteString_Fun t nil = t.
  Proof. destruct t; cbn; auto. Qed.

  Fixpoint WriteString_sem_fix (str : list sig) : pRel sig unit 1 :=
    match str with
    | nil => Nop_Rel
    | [x] => Write_Rel x
    | x :: str' =>
      WriteMove_Rel x D |_tt ∘ WriteString_sem_fix str'
    end.

  Definition WriteString_steps l :=
    2 * l - 1.

  Lemma WriteString_fix_Sem (str : list sig) :
    WriteString str ⊨c(WriteString_steps (length str)) (WriteString_sem_fix str).
  Proof.
    induction str as [ | s [ | s' str'] IH ].
    - apply Nop_Sem.
    - apply Write_Sem.
    - change (WriteString (s :: s' :: str')) with (WriteMove s D;; WriteString (s' :: str')).
      eapply RealiseIn_monotone.
      { apply Seq_RealiseIn.
        - apply WriteMove_Sem.
        - apply IH. }
      { unfold WriteString_steps. cbn. lia. }
      { intros t1 t3 H. destruct H as (()&t2&H1&H2).
        change (WriteString_sem_fix (s :: s' :: str')) with (WriteMove_Rel s D |_tt ∘ WriteString_sem_fix (s' :: str')).
        exists t2. split; auto.
      }
  Qed.

  Definition WriteString_Rel str : Rel (tapes sig 1) (unit * tapes sig 1) :=
    Mono.Mk_R_p (ignoreParam (fun tin tout => tout = WriteString_Fun tin str)).

  Lemma WriteString_Sem str :
    WriteString str ⊨c(WriteString_steps (length str)) (WriteString_Rel str).
  Proof.
    eapply RealiseIn_monotone.
    { apply WriteString_fix_Sem. }
    { reflexivity. }
    { induction str as [ | s [ | s' str'] IH]; intros tin (yout, tout) H.
      - cbn. now TMSimp.
      - cbn. now TMSimp.
      - change (WriteString_sem_fix (s :: s' :: str')) with ((WriteMove_Rel s D |_tt ∘ WriteString_sem_fix (s' :: str'))) in H.
        destruct H as (tmid&H1&H2). hnf in H1. apply IH in H2.
        now TMSimp.
    }
  Qed.

End Write_String.

Arguments WriteString : simpl never.
Arguments WriteString_Rel {sig} (D) (str) x y/.

#[export] Hint Extern 1 (WriteString _ _ ⊨ _) => eapply RealiseIn_Realise; eapply WriteString_Sem : TMdb.
#[export] Hint Extern 1 (WriteString _ _ ⊨c(_) _) => eapply WriteString_Sem : TMdb.
#[export] Hint Extern 1 (projT1 (WriteString _ _) ↓ _) => eapply RealiseIn_TerminatesIn; eapply WriteString_Sem : TMdb.