From Undecidability.TM Require Import ProgrammingTools.
From Undecidability Require Import CaseNat CaseList CaseSum. (* TM.Code.CaseSum contains Constr_Some and Constr_None. *)
From Undecidability.TM Require Hoare.

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


Local Arguments Encode_list : simpl never.
Local Arguments Encode_nat : simpl never.

Set Default Proof Using "Type".

From Undecidability Require Import TM.Basic.Mono TM.Code.Copy.

Lemma pair_eq (A B : Type) (a1 a2 : A) (b1 b2 : B) :
  (a1, b1) = (a2, b2) ->
  a1 = a2 /\ b1 = b2.
Proof. intros H. now inv H. Qed.

Section ListStuff.
  Variable X : Type.

  (* TODO: -> base *)
  Lemma app_or_nil (xs : list X) :
    xs = nil \/ exists ys y, xs = ys ++ [y].
  Proof.
    induction xs as [ | x xs IH]; cbn in *.
    - now left.
    - destruct IH as [ -> | (ys&y&->) ].
      + right. exists nil, x. cbn. reflexivity.
      + right. exists (x :: ys), y. cbn. reflexivity.
  Qed.

  (* TODO: -> base *)
  Lemma map_removelast (A B : Type) (f : A -> B) (l : list A) :
    map f (removelast l) = removelast (map f l).
  Proof.
    induction l as [ | a l IH]; cbn in *; auto.
    destruct l as [ | a' l]; cbn in *; auto.
    f_equal. auto.
  Qed.

  (* TODO: -> base *)
  Corollary removelast_app_singleton (xs : list X) (x : X) :
    removelast (xs ++ [x]) = xs.
  Proof. destruct xs. reflexivity. rewrite removelast_app. cbn. rewrite app_nil_r. reflexivity. congruence. Qed.

  (* TODO: -> base *)
  Corollary removelast_cons (xs : list X) (x : X) :
    xs <> nil ->
    removelast (x :: xs) = x :: removelast xs.
  Proof. intros. change (x :: xs) with ([x] ++ xs). now rewrite removelast_app. Qed.

  (* TODO: -> base *)
  Corollary removelast_length (xs : list X) :
    length (removelast xs) = length xs - 1.
  Proof.
    destruct (app_or_nil xs) as [ -> | (x&xs'&->)].
    - cbn. reflexivity.
    - rewrite removelast_app_singleton. rewrite app_length. cbn. lia.
  Qed.

End ListStuff.

(* ** Append *)

(* I simply copy memory instead of using constructors/deconstructors. The former approach is maybe easier, but I want to use fewer internal tapes. *)
Section Append.

  Variable (sigX : finType) (X : Type) (cX : codable sigX X).
  Hypothesis (defX: inhabitedC sigX).

  Notation sigList := (FinType (EqType (sigList sigX))) (only parsing).

  Let stop : sigList^+ -> bool :=
    fun x => match x with
          | inl (START) => true (* halt at the start symbol *)
          | _ => false
          end.

  Definition App'_size {sigX X : Type} {cX : codable sigX X} (xs : list X) (s1 : nat) := s1 - (size (Encode_list cX) xs - 1).

  Definition App'_Rel : Rel (tapes sigList^+ 2) (unit * tapes sigList^+ 2) :=
    ignoreParam (fun tin tout =>
                   forall (xs ys : list X) (s0 s1 : nat),
                     tin[@Fin0] ≃(;s0) xs ->
                     tin[@Fin1] ≃(;s1) ys ->
                     tout[@Fin0] ≃(;s0) xs /\
                     tout[@Fin1] ≃(;App'_size xs s1) xs ++ ys).

  Definition App' : pTM sigList^+ unit 2 :=
    LiftTapes (MoveRight _;; Move Lmove;; Move Lmove) [|Fin0|];;
    CopySymbols_L stop.

  Lemma App'_Realise : App' App'_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold App'. TM_Correct.
      - apply MoveRight_Realise with (X := list X).
    }
    {
      intros tin ((), tout) H. cbn. intros xs ys s0 s1 HEncXs HEncYs.
      destruct HEncXs as (ls1&HEncXs&Hs0), HEncYs as (ls2&HEncYs&Hs1). TMSimp; clear_trivial_eqs.
      rename H into HMoveRight; rename H0 into HCopy.
      modpon HMoveRight. repeat econstructor. destruct HMoveRight as (ls3&HEncXs'). TMSimp.
      unfold App'_size in *.

      pose proof app_or_nil xs as [ -> | (xs'&x&->) ]; cbn in *; auto.
      - rewrite CopySymbols_L_Fun_equation in HCopy; cbn in *. inv HCopy; TMSimp. repeat econstructor.
        + lia.
        + rewrite Encode_list_hasSize. cbn. lia.
      - cbv [Encode_list] in *; cbn in *.
        rewrite encode_list_app in HCopy. cbn in *.
        rewrite !map_rev, !map_map, <- map_rev in HCopy.

        rewrite rev_app_distr in HCopy. rewrite <- tl_rev in HCopy. rewrite map_app, <- !app_assoc in HCopy.
        rewrite <- tl_map in HCopy. rewrite map_rev in HCopy. cbn in *. rewrite <- app_assoc in HCopy. cbn in *.
        rewrite !List.map_app, !List.map_map in HCopy. rewrite rev_app_distr in HCopy. cbn in *.
        rewrite map_rev, tl_rev in HCopy.

        rewrite app_comm_cons, app_assoc in HCopy. rewrite CopySymbols_L_correct_moveleft in HCopy; cbn in *; auto.
        + rewrite rev_app_distr, rev_involutive, <- app_assoc in HCopy. inv HCopy; TMSimp.
          * rewrite <- app_assoc. cbn. repeat econstructor.
            -- f_equal. cbn. rewrite encode_list_app. rewrite map_map, map_app, <- app_assoc.
               cbn.
               f_equal.
               ++ now rewrite rev_involutive, map_removelast.
               ++ f_equal. now rewrite map_app, List.map_map, <- app_assoc.
            -- lia.
            -- f_equal. cbn. rewrite rev_involutive, <- !app_assoc, !map_map. rewrite !encode_list_app. rewrite map_app, <- app_assoc.
               rewrite <- map_removelast. f_equal. cbn [encode_list].
               rewrite removelast_cons by (intros (?&?) % appendNil; congruence).
               cbn. f_equal.
               rewrite !map_app, <- !app_assoc.
               rewrite !removelast_app by congruence.
               now rewrite !map_app, <- !app_assoc, !map_map.
            -- simpl_list. rewrite encode_list_app. rewrite skipn_length. cbn. simpl_list. rewrite removelast_length. cbn. simpl_list. simpl_list. rewrite removelast_length. cbn. lia.
        + cbn.
          intros ? [ (?&<-&?) % in_rev % in_map_iff | H' % in_rev ] % in_app_iff. cbn. auto. cbn in *.
          rewrite rev_involutive, <- map_removelast in H'.
          apply in_app_iff in H' as [ (?&<-&?) % in_map_iff | [ <- | [] ] ]. all: auto.
    }
  Qed.

  Definition App'_steps {sigX X : Type} {cX : codable sigX X} (xs : list X) :=
    29 + 12 * size xs.

  Definition App'_T : tRel sigList^+ 2 :=
    fun tin k => exists (xs ys : list X), tin[@Fin0] xs /\ tin[@Fin1] ys /\ App'_steps xs <= k.

  Lemma App'_Terminates : projT1 App' App'_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold App'. TM_Correct. (* This is a bit strange, because App' is a sequence of two sequences. *)
      - apply MoveRight_Realise with (X := list X).
      - apply MoveRight_Realise with (X := list X).
      - apply MoveRight_Terminates with (X := list X).
    }
    {
      intros tin k (xs&ys&HEncXS&HEncYs&Hk). unfold App'_steps in *.
      exists (12+4*size xs), (16+8*size xs). repeat split; cbn; try lia.
      exists (8+4*size xs), 3. repeat split; cbn; try lia. eauto.
      intros tmid1 () H. modpon H.
      exists 1, 1. repeat split; try lia. eauto.
      intros tmid (). intros H; TMSimp; clear_trivial_eqs. modpon H.
      destruct H as (ls&HEncXs); TMSimp.
      cbv [Encode_list]; cbn in *.

      destruct (app_or_nil xs) as [-> | (xs'&x&->)]; cbn in *.
      { (* xs = nil *)
        rewrite CopySymbols_L_steps_equation. cbn. lia.
      }
      { (* xs = xs' ++ [x] *)
        rewrite encode_list_app.
        rewrite map_rev, map_map, <- map_rev.
        rewrite rev_app_distr. cbn. rewrite <- app_assoc, rev_app_distr, <- app_assoc. cbn.
        rewrite CopySymbols_L_steps_moveleft; cbn; auto.
        rewrite map_length, !app_length, rev_length. cbn. rewrite map_length, rev_length, !app_length, !map_length. cbn.
        rewrite removelast_length. lia.
      }
    }
  Qed.

  Import Hoare.

  Definition App'_sizeV (xs : list X) :=
    [| id;
       App'_size xs
     |].

  Lemma App'_SpecT (xs ys:list X) ss:
  TripleT ≃≃([],withSpace [|Contains _ xs;Contains _ ys|] ss) (App'_steps xs) App'
  (fun _ => ≃≃([],withSpace [|Contains _ xs;Contains _ (xs++ys)|] (appSize (App'_sizeV xs) ss ))).
  Proof.
    unfold withSpace in *.
    eapply Realise_TripleT. now apply App'_Realise. now apply App'_Terminates.
    - intros tin yout tout H [_ HEnc]%tspecE. cbn in *.
      specializeFin HEnc. simpl_vector in *; cbn in *. modpon H. tspec_solve.
    - intros tin k [_ HEnc]%tspecE Hk. cbn in *.
      specializeFin HEnc. simpl_vector in *; cbn in *. do 2 eexists. repeat split. 1-2:contains_ext. easy.
  Qed.

(*
  Definition App : pTM sigList^+ unit 3 :=
    LiftTapes (CopyValue _) |Fin1; Fin2|;;
    LiftTapes (App') |Fin0; Fin2|.


  
  Lemma App_Computes : App ⊨ Computes2_Rel (@app X).
  Proof.
    eapply Realise_monotone.
    { unfold App. TM_Correct.
      - apply CopyValue_Realise with (X := list X).
      - apply App'_Realise.
    }
    {
      intros tin ((), tout) H. cbn. intros xs ys HEncXs HEncYs HOut _.
      TMSimp. rename H into HCopy; rename H0 into HComp.
      modpon HCopy. modpon HComp.
      repeat split; auto.
      - intros i; destruct_fin i.
    }
  Qed.



  Definition App_steps {sigX X : Type} {cX : codable sigX X} (xs ys : list X) :=
    55 + 12 * size xs + 12 * size ys.


  Definition App_T : tRel sigList^+ 3 :=
    fun tin k => exists (xs ys : list X), tin@Fin0 ≃ xs /\ tin@Fin1 ≃ ys /\ isVoid tin@Fin2 /\ App_steps xs ys <= k.

    
  Lemma App_Terminates : projT1 App ↓ App_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold App. TM_Correct.
      - apply App'_Terminates.
    }
    {
      intros tin k (xs&ys&HEncXs&HEnYs&HRigh2&Hk).
      exists (25 + 12 * size ys), (App'_steps xs). repeat split; cbn; eauto.
      unfold App'_steps, App_steps in *. lia.
      intros tmid () (HApp'&HInjApp'); TMSimp.
      specialize (HApp' ys).
      modpon HApp'.
      hnf. cbn. do 2 eexists. repeat split; eauto.
    }
  Qed. *)


  Definition App :pTM _ _ 2 :=
    App' @ [|Fin0; Fin1|];;
    MoveValue _ @ [|Fin1; Fin0|].

  Definition App_size (Q Q' : list X) : Vector.t (nat->nat) 2 :=
    [| MoveValue_size_y (Q ++ Q') Q; App'_size Q >> MoveValue_size_x (Q ++ Q') |].

  Definition App_Rel : pRel ((sigList sigX) ^+) unit 2 :=
    ignoreParam (
        fun tin tout =>
          forall (Q Q' : list X) (s0 s1 : nat),
            tin[@Fin0] ≃(;s0) Q ->
            tin[@Fin1] ≃(;s1) Q' ->
            tout[@Fin0] ≃(;App_size Q Q' @>Fin0 s0) Q ++ Q' /\
            isVoid_size tout[@Fin1] (App_size Q Q' @>Fin1 s1)
      ).

  Lemma App_Realise : App App_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold App. TM_Correct.
      - apply App'_Realise.
    }
    {
      intros tin ((), tout) H. intros Q Q' s0 s1 HEncQ HEncQ'.
      TMSimp. modpon H. modpon H0. auto.
    }
  Qed.

  Arguments App_size : simpl never.

  Definition App_steps (Q Q': list X) := 1 + App'_steps Q + MoveValue_steps (Q ++ Q') Q.

  Definition App_T : tRel (sigList sigX) ^+ 2 :=
    fun tin k => exists (Q Q' : list X), tin[@Fin0] Q /\ tin[@Fin1] Q' /\ App_steps Q Q' <= k.

  Lemma App_Terminates : projT1 App App_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold App. TM_Correct.
      - apply App'_Realise.
      - apply App'_Terminates.
    }
    {
      intros tin k (Q&Q'&HEncQ&HEncQ'&Hk).
      exists (App'_steps Q), (MoveValue_steps (Q++Q') Q); cbn; repeat split; try lia.
      hnf; cbn. eauto. now rewrite Hk.
      intros tmid () (HApp&HInjApp); TMSimp. modpon HApp.
      exists (Q++Q'), Q. repeat split; eauto.
    }
  Qed.

  Lemma App_SpecT (xs ys:list X) ss:
  TripleT ≃≃([],withSpace [|Contains _ xs;Contains _ ys|] ss) (App_steps xs ys) App
  (fun _ => ≃≃([],withSpace [|Contains _ (xs++ys);Void|] (appSize (App_size xs ys) ss ))).
  Proof.
    unfold withSpace in *.
    eapply Realise_TripleT. now apply App_Realise. now apply App_Terminates.
    - intros tin yout tout H [_ HEnc]%tspecE. cbn in *.
      specializeFin HEnc. simpl_vector in *; cbn in *. modpon H. tspec_solve.
    - intros tin k [_ HEnc]%tspecE Hk. cbn in *.
      specializeFin HEnc. simpl_vector in *; cbn in *. do 2 eexists. repeat split. 1-2:contains_ext. easy.
  Qed.

End Append.

Import Hoare.

Ltac hstep_App :=
  lazymatch goal with
  | [ |- TripleT ?P ?k (App' _) ?Q ] => eapply App'_SpecT
  | [ |- TripleT ?P ?k (App _) ?Q ] => eapply App_SpecT
  end.

Smpl Add hstep_App : hstep_Spec.

Arguments App'_steps {sigX X cX} : simpl never.
Arguments App'_size {sigX X cX} : simpl never.
Arguments App_steps {sigX X cX} : simpl never.
Arguments App_size {sigX X cX} : simpl never.

From Undecidability.L.Complexity Require Import UpToC.

Section App_nice.
  Variable (sigX X : Type) (cX : codable sigX X).

  Lemma App'_steps_nice :
    App'_steps <=c size (X:=list X).
  Proof.
    eexists (29+12). intros xs. unfold App'_steps.
    rewrite Encode_list_hasSize.
    specialize (Encode_list_hasSize_ge1 _ xs). nia.
  Qed.

End App_nice.