From Coq Require Import FunInd.

From Undecidability Require Import TM.Code.CodeTM.
From Undecidability.TM.Compound Require Export CopySymbols MoveToSymbol.

From Undecidability Require Import TM.Basic.Mono.
From Undecidability Require Import TM.Combinators.Combinators.
From Undecidability Require Import TM.Compound.TMTac TM.Compound.Multi.
From Undecidability Require Import TM.Lifting.LiftAlphabet.

Local Generalizable All Variables.
Set Default Proof Using "Type".

Local Arguments skipn { A } !n !l.
Local Arguments plus : simpl never.
Local Arguments mult : simpl never.

Lemma pair_inv (X Y : Type) (x1 x2 : X) (y1 y2 : Y) :
  (, ) = (, ) = = .
Proof. intros H. now inv H. Qed.


Section Copy.

  Variable sig : finType.
  Variable stop : sig bool.

  Lemma CopySymbols_correct (t : tape sig * tape sig) str1 x str2 :
    ( x, List.In x stop x = false)
    (stop x = true)
    tape_local (fst t) = x ::
    CopySymbols_Fun stop t =
    (midtape (rev left (fst t)) x ,
     midtape (rev left (snd t)) x (skipn (||) (right (snd t)))).
  Proof.
    intros . intros HEnc.
    revert x HEnc .
    functional induction (CopySymbols_Fun stop t); cbn in *; intros.
    - destruct ; cbn in *.
      * rewrite skipn_0.
        pose proof tape_local_current_cons HEnc as HEnc'. assert (s = x) as by congruence. clear HEnc'.
        f_equal. now apply midtape_tape_local_cons.
      * apply tape_local_cons_iff in HEnc as (HEnc'&HEnc). assert (s = ) as by congruence. clear HEnc'.
        specialize ( _ ltac:(eauto)). congruence.
    - destruct ; cbn in *.
      + apply tape_local_cons_iff in HEnc as (HEnc'&HEnc). assert (s = x) as by congruence. clear HEnc'.
        congruence.
      + apply tape_local_cons_iff in HEnc as (HEnc'&HEnc). assert (s = ) as by congruence. clear HEnc'.
        apply (tape_midtape_current_right e) in HEnc. rewrite HEnc in *. cbn in *.
        rewrite !app_assoc. erewrite IHp; eauto. rewrite HEnc. cbn. f_equal.
        * now simpl_tape.
        * f_equal; simpl_tape. reflexivity. now rewrite skipn_tl.
        * now simpl_tape.
    - destruct (current (fst tin)) eqn:E; auto.
      apply tape_local_nil in E. rewrite E in HEnc. now apply app_cons_not_nil in HEnc.
  Qed.


  Corollary CopySymbols_correct_midtape ls m rs x rs' t2 :
    stop m = false
    ( x, List.In x rs stop x = false)
    stop x = true
    CopySymbols_Fun stop (midtape ls m (rs x :: rs'), ) =
    (midtape (rev rs m :: ls) x rs',
     midtape (rev rs m :: left ()) x (skipn (S (|rs|)) (right ))).
  Proof.
    intros HStopM HStopRs HStopX.
    unshelve epose proof @CopySymbols_correct (midtape ls m (rs x :: rs'), ) (m::rs) x rs' _ _ _ as Lmove; cbn in *; eauto.
    - intros ? [|?]; auto.
    - now rewrite !app_assoc in Lmove.
  Qed.


  Corollary CopySymbols_correct_moveright ls m rs x rs' t2:
    ( x, List.In x rs stop x = false)
    stop x = true
    CopySymbols_Fun stop (tape_move_right' ls m (rs x :: rs'), ) =
   (midtape (rev rs m :: ls) x rs',
      midtape (rev rs left ) x (skipn (|rs|) (right ))).
  Proof.
    intros HStopLs HStopX.
    cbv [tape_move_left']. destruct rs as [ | s s'] eqn:E; cbn in *.
    - rewrite CopySymbols_Fun_equation. cbn. rewrite HStopX; cbn. reflexivity.
    - rewrite CopySymbols_correct_midtape; auto. subst. rewrite !app_assoc; cbn. reflexivity.
  Qed.


  Corollary CopySymbols_L_correct t str1 x str2 :
    ( x, List.In x stop x = false)
    (stop x = true)
    tape_local_l (fst t) = x ::
    CopySymbols_L_Fun stop t =
    (midtape x (rev right (fst t)),
     midtape (skipn (||) (left (snd t))) x (rev right (snd t))).
  Proof.
    intros . intros HEnc.
    pose proof @CopySymbols_correct (mirror_tape (fst t), mirror_tape (snd t)) x as Lmove.
    spec_assert Lmove by now (cbn; simpl_tape).
    apply CopySymbols_mirror. rewrite Lmove. unfold mirror_tapes; cbn. f_equal; [ | f_equal]; now simpl_tape.
  Qed.


  Corollary CopySymbols_L_correct_midtape ls ls' m rs x t2 :
    stop m = false
    ( x, List.In x ls stop x = false)
    stop x = true
    CopySymbols_L_Fun stop (midtape (ls x :: ls') m rs, ) =
    (midtape ls' x (rev ls m :: rs),
     midtape (skipn (S (|ls|)) (left )) x (rev ls m :: right )).
  Proof.
    intros HStopM HStopRs HStopX.
    unshelve epose proof @CopySymbols_L_correct (midtape (ls x :: ls') m rs, ) (m::ls) x ls' _ _ _ as Lmove; cbn in *; eauto.
    - intros ? [|?]; auto.
    - now rewrite !app_assoc in Lmove.
  Qed.


  Corollary CopySymbols_L_correct_moveleft ls x ls' m rs t2 :
    ( x, List.In x ls stop x = false)
    stop x = true
    CopySymbols_L_Fun stop (tape_move_left' (ls x :: ls') m rs, ) =
    (midtape ls' x (rev ls m :: rs),
     midtape (skipn (|ls|) (left )) x (rev ls right )).
  Proof.
    intros HStopLs HStopX.
    cbv [tape_move_left']. destruct ls as [ | s s'] eqn:E; cbn in *.
    - rewrite CopySymbols_L_Fun_equation. cbn. rewrite HStopX; cbn. reflexivity.
    - rewrite CopySymbols_L_correct_midtape; auto. subst. rewrite !app_assoc; cbn. reflexivity.
  Qed.


  Variable f : sig sig.
  Lemma CopySymbols_steps_local t r1 sym r2 :
    tape_local t = sym ::
    stop sym = true
    CopySymbols_steps stop t 8 + 8 * length .
  Proof.
    revert t sym . induction ; intros t sym HEnc HStop; cbn -[plus mult] in *.
    - destruct t; cbn in HEnc; inv HEnc. rewrite CopySymbols_steps_equation. cbn. rewrite HStop. cbn. .
    - destruct t; cbn in HEnc; try congruence. inv HEnc.
      rewrite CopySymbols_steps_equation. cbn. destruct (stop a).
      + .
      + apply Nat.add_le_mono_l. replace (8 * S (||)) with (8 + 8 * ||) by .
        eapply ; eauto. cbn. now simpl_tape.
  Qed.


  Corollary CopySymbols_steps_midtape ls m rs x rs' :
    stop x = true
    CopySymbols_steps stop (midtape ls m (rs x :: rs')) 16 + 8 * length rs.
  Proof.
    intros. erewrite CopySymbols_steps_local with ( := m :: rs); cbn -[plus mult]; eauto. .
  Qed.


  Corollary CopySymbols_steps_moveright ls m rs x rs' :
    stop x = true
    CopySymbols_steps stop (tape_move_right' ls m (rs x :: rs')) 8 + 8 * length rs.
  Proof.
    intros HStop. destruct rs as [ | s s'] eqn:E; cbn.
    - rewrite CopySymbols_steps_equation. cbn. rewrite HStop; cbn. .
    - rewrite CopySymbols_steps_midtape; auto. .
  Qed.


  Lemma CopySymbols_L_steps_local t r1 sym r2 :
    tape_local_l t = sym ::
    stop sym = true
    CopySymbols_L_steps stop t 8 + 8 * length .
  Proof.
    revert t sym . induction ; intros t sym HEnc HStop; cbn -[plus mult] in *.
    - destruct t; cbn in HEnc; inv HEnc. rewrite CopySymbols_L_steps_equation. cbn. rewrite HStop. cbn. .
    - destruct t; cbn in HEnc; try congruence. inv HEnc.
      rewrite CopySymbols_L_steps_equation. cbn. destruct (stop a).
      + .
      + apply Nat.add_le_mono_l. replace (8 * S (||)) with (8 + 8 * ||) by .
        eapply ; eauto. cbn. now simpl_tape.
  Qed.


  Corollary CopySymbols_L_steps_midtape ls x ls' m rs :
    stop x = true
    CopySymbols_L_steps stop (midtape (ls x :: ls') m rs) 16 + 8 * length ls.
  Proof.
    intros. erewrite CopySymbols_L_steps_local with ( := m :: ls); cbn -[plus mult]; eauto. .
  Qed.


  Corollary CopySymbols_L_steps_moveleft ls ls' x m rs :
    stop x = true
    CopySymbols_L_steps stop (tape_move_left' (ls x :: ls') m rs) 8 + 8 * length ls.
  Proof.
    intros HStop. destruct ls as [ | s s'] eqn:E; cbn.
    - rewrite CopySymbols_L_steps_equation. cbn. rewrite HStop; cbn. .
    - rewrite CopySymbols_L_steps_midtape; auto. .
  Qed.


End Copy.

Section Move.
  Variable (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig).

  Definition isStop (s: sig^+) := match s with inl STOP true | _ false end.
  Definition isStart (s: sig^+) := match s with inl START true | _ false end.

  Lemma stop_not_in (x : X) (s : (sig^+)) :
    List.In s (map inr (Encode_map _ _ x)) isStop s = false.
  Proof. cbn. intros (?&&?) % in_map_iff. reflexivity. Qed.

  Lemma start_not_in (x : X) (s : (sig^+)) :
    List.In s (map inr (Encode_map _ _ x)) isStart s = false.
  Proof. cbn. intros (?&&?) % in_map_iff. reflexivity. Qed.

  Definition MoveRight := Return (MoveToSymbol isStop id) tt.
  Definition MoveLeft := Return (MoveToSymbol_L isStart id) tt.
  Definition Reset := MoveRight.

  Definition MoveRight_Rel : Rel (tapes (sig^+) 1) (unit * tapes (sig^+) 1) :=
    ignoreParam
      ( tin tout
          (x : X) (s : ),
           tin[@] ≃(;s) x
           tout[@] ≂(;s) x).

  Definition MoveLeft_Rel : Rel (tapes (sig^+) 1) (unit * tapes (sig^+) 1) :=
    ignoreParam
      ( tin tout
          (x : X) (s : ),
           tin[@] ≂(;s) x
           tout[@] ≃(;s) x).

  Definition Reset_size {sigX : Type} {cX : codable sigX X} (x : X) (s : ) := S (size x + s).

  Definition Reset_Rel : Rel (tapes (sig^+) 1) (unit * tapes (sig^+) 1) :=
    ignoreParam
      ( tin tout
          (s : ) (x:X),
           tin[@] ≃(;s) x
           isVoid_size tout[@] (Reset_size x s)).

  Lemma MoveRight_Realise : MoveRight MoveRight_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold MoveRight. TM_Correct. }
    {
      intros tin ((), tout) H. intros x s HEncX.
      TMSimp; clear_trivial_eqs.
      destruct HEncX as (&&Hs).
      erewrite MoveToSymbol_correct_midtape; eauto.
      - repeat econstructor. now rewrite map_id, map_rev. auto.
      - apply stop_not_in.
    }
  Qed.


  Lemma MoveLeft_Realise : MoveLeft MoveLeft_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold MoveLeft. TM_Correct. }
    {
      intros tin ((), tout) H. intros x s HEncX.
      TMSimp; clear_trivial_eqs.
      destruct HEncX as (&&Hs).
      erewrite MoveToSymbol_L_correct_midtape; eauto.
      - repeat econstructor. now rewrite map_id, map_rev, rev_involutive. auto.
      - intros ? (?&&?) % in_map_iff. reflexivity.
    }
  Qed.


  Lemma Reset_Realise : Reset Reset_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Reset. eapply MoveRight_Realise. }
    {
      intros tin ((), tout) H. intros x s HEncX.
      TMSimp. eapply tape_contains_rev_size_isVoid; eauto.
    }
  Qed.


  Definition MoveRight_steps {sigX : Type} (cX : codable sigX X) (x : X) := 8 + 4 *size x.

  Lemma MoveRight_Terminates :
     MoveRight ( tin k x, tin[@] x MoveRight_steps _ x k).
  Proof.
    unfold MoveRight_steps. eapply TerminatesIn_monotone.
    { unfold MoveRight. TM_Correct. }
    {
      intros tin k (x&HEncX&Hk).
      destruct HEncX as (&).
      rewrite MoveToSymbol_steps_midtape; auto. cbn. now simpl_list.
    }
  Qed.


  Definition MoveLeft_steps {sigX : Type} {cX : codable sigX X} (x:X) := 8 + 4 *size x.

  Lemma MoveLeft_Terminates :
     MoveLeft ( tin k x, tin[@] x MoveLeft_steps x k).
  Proof.
    unfold MoveLeft_steps. eapply TerminatesIn_monotone.
    { unfold MoveLeft. TM_Correct. }
    {
      intros tin k (x&HEncX&Hk).
      destruct HEncX as (&).
      rewrite MoveToSymbol_L_steps_midtape; auto. cbn. now rewrite map_length, rev_length, map_length.
    }
  Qed.


  Definition Reset_steps {sigX : Type} {cX : codable sigX X} (x:X) := 8 + 4 *size x.

  Definition Reset_Terminates :
     Reset ( tin k x, tin[@] x Reset_steps x k).
  Proof. exact MoveRight_Terminates. Qed.

  Definition ResetEmpty : pTM sig^+ unit 1 := Move Rmove.

  Definition ResetEmpty_size : := S.

  Definition ResetEmpty_Rel : pRel sig^+ unit 1 :=
    ignoreParam (
         tin tout
           (s : ) (x : X),
            tin[@] ≃(;s) x
            cX x = nil
            isVoid_size tout[@] (ResetEmpty_size s)
        ).

  Definition ResetEmpty_steps := 1.

  Lemma ResetEmpty_Sem : ResetEmpty c(ResetEmpty_steps) ResetEmpty_Rel.
  Proof.
    eapply RealiseIn_monotone.
    { unfold ResetEmpty. TM_Correct. }
    { reflexivity. }
    {
      intros tin ((), tout) H. cbn. intros s x HEncX HCod.
      unfold ResetEmpty_size in *.
      destruct HEncX as (ls&HEncX). TMSimp; clear_trivial_eqs. rewrite HCod;cbn.
      hnf. do 2 eexists. split. f_equal. cbn. .
    }
  Qed.


  Definition : pTM sig^+ (FinType(EqType unit)) 1 := Move Rmove;; Move Rmove.

  Definition ResetEmpty1_size : := S >> S.

  Definition ResetEmpty1_Rel : pRel sig^+ (FinType(EqType unit)) 1 :=
    ignoreParam (
         tin tout
           (x : X) (s : ),
            tin[@] ≃(;s) x
           size x = 1
            isVoid_size tout[@] (ResetEmpty1_size s)).

  Definition ResetEmpty1_steps := 3.

  Lemma ResetEmpty1_Sem : c(ResetEmpty1_steps) ResetEmpty1_Rel.
  Proof.
    eapply RealiseIn_monotone.
    { unfold . TM_Correct. }
    { reflexivity. }
    {
      intros tin ((), tout) H. cbn. intros x s HEncX HCod.
      unfold ResetEmpty1_size in *.
      destruct HEncX as (ls&HEncX). unfold size in *. TMSimp; clear_trivial_eqs.
      destruct (cX x); cbn in *; inv HCod. destruct l; cbn in *; inv .
      hnf. do 2 eexists. split. f_equal. cbn. .
    }
  Qed.


End Move.

Arguments Reset_size {X sigX cX} : simpl never.
Arguments Reset_steps {X sigX cX} : simpl never.
Typeclasses Opaque Reset_size.
Typeclasses Opaque Reset_steps.

Section CopyValue.
  Variable (sig: finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig).

  Definition CopyValue :=
    LiftTapes (MoveRight _) [||];; CopySymbols_L (@isStart sig).

  Definition CopyValue_size {sig: Type} {cX : codable sig X} (x : X) (s1 : ) := - S (size x).

  Definition CopyValue_Rel : Rel (tapes (sig^+) 2) (unit * tapes (sig^+) 2) :=
    ignoreParam (
         tin tout
           (x:X) (sx s1 : ),
            tin[@] ≃(;sx) x
            isVoid_size tin[@]
            tout[@] ≃(;sx) x
            tout[@] ≃(;CopyValue_size x ) x
      ).

  Lemma CopyValue_Realise : CopyValue CopyValue_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold CopyValue. TM_Correct. eapply MoveRight_Realise with (X := X). }
    {
      intros tin ((), tout) H.
      intros x sx HEncX HRight.
      TMSimp. rename H into HMoveRight, into HCopy.
      specialize HMoveRight with (1 := HEncX).

      destruct HMoveRight as (rx&HMoveRight&Hsx). destruct HRight as (&&HRight&). TMSimp.
      erewrite CopySymbols_L_correct_midtape in HCopy; eauto.
      - apply pair_inv in HCopy as (&). TMSimp. split.
        + hnf. eexists. rewrite map_rev, rev_involutive. split. f_equal. auto.
        + hnf. eexists. rewrite map_rev, rev_involutive. split. f_equal.
          simpl_list. rewrite skipn_length. cbn. unfold CopyValue_size, size. .
      - now intros ? (?&&?) % in_map_iff.
    }
  Qed.


  Definition CopyValue_steps {sig:Type} {cX : codable sig X} (x:X) := 25 + 12 *size x.

  Lemma CopyValue_Terminates :
     CopyValue ( tin k x:X, tin[@] x CopyValue_steps x k).
  Proof.
    unfold CopyValue_steps. eapply TerminatesIn_monotone.
    { unfold CopyValue. TM_Correct.
      - eapply MoveRight_Realise.
      - eapply MoveRight_Terminates. }
    {
      intros tin k (x&HEncX&Hk).
      exists (8 + 4 * length (Encode_map _ _ x : list sig)), (16 + 8 * length (Encode_map _ _ x : list sig)). repeat split; cbn; eauto.
      - exists x. split. auto. unfold MoveRight_steps, size. now rewrite map_length.
      - unfold size in *. rewrite !map_length. .
      - intros tmid () (&HInj). TMSimp.
        apply tape_contains_contains_size in HEncX.
        specialize with (1 := HEncX).
        destruct as (&&). TMSimp.
        rewrite CopySymbols_L_steps_midtape; eauto.
        now rewrite map_length, rev_length, map_length.
    }
  Qed.


End CopyValue.

Arguments CopyValue_size {X sig cX} : simpl never.
Arguments CopyValue_steps {X sig cX} : simpl never.
Typeclasses Opaque CopyValue_size.
Typeclasses Opaque CopyValue_steps.

Section MoveValue.
  Variable sig : finType.
  Variable (sigX sigY X Y : Type) (cX : codable sigX X) (cY : codable sigY Y) ( : Retract sigX sig) ( : Retract sigY sig).

  Definition MoveValue : pTM sig^+ unit 2 :=
    LiftTapes (Reset _) [||];;
    CopyValue _;;
    LiftTapes (Reset _) [||].

  Definition MoveValue_size_x {sigX : Type} {cX : codable sigX X} (x : X) (sx : ) := S (size x + sx).
  Definition MoveValue_size_y {sigX sigY : Type} {cX : codable sigX X} {cY : codable sigY Y} (x : X) (y : Y) (sy : ) := sy + size cY y -size x.

  Definition MoveValue_Rel : pRel sig^+ unit 2 :=
    ignoreParam (
         tin tout
           (x : X) (y : Y) (sx sy : ),
            tin[@] ≃(;sx) x
            tin[@] ≃(;sy) y
            isVoid_size tout[@] (MoveValue_size_x x sx)
            tout[@] ≃(;MoveValue_size_y x y sy) x).

  Lemma MoveValue_Realise : MoveValue MoveValue_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold MoveValue. TM_Correct.
      - apply Reset_Realise with (X := Y).
      - apply CopyValue_Realise with (X := X).
      - apply Reset_Realise with (X := X).
    }
    {
      intros tin ((), tout) H. cbn. intros x y sx sy HEncX HEncY.
      TMSimp. unfold MoveValue_size_x, MoveValue_size_y, CopyValue_size, Reset_size in *.
      specialize H with (1 := HEncY).
      specialize with (1 := HEncX) (2 := H) as (&).
      specialize with (1 := ).
      repeat split; auto.
    }
  Qed.


  Definition MoveValue_steps {sigX sigY:Type} {cX : codable sigX X} {cY : codable sigY Y} (x:X) (y:Y) := 43 + 16 *size x + 4 * size cY y.

  Lemma MoveValue_Terminates :
     MoveValue ( tin k (x : X) (y : Y), tin[@] x tin[@] y MoveValue_steps x y k).
  Proof.
    unfold MoveValue_steps. eapply TerminatesIn_monotone.
    { unfold MoveValue. TM_Correct.
      - apply Reset_Realise with (X := Y).
      - apply Reset_Terminates with (X := Y).
      - apply CopyValue_Realise with (X := X).
      - apply CopyValue_Terminates with (X := X).
      - apply Reset_Terminates with (X := X).
    }
    {
      intros tin k (x&y&HEncX&HEncY&Hk).
      exists (8 + 4 * length (cY y)), (34 + 16 * length (cX x)). repeat split; cbn; eauto.
      - unfold size in *. .
      - intros () (&). TMSimp.
        apply tape_contains_contains_size in HEncX; apply tape_contains_contains_size in HEncY.
        specialize with (1 := HEncY).
        exists (25 + 12 * length (cX x)), (8 + 4 * length (cX x)). repeat split; cbn; eauto.
        + .
        + intros tmid2_ () .
          specialize with (1 := HEncX) (2 := ) as (&).
          exists x. split; eauto.
    }
  Qed.


End MoveValue.

Arguments MoveValue_size_x {X sigX cX} : simpl never.
Arguments MoveValue_size_y {X Y sigX sigY cX cY} : simpl never.
Arguments MoveValue_steps {X Y sigX sigY cX cY} : simpl never.
Typeclasses Opaque MoveValue_size_x MoveValue_size_y.
Typeclasses Opaque MoveValue_steps.

Section Translate.

  Variable (sig : finType).
  Variable (sigX X : Type) (cX : codable sigX X).
  Variable ( : Retract sigX sig).

  Definition translate : sig^+ sig^+ :=
     t match t with
          | inl _ t
          | inr x match Retr_g (Retract := ) x with
                    | Some y inr (Retr_f (Retract := ) y)
                    | None inl UNKNOWN
                    end
          end.

  Definition Translate' := MoveToSymbol (@isStop sig) translate.

  Definition : pRel sig^+ unit 1 :=
    ignoreParam (
         tin tout
           (x : X) (s : ),
            tin[@] ≃(; s) x
            tout[@] ≂(; s) x
      ).

  Lemma Translate'_Realise : Translate' .
  Proof.
    eapply Realise_monotone.
    { unfold Translate'. TM_Correct. }
    {
      intros tin ((), tout) H. intros x s HEncX.
      destruct HEncX as (ls&HEncX&Hs). TMSimp.
      rewrite MoveToSymbol_correct_midtape; cbn; auto.
      - repeat econstructor. cbn. f_equal. f_equal. rewrite map_rev, !List.map_map. f_equal.
        apply List.map_ext. cbn. intros. now retract_adjoint. auto.
      - rewrite List.map_map. now intros ? (?&&?) % in_map_iff.
    }
  Qed.


  Definition {sigX X : Type} {cX : codable sigX X} (x:X) := 8 + 4 *size x.

  Lemma Translate'_Terminates :
     Translate' ( tin k x, tin[@] ≃() x (cX:=cX) x k).
  Proof.
    eapply TerminatesIn_monotone.
    { unfold Translate'. TM_Correct. }
    {
      intros tin k (x&HEncX&Hk). unfold size in *.
      destruct HEncX as (&).
      rewrite MoveToSymbol_steps_midtape; auto. cbn. now rewrite !map_length.
    }
  Qed.


  Definition Translate := Translate';; MoveLeft _.

  Definition Translate_Rel : pRel sig^+ unit 1 :=
    ignoreParam (
         tin tout
           (x : X) (s : ),
            tin[@] ≃(; s) x
            tout[@] ≃(; s) x
      ).

  Lemma Translate_Realise : Translate Translate_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Translate. TM_Correct.
      - apply Translate'_Realise.
      - apply MoveLeft_Realise with (I := ) (cX:=cX).
    }
    {
      intros tin ((), tout) H. intros x s HEncX.
      TMSimp. apply . apply H. apply HEncX.
    }
  Qed.


  Definition Translate_steps {sigX:Type} {cX : codable sigX X} (x : X) := 17 + 8 *size x.

  Definition Translate_T : tRel sig^+ 1 :=
     tin k x, tin[@] ≃() x Translate_steps x k.

  Lemma Translate_Terminates :
     Translate Translate_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold Translate. TM_Correct.
      - apply Translate'_Realise.
      - apply Translate'_Terminates.
      - eapply MoveLeft_Terminates.
    }
    {
      intros tin k (x&HEncX&Hk). unfold Translate_steps in *.
      exists (8 + 4 *size x), (8 + 4 *size x). repeat split; try .
      eexists. repeat split; eauto.
      intros tmid () H. cbn in H.
      apply tape_contains_contains_size in HEncX.
      specialize H with (1 := HEncX).
      exists x. split. eauto. unfold MoveLeft_steps. .
    }
  Qed.


End Translate.

Arguments Translate_steps {X sigX cX}.

Ltac smpl_TM_Copy :=
  once lazymatch goal with
  | [ |- Translate _ _ _] notypeclasses refine (@Translate_Realise _ _ _ _ _ _);shelve
  | [ |- (Translate _ _) _] notypeclasses refine (@Translate_Terminates _ _ _ _ _ _);shelve
  | [ |- Reset _ _] notypeclasses refine (@Reset_Realise _ _ _ _ _);shelve
  | [ |- (Reset _) _] notypeclasses refine (@Reset_Terminates _ _ _ _ _);shelve
  | [ |- CopyValue _ _] notypeclasses refine (@CopyValue_Realise _ _ _ _ _);shelve
  | [ |- (CopyValue _) _] notypeclasses refine (@CopyValue_Terminates _ _ _ _ _);shelve
  | [ |- MoveValue _ _] notypeclasses refine (@MoveValue_Realise _ _ _ _ _ _ _ _ _);shelve
  | [ |- (MoveValue _) _] notypeclasses refine (@MoveValue_Terminates _ _ _ _ _ _ _ _ _);shelve
  end.

Smpl Add smpl_TM_Copy : TM_Correct.

From Undecidability.TM.Hoare Require Import HoareLogic HoareRegister HoareTactics.


Definition CopyValue_sizefun {sigX X : Type} {cX : codable sigX X} (x : X) : Vector.t () 2 := [|id; CopyValue_size x|].

Lemma CopyValue_SpecT_size (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) (ss : Vector.t 2) :
  TripleT (≃≃([],withSpace [|Contains _ x; Void|] ss))
          (CopyValue_steps x) (CopyValue sig)
          ( _ ≃≃([],withSpace [|Contains _ x; Contains _ x|] (appSize (CopyValue_sizefun x) ss))).
Proof.
  eapply Realise_TripleT.
  - eapply CopyValue_Realise.
  - eapply CopyValue_Terminates.
  - intros tin [] tout H HEnc. unfold withSpace in *|-. cbn in *.
    specialize (HEnc ) as ; specialize (HEnc ) as .
    cbn in *; simpl_vector in *; cbn in *.
    modpon H. tspec_solve.
  - intros tin k HEnc. cbn in *. unfold withSpace in *.
    specialize (HEnc ) as ; specialize (HEnc ) as .
    cbn in *; simpl_vector in *; cbn in *. eauto.
Qed.


Lemma CopyValue_SpecT (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
  TripleT (≃≃([],[|Contains _ x; Void|])) (CopyValue_steps x) (CopyValue sig) ( _ ≃≃([],[|Contains _ x; Contains _ x|])).
Proof. eapply TripleT_RemoveSpace. cbn. intros s. apply CopyValue_SpecT_size. Qed.

Lemma CopyValue_Spec_size (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) (ss : Vector.t 2) :
  Triple (≃≃(([], withSpace [|Contains _ x; Void|] ss)))
         (CopyValue sig)
         ( _ ≃≃(([], withSpace [|Contains _ x; Contains _ x|] (appSize (CopyValue_sizefun x) ss)))).
Proof. eapply TripleT_Triple. apply CopyValue_SpecT_size. Qed.

Lemma CopyValue_Spec (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
  Triple (≃≃([], [|Contains _ x; Void|]))
         (CopyValue sig)
         ( _ ≃≃([], [|Contains _ x; Contains _ x|])).
Proof. eapply Triple_RemoveSpace. apply CopyValue_Spec_size. Qed.

Lemma Reset_SpecT_space (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) (ss : Vector.t 1) :
  TripleT (≃≃([], withSpace [|Contains _ x |] ss)) (Reset_steps x) (Reset sig) ( _ ≃≃(([], withSpace [|Void|] (appSize [|Reset_size x|] ss)))).
Proof.
  eapply Realise_TripleT.
  - eapply Reset_Realise.
  - eapply Reset_Terminates.
  - intros tin [] tout H HEnc. unfold withSpace in *. cbn in *.
    specialize (HEnc ); cbn in *. simpl_vector in *; cbn in *.
    modpon H.
    tspec_solve.
  - intros tin k HEnc. unfold withSpace in *. cbn in *.
    specialize (HEnc ). simpl_vector in *; cbn in *. eauto.
Qed.


Lemma Reset_SpecT (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
  TripleT (≃≃([], [|Contains _ x|])) (Reset_steps x) (Reset sig) ( _ ≃≃([], [|Void|])).
Proof. eapply TripleT_RemoveSpace. apply Reset_SpecT_space. Qed.

Lemma Reset_Spec_size (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) ss :
  Triple (≃≃(([], withSpace [|Contains _ x |] ss))) (Reset sig) ( _ ≃≃(([], withSpace [|Void|] (appSize [|Reset_size x|] ss)))).
Proof. eapply TripleT_Triple. apply Reset_SpecT_space. Qed.

Lemma Reset_Spec (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
  Triple (≃≃([], [|Contains _ x|])) (Reset sig) ( _ ≃≃([], [|Void|])).
Proof. eapply TripleT_Triple. apply Reset_SpecT. Qed.

Lemma ResetEmpty_SpecT_space (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) (ss : Vector.t 1) :
  cX x = []
  TripleT (≃≃(([], withSpace [|Contains _ x |] ss))) (ResetEmpty_steps) (ResetEmpty sig) ( _ ≃≃(([], withSpace [|Void|] (appSize [|ResetEmpty_size|] ss)))).
Proof.
  intros HEncEmpty. eapply RealiseIn_TripleT.
  - eapply ResetEmpty_Sem.
  - intros tin [] tout H HEnc. unfold withSpace in *. cbn in *.
    specialize (HEnc ); cbn in *. simpl_vector in *; cbn in *.
    modpon H. tspec_solve.
Qed.


Lemma ResetEmpty_SpecT (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
  cX x = []
  TripleT (≃≃([], [|Contains _ x|])) (ResetEmpty_steps) (ResetEmpty sig) ( _ ≃≃([], [|Void|])).
Proof. intros. eapply TripleT_RemoveSpace. intros. now apply ResetEmpty_SpecT_space. Qed.

Lemma ResetEmpty_Spec_size (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) ss :
  cX x = []
  Triple (≃≃(([], withSpace [|Contains _ x |] ss))) (ResetEmpty sig) ( _ ≃≃(([], withSpace [|Void|] (appSize [|ResetEmpty_size|] ss)))).
Proof. intros. eapply TripleT_Triple. now apply ResetEmpty_SpecT_space. Qed.

Lemma ResetEmpty_Spec (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
  cX x = []
  Triple (≃≃([], [|Contains _ x|])) (ResetEmpty sig) ( _ ≃≃([], [|Void|])).
Proof. intros. eapply TripleT_Triple. now apply ResetEmpty_SpecT. Qed.

Lemma ResetEmpty1_SpecT_space (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) (ss : Vector.t 1) :
 size x = 1
  TripleT (≃≃(([], withSpace [|Contains _ x |] ss))) (ResetEmpty1_steps) ( sig) ( _ ≃≃(([], withSpace [|Void|] (appSize [|ResetEmpty1_size|] ss)))).
Proof.
  intros HEncEmpty. eapply RealiseIn_TripleT.
  - eapply ResetEmpty1_Sem.
  - intros tin [] tout H HEnc. cbn in *. unfold withSpace in *.
    specialize (HEnc ); cbn in *. simpl_vector in *; cbn in *.
    modpon H. tspec_solve.
Qed.


Lemma ResetEmpty1_SpecT (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
 size x = 1
  TripleT (≃≃([], [|Contains _ x|])) (ResetEmpty1_steps) ( sig) ( _ ≃≃([], [|Void|])).
Proof. intros. eapply TripleT_RemoveSpace. intros. now apply ResetEmpty1_SpecT_space. Qed.

Lemma ResetEmpty1_Spec_size (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) ss :
 size x = 1
  Triple (≃≃(([], withSpace [|Contains _ x |] ss))) ( sig) ( _ ≃≃(([], withSpace [|Void|] (appSize [|ResetEmpty1_size|] ss)))).
Proof. intros. eapply TripleT_Triple. now apply ResetEmpty1_SpecT_space. Qed.

Lemma ResetEmpty1_Spec (sig : finType) (sigX X : Type) (cX : codable sigX X) (I : Retract sigX sig) (x : X) :
 size x = 1
  Triple (≃≃([], [|Contains _ x|])) ( sig) ( _ ≃≃([], [|Void|])).
Proof. intros. eapply TripleT_Triple. now apply ResetEmpty1_SpecT. Qed.

Definition MoveValue_size {X Y sigX sigY : Type} {cX : codable sigX X} {cY : codable sigY Y} (x : X) (y : Y) : Vector.t () 2 :=
  [|MoveValue_size_x x; MoveValue_size_y x y|].

Lemma MoveValue_SpecT_size (sig : finType) (sigX sigY X Y : Type)
      (cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) (ss : Vector.t 2) :
  TripleT (≃≃(([], withSpace [|Contains _ x; Contains _ y |] ss))) (MoveValue_steps x y) (MoveValue sig)
          ( _ ≃≃(([], withSpace [|Void; Contains _ x|] (appSize (MoveValue_size x y) ss)))).
Proof. unfold withSpace.
  eapply Realise_TripleT.
  - apply MoveValue_Realise with (X := X) (Y := Y).
  - apply MoveValue_Terminates with (X := X) (Y := Y).
  - intros tin [] tout H HEnc. cbn in *.
    specialize (HEnc ) as ; specialize (HEnc ) as . simpl_vector in *; cbn in *.
    modpon H. tspec_solve.
  - intros tin k HEnc. cbn in *.
    specialize (HEnc ) as ; specialize (HEnc ) as . simpl_vector in *; cbn in *. eauto.
Qed.


Lemma MoveValue_SpecT (sig : finType) (sigX sigY X Y : Type)
      (cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) :
  TripleT (≃≃([], [|Contains _ x; Contains _ y|])) (MoveValue_steps x y) (MoveValue sig) ( _ ≃≃([], [|Void; Contains _ x|])).
Proof. eapply TripleT_RemoveSpace. apply MoveValue_SpecT_size. Qed.

Lemma MoveValue_Spec_size (sig : finType) (sigX sigY X Y : Type)
      (cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) (ss : Vector.t 2) :
  Triple (≃≃(([], withSpace [|Contains _ x; Contains _ y |] ss))) (MoveValue sig)
         ( _ ≃≃(([], withSpace [|Void; Contains _ x|] (appSize (MoveValue_size x y) ss)))).
Proof. eapply TripleT_Triple. apply MoveValue_SpecT_size. Qed.

Lemma MoveValue_Spec (sig : finType) (sigX sigY X Y : Type)
      (cX : codable sigX X) (cY : codable sigY Y) (I1 : Retract sigX sig) (I2 : Retract sigY sig) (x : X) (y : Y) :
  Triple (≃≃([], [|Contains _ x; Contains _ y|])) (MoveValue sig) ( _ ≃≃([], [|Void; Contains _ x|])).
Proof. eapply TripleT_Triple. apply MoveValue_SpecT. Qed.

Lemma Translate_SpecT_size (sig : finType) (sigX X : Type)
      (cX : codable sigX X) (I1 I2 : Retract sigX sig) (x : X) (ss : Vector.t 1) :
  TripleT (≃≃(([], withSpace [|Contains x |] ss))) (Translate_steps x) (Translate )
          ( _ ≃≃(([], withSpace [|Contains x|] (appSize [|id|] ss)))).
Proof. unfold withSpace.
  eapply Realise_TripleT.
  - apply Translate_Realise with (X := X).
  - apply Translate_Terminates with (X := X).
  - intros tin [] tout H HEnc. cbn in *.
    specialize (HEnc ) as ; simpl_vector in *; cbn in *.
    modpon H. tspec_solve.
  - intros tin k HEnc Hk. cbn in *.
    specialize (HEnc ) as . simpl_vector in *; cbn in *. unfold Translate_T. eauto.
Qed.


Lemma Translate_SpecT (sig : finType) (sigX X : Type)
      (cX : codable sigX X) (I1 I2 : Retract sigX sig) (x : X) :
  TripleT (≃≃([], [|Contains x|])) (Translate_steps x) (Translate )
          ( _ ≃≃([], [|Contains x|])).
Proof. eapply TripleT_RemoveSpace. apply Translate_SpecT_size. Qed.

Lemma Translate_Spec_size (sig : finType) (sigX X : Type)
      (cX : codable sigX X) (I1 I2 : Retract sigX sig) (x : X) (ss : Vector.t 1) :
  Triple (≃≃(([], withSpace [|Contains x |] ss))) (Translate )
         ( _ ≃≃(([], withSpace [|Contains x|] (appSize [|id|] ss)))).
Proof. eapply TripleT_Triple. apply Translate_SpecT_size. Qed.

Lemma Translate_Spec (sig : finType) (sigX X : Type)
      (cX : codable sigX X) (I1 I2 : Retract sigX sig) (x : X) :
  Triple (≃≃([], [|Contains x|])) (Translate )
         ( _ ≃≃([], [|Contains x|])).
Proof. eapply TripleT_Triple. apply Translate_SpecT. Qed.

Ltac hstep_Reset :=
  lazymatch goal with
  | [ |- TripleT ?P ?k (CopyValue _) ?Q ] notypeclasses refine (CopyValue_SpecT_size _ _ _ _)
  | [ |- TripleT ?P ?k (Reset _) ?Q ] eapply @Reset_SpecT_space
  | [ |- TripleT ?P ?k (ResetEmpty _) ?Q ] eapply @ResetEmpty_SpecT_space
  | [ |- TripleT ?P ?k ( _) ?Q ] eapply @ResetEmpty1_SpecT_space
  | [ |- TripleT ?P ?k (MoveValue _) ?Q ] eapply @MoveValue_SpecT_size
  | [ |- TripleT ?P ?k (Translate _ _) ?Q ] eapply @Translate_SpecT_size
  end.

Smpl Add hstep_Reset : hstep_Spec.