From Undecidability.Shared.Libs.PSL Require Import FinTypes Vectors.
From Undecidability.L Require Import L_facts UpToC.

From Coq Require Vector.
Import ListNotations.

From Coq Require Import List.

From Undecidability.TM.L.CompilerBoolFuns Require Import Compiler_spec.

From Undecidability.TM Require Import TM_facts Hoare ProgrammingTools.
From Undecidability.TM.Code Require Import CaseBool CaseList WriteValue Copy ListTM.

Set Default Proof Using "Type".

Module Boollist2encBoolsTM.
Section Fix.

  Variable Σ : finType.
  Variable s b : Σ^+.

  Variable (retr_list : Retract (sigList bool) Σ).
  Local Instance retr_bool : Retract bool Σ := ComposeRetract retr_list (Retract_sigList_X _).

  Definition M__step : pTM (Σ) ^+ (option unit) 3 :=
    If (CaseList _ retr_list @ [|Fin0;Fin2|])
       (Switch (CaseBool retr_bool @ [|Fin2|])
            (fun x =>
            WriteMove (if x then s else b) Lmove @ [|Fin1|];;
            Return Nop None))
       (Reset _ @[|Fin0|];;Return (Write b @ [|Fin1|]) (Some tt)).

  Definition M__loop := While M__step.

  Lemma loop_SpecT:
    { f : UpToC (fun bs => length bs + 1) &
    forall bs res,
      TripleT
        (≃≃([]%list,[|Contains _ bs; Custom (fun t => right t = map (fun (x:bool) => if x then s else b) res
        /\ length (left t) <= length bs); Void|]) )
        (f bs)
        M__loop
        (fun _ => ≃≃([]%list,[|Void; Custom (eq (encBoolsTM s b (rev bs++res))) ; Void |])) }.
  Proof.
    evar (c1 : nat);evar (c2 :nat).
    exists_UpToC (fun bs => c1 * length bs + c2). 2:now smpl_upToC_solve.
    intros bs res.
    unfold M__loop.
    refine (While_SpecTReg _ _
      (PRE := fun '(bs,res) => (_,_)) (INV := fun '(bs,res) y => ([y = match bs with []%list => Some tt | _ => None end]%list,_)) (POST := fun '(bs,res) y => (_,_))
    (f__step := fun '(bs,res) => _) (f__loop := fun '(bs,res) => _) (bs,res));
    clear bs res; intros (bs,res); cbn in *.
    { unfold M__step. hstep.
      - hsteps_cbn. cbn. tspec_ext.
      - cbn. hintros H.
        refine (_ : TripleT _ _ _ (fun y => ≃≃( _ ,match bs with nil => _ | cons b0 bs => _ end))).
        destruct bs as [ | b0 bs]. easy. hsteps_cbn;cbn. 3:reflexivity. now tspec_ext.
        + hintros ? ->. hsteps_cbn. 2:cbn;reflexivity. tspec_ext.
      - cbn. hintros H. destruct bs. 2:easy.
        hsteps_cbn; cbn. tspec_ext. now unfold Reset_steps;cbn;reflexivity.
      - cbn. intros ? ->. reflexivity.
    }
    cbn. split.
    -intros. destruct bs. 2:easy. split.
      +tspec_ext. unfold encBoolsTM,encBoolsListTM. destruct H1 as (t&->&H'&Hr). rewrite H'.
       destruct (left t). all:easy.
      + cbn. rewrite Nat.mul_0_r. cbn. shelve.
    - intros. destruct bs as [ | b' bs]. easy. eexists (_,_);cbn.
      split.
      +tspec_ext. destruct H1 as (t&->&?&?).
       rewrite tape_right_move_left',tape_left_move_left'. rewrite H1.
       instantiate (1:=b'::res). split. easy. destruct (left t);cbn in H2|-*. all:nia.
      + split. 2:{ tspec_ext. rewrite <- H1. now rewrite <- app_assoc. }
        shelve.
    Unshelve.
    3:unfold c2;reflexivity.
    2:{ unfold CaseList_steps,CaseList_steps_cons. rewrite Encode_bool_hasSize.
     ring_simplify. [c1]:exact 68. subst c1. cbn - ["+" "*"] in *. fold Nat.add. nia. }
  Qed.

  Definition M : pTM (Σ) ^+ unit 3 :=
     M__loop.

  Lemma SpecT:
  { f : UpToC (fun bs => length bs + 1) &
    forall bs,
      TripleT
        (≃≃([],[|Contains _ bs; Custom (eq niltape); Void|]) )
        (f bs)
        M
        (fun _ => ≃≃([],[|Void; Custom (eq (encBoolsTM s b (rev bs))) ; Void |])) }.
  Proof.
    eexists. intros. eapply ConsequenceT.
    eapply (projT2 loop_SpecT) with (res:=[]).
    -tspec_ext. rewrite <- H0. now cbn.
    -intros []. now rewrite app_nil_r.
    -reflexivity.
  Qed.

  Theorem Realise :
    Realise M (fun t '(r, t') =>
                     forall (l : list bool),
                        t[@Fin0] l ->
                        t[@Fin1] = niltape ->
                        isVoid (t[@Fin2]) ->
                        t'[@Fin1] = encBoolsTM s b (rev l)
                        /\ (isVoid (t'[@Fin0]) /\ isVoid (t'[@Fin2]))).
  Proof.
    repeat (eapply RealiseIntroAll;intro). eapply Realise_monotone.
    -eapply TripleT_Realise. eapply (projT2 SpecT).
    -cbn. intros ? [] H **. modpon H.
    {unfold "≃≃",withSpace;cbn. intros i; destruct_fin i;cbn. all:easy. }
    repeat destruct _;unfold "≃≃",withSpace in H;cbn in H.
    all:specializeFin H;eauto 6.
  Qed.

End Fix.
End Boollist2encBoolsTM.

Module encBoolsTM2boollist.
Section Fix.

  Variable Σ : finType.
  Variable s b : Σ^+.

  Variable (retr_list : Retract (sigList bool) Σ).
  Local Instance retr_bool : Retract bool Σ := ComposeRetract retr_list (Retract_sigList_X _).

  Definition M__step : pTM (Σ) ^+ (option unit) 2 :=
    Switch (ReadChar @ [|Fin0|])
      (fun x =>
        match x with
          None => Return Nop (Some tt)
        | Some x => Move Lmove @ [|Fin0|];;
                    If (Relabel (ReadChar @ [|Fin0|]) ssrbool.isSome)
                       ((Cons_constant.M (if Dec (x=s) then true else false)) retr_list @ [|Fin1|];;Return Nop (None))
                       (Return (Move Rmove @ [|Fin0|]) (Some tt))
        end).

  Definition M__loop := While M__step.


  Lemma loop_SpecT (H__neq : s <> b):
    { f : UpToC (fun bs => length bs + 1) &
    forall bs res tin,
      TripleT
        (≃≃([right tin = map (fun (x:bool) => if x then s else b) res
           /\ tape_local_l tin = (map (fun (x:bool) => if x then s else b) bs++[b]) ],[| Custom (eq tin); Contains _ res|]) )
        (f bs)
        M__loop
        (fun _ => ≃≃([],[|Custom (eq (encBoolsTM s b (rev bs++res))) ; Contains _ (rev bs ++ res)|])) }.
  Proof.
    evar (c1 : nat);evar (c2 :nat).
    exists_UpToC (fun bs => c1 * length bs + c2). 2:now smpl_upToC_solve.
    intros bs res tin.
    unfold M__loop.
    refine (While_SpecTReg
      (PRE := fun '(bs,res,tin) => (_,_))
      (INV := fun '(bs,res,tin) y =>
      ([match y with None => bs <> nil | _ => bs = nil end;
      right tin = map (fun (x:bool) => if x then s else b) res;
      tape_local_l tin = (map (fun (x:bool) => if x then s else b) bs++[b])],
      match bs with nil => [|Custom (eq tin) ; Contains _ res|]
               | b'::bs => [|Custom (eq (tape_move_left tin));Contains _ (b'::res)|] end)) (POST := fun '(bs,res,tin) y => (_,_))
    (f__step := fun '(bs,res,tin) => _) (f__loop := fun '(bs,res,tin) => _) _ _ ((bs,res,tin)));
    clear bs res tin; intros [[bs res] tin]; cbn in *.
    { unfold M__step. hintros [Hres Hbs]. hsteps_cbn;cbn. 2:reflexivity.
      cbn. intros y.
      hintros (?&->&<-).
      assert (Hcur : current tin = Some (hd s (map (fun x : bool => if x then s else b) bs ++ [b]))).
      { destruct bs;cbn in Hbs. all:now eapply tape_local_l_current_cons in Hbs as ->. }
      setoid_rewrite Hcur at 2;cbn.
      hstep;cbn. now hsteps_cbn. 2:reflexivity.
      cbn;intros _.
      hstep.
      { hsteps_cbn;cbn. intros yout. hintros (?&Hy&?&->&_&<-).
        set (y:=@ssrbool.isSome (boundary + Σ) yout).
        refine (_ : Entails _ ≃≃([ y=match bs with [] => false | _ => true end],_)). subst y yout.
        tspec_ext.
        destruct bs;cbn in Hbs;eapply tape_local_l_move_left in Hbs;cbn in Hbs.
        now destruct (tape_move_left tin);cbn in Hbs|-*;congruence.
        destruct bs;cbn in Hbs;eapply tape_local_l_current_cons in Hbs. all:now rewrite Hbs.
      }
      2:{destruct bs;hintros [=];[]. cbn in *. hsteps_cbn.
        tspec_ext. 1-2:assumption. destruct H0 as (?&?&?&?&->&?&<-). rewrite H0.
        erewrite tape_move_left_right. all:easy.
      }
      { destruct bs;hintros [=];[]. cbn in *. hsteps.
        { tspec_ext;cbn in *. contains_ext. }
        { intros. hsteps_cbn. tspec_ext. 1-3:easy. 2:now destruct H0 as (?&?&?&?&?);congruence.
          f_equal. destruct b0;decide _. all:congruence. } cbv. reflexivity.
      }
      cbn. intros ? ->. destruct bs. 2:reflexivity. nia.
    }
    split.
    - intros [Hres Hbs] _;cbn. split. 2:{ cbn. [c2]:exact 14. subst c2. fold plus. nia. }
      destruct bs as [ | ];cbn. 2:easy.
      apply midtape_tape_local_l_cons in Hbs. rewrite Hres in Hbs.
      rewrite Hbs. reflexivity.
    - intros H. destruct bs as [ | b' bs]. easy.
      intros Hres Hbs. cbn in Hbs.
      apply midtape_tape_local_l_cons in Hbs. rewrite Hres in Hbs.
       eexists ((bs,b'::res),tape_move_left tin).
      repeat eapply conj.
      +cbn.
      erewrite tape_right_move_left. 2:subst;reflexivity.
      erewrite tape_local_l_move_left. 2:subst;reflexivity.
      rewrite Hres. tspec_ext. easy.
     + subst c2;cbn;ring_simplify. [c1]:exact 15. unfold c1;fold plus;nia.
     + cbn. rewrite <- !app_assoc. reflexivity.
  Qed.

  Definition M : pTM (Σ) ^+ unit 2 :=
    (MoveToSymbol (fun _ => false) (fun x => x);;Move Lmove) @ [|Fin0|];;
    WriteValue (@nil bool) retr_list @ [|Fin1|];;
    M__loop.

  Lemma SpecT (H__neq : s <> b):
    { f : UpToC (fun bs => length bs + 1) &
      forall bs,
      TripleT
        (≃≃([],[| Custom (eq (encBoolsTM s b bs)); Void|]) )
        (f bs)
        M
        (fun _ => ≃≃([],[|Custom (eq (encBoolsTM s b bs)) ; Contains _ bs|])) }.
  Proof.
    evar (f : nat -> nat).
    exists_UpToC (fun bs => f (length bs)). 2:now shelve.
    unfold M.
    intros bs.
    hstep. {hsteps_cbn. reflexivity. }
    hnf.
    intros _.
    hstep. {hsteps_cbn. reflexivity. } 2:reflexivity.
    cbn. intros _.
    {
      eapply ConsequenceT. eapply (projT2 (loop_SpecT H__neq)) with (bs:=_)(res:=_) (tin:=_).
      3:reflexivity. 2:{ intro;cbn. rewrite rev_involutive,app_nil_r. reflexivity. }
      eapply EntailsI. intros tin.
      unfold encBoolsTM,encBoolsListTM.
      rewrite MoveToSymbol_correct_midtape_end. 2:easy.
      intros [_ H]%tspecE.
      specializeFin H.
      destruct H0 as (?&H0&<-).
      tspec_solve. 2:rewrite H0;reflexivity.
      cbn. split. easy. rewrite <- map_rev,map_map;cbn. destruct (rev bs);cbn. all:easy.
    }
    cbn - ["+"].
    rewrite UpToC_le. ring_simplify.
    unfold encBoolsTM,encBoolsListTM.
    rewrite MoveToSymbol_steps_midtape_end. 2:easy.
    rewrite map_length,rev_length.
    [f]:intros n. now unfold f;set (n:=length bs);reflexivity.

    Unshelve. subst f;cbn beta. smpl_upToC_solve.
  Qed.

  Theorem Realise (H__neq : s <> b):
    Realise M (fun t '(r, t') =>
                     forall (l : list bool),
                        t[@Fin0] = encBoolsTM s b l ->
                        isVoid t[@Fin1] ->
                        t[@Fin0] = t'[@Fin0]
                        /\ t'[@Fin1] l).
  Proof.
    repeat (eapply RealiseIntroAll;intro). eapply Realise_monotone.
    -eapply TripleT_Realise,(projT2 (SpecT H__neq)).
    -intros ? [] H **. modpon H.
    {unfold "≃≃",withSpace;cbn. intros i; destruct_fin i;cbn. all:eauto. }
    repeat destruct _;unfold "≃≃",withSpace in H;cbn in H.
    specializeFin H. cbn in *;easy.
  Qed.

End Fix.
End encBoolsTM2boollist.