From Undecidability Require Import TM.Util.Prelim.
From Undecidability Require Import TM.Basic.Mono.
From Undecidability Require Import TM.Combinators.Combinators.
From Undecidability Require Import TM.Compound.TMTac.
From Undecidability Require Import TM.Compound.Multi.

From Undecidability Require Import ArithPrelim.

From Coq Require Import FunInd.
From Coq Require Import Recdef.

Set Default Proof Using "Type".


Section MoveToSymbol.

  Variable sig : finType.

  Variable f : sig bool.

  Variable g : sig sig.

  Definition MoveToSymbol_Step : pTM sig (option unit) 1 :=
    Switch (ReadChar)
          ( b : option sig
             match b with
             | Some x if f x
                        
                        then Return (Write (g x)) (Some tt)
                        else Return (WriteMove (g x) Rmove) (None)
             | _ Return (Nop) (Some tt)
             end).

  Definition MoveToSymbol_Step_Fun : tape sig tape sig :=
     t1
      match current with
      | Some s if (f s)
                 then tape_write (Some (g s))
                 else doAct (Some (g s), Rmove)
      | _
      end.

  Definition MoveToSymbol_Step_Rel : Rel (tapes sig 1) (option unit * tapes sig 1) :=
    Mk_R_p ( tin '(yout, tout)
              tout = MoveToSymbol_Step_Fun tin
              yout = match current tin with
                     | Some m
                       if f m
                       then Some tt
                       else None
                     | _ (Some tt)
                     end
           ).

  Lemma MoveToSymbol_Step_Sem :
    MoveToSymbol_Step c(3) MoveToSymbol_Step_Rel.
  Proof.
    eapply RealiseIn_monotone.
    {
      unfold MoveToSymbol_Step. eapply Switch_RealiseIn. eapply ReadChar_Sem. cbn.
      instantiate (2 := o : option sig match o with Some x if f x then _ else _ | None _ end).
      intros [ | ]; cbn.
      - destruct (f e).
        + instantiate (1 := 1). apply Return_RealiseIn. eapply Write_Sem.
        + apply Return_RealiseIn. eapply WriteMove_Sem.
      - apply Return_RealiseIn. eapply Nop_Sem.
    }
    {
      (cbn; ).
    }
    {
      unfold MoveToSymbol_Step_Rel, MoveToSymbol_Step_Fun. intros tin (yout, tout) H.
      TMCrush idtac; TMSolve 6.
    }
  Qed.


  Definition MoveToSymbol : pTM sig unit 1 := While MoveToSymbol_Step.

  Definition rlength (t : tape sig) := length (tape_local t).

  Function MoveToSymbol_Fun (t : tape sig) { measure rlength t } : tape sig :=
    match current t with
    | Some m if f m
               then tape_write t (Some (g m))
               else MoveToSymbol_Fun (doAct t (Some (g m), Rmove))
    | _ t
    end.
  Proof.
    intros. cbn. unfold rlength. simpl_tape.
    destruct t eqn:E; cbn in *; try now inv teq. .
  Qed.


  Lemma MoveToSymbol_Step_Fun_M2_None t :
    current t = None
    MoveToSymbol_Fun t = MoveToSymbol_Step_Fun t.
  Proof.
    intros . destruct t; cbn in *; inv ; rewrite MoveToSymbol_Fun_equation; auto.
  Qed.


  Lemma MoveToSymbol_Step_None t :
    current t = None
    MoveToSymbol_Step_Fun t = t.
  Proof.
    intros . unfold MoveToSymbol_Step_Fun. destruct t; cbn in *; inv ; auto.
  Qed.


  Lemma MoveToSymbol_Step_true t x :
    current t = Some x
    f x = true
    MoveToSymbol_Step_Fun t = tape_write t (Some (g x)).
  Proof.
    intros . unfold MoveToSymbol_Step_Fun. destruct t; cbn in *; inv . rewrite . auto.
  Qed.


  Lemma MoveToSymbol_Step_false t x :
    current t = Some x
    f x = false
    MoveToSymbol_Step_Fun t = doAct t (Some (g x), Rmove).
  Proof.
    intros . unfold MoveToSymbol_Step_Fun. destruct t; cbn in *; inv . rewrite . auto.
  Qed.


  Lemma MoveToSymbol_Step_Fun_M2_true t x :
    current t = Some x
    f x = true
    MoveToSymbol_Fun t = MoveToSymbol_Step_Fun t.
  Proof.
    intros . destruct t; cbn in *; inv . rewrite MoveToSymbol_Fun_equation, . cbn. now rewrite .
  Qed.


  Lemma MoveToSymbol_skip t s :
    current t = Some s
    f s = false
    MoveToSymbol_Fun (doAct t (Some (g s), Rmove)) = MoveToSymbol_Fun t.
  Proof. intros . cbn. symmetry. rewrite MoveToSymbol_Fun_equation. cbn. now rewrite , . Qed.

  Definition MoveToSymbol_Rel : Rel (tapes sig 1) (unit * tapes sig 1) :=
    Mk_R_p (ignoreParam ( tin tout tout = MoveToSymbol_Fun tin)).

  Lemma MoveToSymbol_Realise :
    MoveToSymbol MoveToSymbol_Rel.
  Proof.
    eapply Realise_monotone.
    {
      unfold MoveToSymbol. eapply While_Realise. eapply RealiseIn_Realise. eapply MoveToSymbol_Step_Sem.
    }
    {
      eapply WhileInduction; intros; hnf in *.
      - destruct HLastStep as (&); TMSimp.
        destruct (current _) as [s | ] eqn:E.
        + destruct (f s) eqn:E'; cbn in *; inv .
          rewrite MoveToSymbol_Fun_equation. rewrite E, E'. cbn. now apply MoveToSymbol_Step_true.
        + rewrite MoveToSymbol_Step_None; auto.
          now rewrite MoveToSymbol_Fun_equation, E.
      - destruct HStar as (&); TMSimp.
        destruct (current _) as [s | ] eqn:E; cbn in *.
        + destruct (f s) eqn:E'; cbn in *; inv .
          erewrite MoveToSymbol_Step_false; eauto. eapply MoveToSymbol_skip; eauto.
        + inv .
    }
  Qed.



  Function MoveToSymbol_steps (t : tape sig) { measure rlength t } : :=
    match current t with
    | Some m if f m then 4 else 4 + (MoveToSymbol_steps (doAct t (Some (g m), Rmove)))
    | _ 4
    end.
  Proof.
    intros t m . cbn. unfold rlength. simpl_tape.
    destruct t; cbn in *; auto. all: try now inv .
  Qed.


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

  Lemma MoveToSymbol_Terminates :
     MoveToSymbol ( tin k MoveToSymbol_steps (tin[@]) k).
  Proof.
    eapply TerminatesIn_monotone.
    { unfold MoveToSymbol. TM_Correct.
      1-2: eapply Realise_total; eapply MoveToSymbol_Step_Sem.
    }
    {
      apply WhileCoInduction; intros. cbn.
      exists 3. repeat split.
      - reflexivity.
      - intros ymid tmid. intros H. destruct ymid as [()| ]; TMSimp.
        + destruct (current _) eqn:E; TMSimp; auto.
          * destruct (f e) eqn:Ef; inv . rewrite MoveToSymbol_steps_equation in HT. rewrite E, Ef in HT. .
          * rewrite MoveToSymbol_steps_equation in HT. rewrite E in HT. .
        + destruct (current _) eqn:E.
          * destruct (f e) eqn:Ef; inv . rewrite MoveToSymbol_steps_equation in HT. rewrite E, Ef in HT.
            eexists (MoveToSymbol_steps (doAct _ (Some (g e), Rmove))). cbn.
            split.
            -- unfold MoveToSymbol_Step_Fun. rewrite E, Ef. cbn. reflexivity.
            -- rewrite HT. cbn. .
          * congruence.
    }
  Qed.



  Definition MoveToSymbol_L := Mirror MoveToSymbol.


  Definition llength (t : tape sig) := length (tape_local_l t).

  Function MoveToSymbol_L_Fun (t : tape sig) { measure llength t } : tape sig :=
    match current t with
    | Some s
      if f s
      then tape_write t (Some (g s))
      else MoveToSymbol_L_Fun (doAct t (Some (g s), Lmove))
    | _ t
    end.
  Proof. intros. unfold llength. cbn. simpl_tape. destruct t; cbn in *; inv teq. . Qed.

  Lemma MoveToSymbol_mirror t t' :
    MoveToSymbol_Fun (mirror_tape t) = mirror_tape t' MoveToSymbol_L_Fun t = t'.
  Proof.
    functional induction MoveToSymbol_L_Fun t; intros H; cbn in *; try reflexivity;
      rewrite MoveToSymbol_Fun_equation in H; cbn; auto.
    - simpl_tape in *. rewrite e, in H. cbn in *. simpl_tape in *. now apply mirror_tape_inv_midtape' in H as .
    - simpl_tape in *. rewrite e, in H. cbn in *. simpl_tape in *. auto.
    - simpl_tape in *. destruct (current t); cbn in *; auto. now apply mirror_tape_injective in H.
  Qed.


  Lemma MoveToSymbol_mirror' t t' :
    MoveToSymbol_L_Fun (mirror_tape t) = mirror_tape t' MoveToSymbol_Fun t = t'.
  Proof.
    functional induction MoveToSymbol_Fun t; intros H; cbn in *; try reflexivity;
      rewrite MoveToSymbol_L_Fun_equation in H; cbn; auto.
    - simpl_tape in *. rewrite e, in H. cbn in *. simpl_tape in *. now apply mirror_tape_inv_midtape' in H as .
    - simpl_tape in *. rewrite e, in H. cbn in *. simpl_tape in *. auto.
    - simpl_tape in *. destruct (current t); cbn in *; auto. now apply mirror_tape_injective in H.
  Qed.


  Definition MoveToSymbol_L_Rel : Rel (tapes sig 1) (unit * tapes sig 1) :=
    Mk_R_p (ignoreParam ( tin tout tout = MoveToSymbol_L_Fun tin)).

  Lemma MoveToSymbol_L_Realise :
    MoveToSymbol_L MoveToSymbol_L_Rel.
  Proof.
    eapply Realise_monotone.
    - eapply Mirror_Realise. eapply MoveToSymbol_Realise.
    - intros tin (y&tout) H. hnf in *. destruct_tapes; cbn in *. rewrite mirror_tapes_nth in H. cbn in H.
      symmetry in H. apply MoveToSymbol_mirror in H as . TMCrush simpl_tape in *; TMSolve 6.
  Qed.


  Function MoveToSymbol_L_steps (t : tape sig) { measure llength t } : :=
    match current t with
    | Some s if f s then 4 else 4 + (MoveToSymbol_L_steps (doAct t (Some (g s), Lmove)))
    | _ 4
    end.
  Proof. intros. unfold llength. cbn. simpl_tape. destruct t; cbn in *; inv teq. . Qed.

  Lemma MoveToSymbol_steps_mirror t :
    MoveToSymbol_L_steps t = MoveToSymbol_steps (mirror_tape t).
  Proof.
    functional induction MoveToSymbol_L_steps t; cbn; auto;
      simpl_tape in *; cbn in *; rewrite MoveToSymbol_steps_equation.
    - simpl_tape. now rewrite e, .
    - simpl_tape. rewrite e, . rewrite IHn. cbn. now simpl_tape.
    - simpl_tape. destruct (current t); cbn in *; auto.
  Qed.


  Lemma MoveToSymbol_L_Terminates :
     MoveToSymbol_L ( tin k MoveToSymbol_L_steps (tin[@]) k).
  Proof.
    eapply TerminatesIn_monotone.
    - eapply Mirror_Terminates. eapply MoveToSymbol_Terminates.
    - cbn. intros tin k Hk. destruct_tapes; cbn. rewrite Hk. unfold mirror_tapes. rewrite MoveToSymbol_steps_mirror. cbn. auto.
  Qed.


End MoveToSymbol.

Ltac smpl_TM_MoveToSymbol :=
  once lazymatch goal with
  | [ |- MoveToSymbol _ _ _ ] eapply MoveToSymbol_Realise
  | [ |- MoveToSymbol_L _ _ _ ] eapply MoveToSymbol_L_Realise
  | [ |- (MoveToSymbol _ _) _ ] eapply MoveToSymbol_Terminates
  | [ |- (MoveToSymbol_L _ _) _ ] eapply MoveToSymbol_L_Terminates
  end.

Smpl Add smpl_TM_MoveToSymbol : TM_Correct.

Section MoveToSymbol_Sem.

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

  Variable sig : finType.

  Variable stop : sig bool.

  Variable f : sig sig.

  Lemma MoveToSymbol_correct t str1 str2 x :
  ( x, List.In x stop x = false)
  (stop x = true)
  tape_local t = x ::
  MoveToSymbol_Fun stop f t = midtape (rev (map f ) left t) (f x) .
  Proof.
  intros H . destruct t as [ | r rs | l ls | ls m rs]; cbn in *.
  1,3: rewrite MoveToSymbol_Fun_equation; cbn; destruct ; cbn in *; try congruence.
  1: destruct ; cbn in *; congruence.
  revert m ls H. revert rs.
  refine (@size_induction _ (@length sig) _ _); intros [ | s rs'] IH; intros.
  - rewrite MoveToSymbol_Fun_equation; cbn. destruct ; cbn in *; inv .
    + rewrite . cbn. auto.
    + destruct ; cbn in *; congruence.
  - rewrite MoveToSymbol_Fun_equation; cbn.
    destruct (stop m) eqn:.
    + cbn. destruct ; cbn in *; inv ; eauto. specialize (H _ ltac:(eauto)). congruence.
    + destruct ; cbn in *; inv .
      * congruence.
      * simpl_list. eapply IH; cbn; eauto.
  Qed.


  Corollary MoveToSymbol_correct_midtape ls rs rs' m x :
  stop m = false
  ( x, List.In x rs stop x = false)
  stop x = true
  MoveToSymbol_Fun stop f (midtape ls m (rs x :: rs')) =
  midtape (rev (map f rs) (f m) :: ls) (f x) rs'.
  Proof.
  intros HStopM HStopRs HStopX.
  unshelve epose proof (@MoveToSymbol_correct (midtape ls m (rs x :: rs')) (m::rs) rs' x _ HStopX eq_refl) as Lmove.
  { intros ? [|?]; auto. }
  cbn in *. now rewrite app_assoc in Lmove.
  Qed.


  Corollary MoveToSymbol_correct_moveright ls m rs x rs' :
  ( x, List.In x rs stop x = false)
  stop x = true
  MoveToSymbol_Fun stop f (tape_move_right' ls m (rs x :: rs')) =
  midtape (rev (map f rs) m :: ls) (f x) rs'.
  Proof.
  intros HStopR HStopX.
  destruct rs as [ | s s'] eqn:E; cbn.
  - rewrite MoveToSymbol_Fun_equation. cbn. rewrite HStopX. reflexivity.
  - rewrite MoveToSymbol_correct_midtape; auto. rewrite !app_assoc. reflexivity.
  Qed.


  Lemma MoveToSymbol_correct_midtape_end tl c tr :
    ( x, List.In x (c::tr) stop x = false)
    MoveToSymbol_Fun stop f (midtape tl c tr) = rightof (hd (f c) (map f (rev tr))) (List.tl (map f (rev tr) f c::tl)).
  Proof.
    revert c tl. revert tr. cbn.
    refine (@size_induction _ (@length sig) _ _); intros [ | c' tr'] IH; intros.
    all:rewrite MoveToSymbol_Fun_equation.
    all:cbn.
    all:erewrite (H c);[ |now eauto].
    - rewrite MoveToSymbol_Fun_equation;cbn. eauto.
    - rewrite IH. 2,3:now eauto. destruct (rev tr'); cbn. easy. now autorewrite with list;cbn.
  Qed.


  Corollary MoveToSymbol_L_correct t str1 str2 x :
  ( x, List.In x stop x = false)
  (stop x = true)
  tape_local_l t = x ::
  MoveToSymbol_L_Fun stop f t = midtape (f x) (rev (map f ) right t).
  Proof.
  intros. pose proof (@MoveToSymbol_correct (mirror_tape t) x) as Lmove.
  simpl_tape in Lmove. repeat spec_assert Lmove by auto.
  erewrite (MoveToSymbol_mirror' (t' := mirror_tape (MoveToSymbol_L_Fun stop f t))) in Lmove; simpl_tape in *; eauto.
  now apply mirror_tape_inv_midtape in Lmove.
  Qed.


  Corollary MoveToSymbol_L_correct_midtape ls ls' rs m x :
  stop m = false
  ( x, List.In x ls stop x = false)
  stop x = true
  MoveToSymbol_L_Fun stop f (midtape (ls x :: ls') m rs) =
  midtape ls' (f x) (rev (map f ls) (f m) :: rs).
  Proof.
  intros HStopM HStopRs HStopX.
  unshelve epose proof (@MoveToSymbol_L_correct (midtape (ls x :: ls') m rs) (m::ls) ls' x _ HStopX eq_refl) as Lmove.
  { intros ? [|?]; auto. }
  cbn in *. now rewrite app_assoc in Lmove.
  Qed.


  Corollary MoveToSymbol_L_correct_moveleft ls x ls' m rs :
  ( x, List.In x ls stop x = false)
  stop x = true
  MoveToSymbol_L_Fun stop f (tape_move_left' (ls x :: ls') m rs) =
  midtape ls' (f x) (rev (map f ls) m :: rs).
  Proof.
  intros HStopL HStopX.
  destruct ls as [ | s s'] eqn:E; cbn.
  - rewrite MoveToSymbol_L_Fun_equation. cbn. rewrite HStopX. reflexivity.
  - rewrite MoveToSymbol_L_correct_midtape; auto. rewrite !app_assoc. reflexivity.
  Qed.




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


  Corollary MoveToSymbol_steps_midtape ls x m rs rs' :
  stop x = true
  MoveToSymbol_steps stop f (midtape ls m (rs x :: rs')) 8 + 4 * length rs.
  Proof.
  intros.
  rewrite MoveToSymbol_steps_local with ( := m::rs) (sym := x) ( := rs'); auto.
  cbn [length]. .
  Qed.


  Corollary MoveToSymbol_steps_moveright ls m rs x rs' :
  stop x = true
  MoveToSymbol_steps stop f (tape_move_right' ls m (rs x :: rs')) 4 + 4 * length rs.
  Proof.
  intros HStop. destruct rs as [ | s s'] eqn:E; cbn.
  - rewrite MoveToSymbol_steps_equation. cbn. rewrite HStop; cbn. .
  - rewrite MoveToSymbol_steps_midtape; auto. .
  Qed.


  Lemma MoveToSymbol_steps_local_end t :
  ( x, List.In x (tape_local t) stop x = false)
  MoveToSymbol_steps stop f t 4 + 4 * length (tape_local t).
  Proof.
    remember (tape_local t) as tr eqn:Ht.
    induction tr in t,Ht |-*;intros Hhalt.
    all: specialize (tape_local_nil t) as Hcur.
    - rewrite MoveToSymbol_steps_equation.
      destruct Hcur as [ _]. all:easy.
    - rewrite Ht in Hcur. destruct (current t) eqn:Hcur'.
      2:{exfalso. destruct Hcur as [? H']. now discriminate H'. }
      rewrite MoveToSymbol_steps_equation. rewrite Hcur'.
      rewrite Hhalt. 2:{destruct t;inv Hcur'. now inv Ht. }
      setoid_rewrite IHtr.
      +now cbn;nia.
      +cbn. rewrite tape_local_move_right'. symmetry in Ht. erewrite tape_local_right;eauto.
      +intros. eapply Hhalt. eauto.
  Qed.


  Corollary MoveToSymbol_steps_midtape_end tl c tr :
  ( x, List.In x (c::tr) stop x = false)
  MoveToSymbol_steps stop f (midtape tl c tr) 8 + 4 * length tr.
  Proof.
    intros. rewrite MoveToSymbol_steps_local_end. 2:easy. cbn. nia.
  Qed.


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


  Corollary MoveToSymbol_L_steps_midtape ls ls' x m rs :
  stop x = true
  MoveToSymbol_L_steps stop f (midtape (ls x :: ls') m rs) 8 + 4 * length ls.
  Proof.
  intros.
  rewrite MoveToSymbol_L_steps_local with ( := m::ls) (sym := x) ( := ls'); auto.
  cbn [length]. .
  Qed.


  Corollary MoveToSymbol_L_steps_moveleft ls ls' x m rs :
  stop x = true
  MoveToSymbol_L_steps stop f (tape_move_left' (ls x :: ls') m rs) 4 + 4 * length ls.
  Proof.
  intros HStop. destruct ls as [ | s s'] eqn:E; cbn.
  - rewrite MoveToSymbol_L_steps_equation. cbn. rewrite HStop; cbn. .
  - rewrite MoveToSymbol_L_steps_midtape; auto. .
  Qed.


End MoveToSymbol_Sem.