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.

Require Import Equations.Type.DepElim.

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 @ [|;|])
       (Switch (CaseBool retr_bool @ [||])
            ( x
            WriteMove (if x then s else b) Lmove @ [||];;
            Return Nop None))
       (Reset _ @[||];;Return (Write b @ [||]) (Some tt)).

  Definition M__loop := While M__step.

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


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

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


  Theorem Realise :
    Realise M ( t '(r, t')
                      (l : list bool),
                        t[@] l
                        t[@] = niltape
                        isVoid (t[@])
                        t'[@] = encBoolsTM s b (rev l)
                         (isVoid (t'[@]) isVoid (t'[@]))).
  Proof.
    repeat (eapply RealiseIntroAll;intro). eapply Realise_monotone.
    -eapply TripleT_Realise. eapply ( 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 @ [||])
      ( x
        match x with
          None Return Nop (Some tt)
        | Some x Move Lmove @ [||];;
                    If (Relabel (ReadChar @ [||]) ssrbool.isSome)
                       ((Cons_constant.M (if Dec (x=s) then true else false)) retr_list @ [||];;Return Nop (None))
                       (Return (Move Rmove @ [||]) (Some tt))
        end).

  Definition M__loop := While M__step.


  Lemma loop_SpecT (H__neq : s b):
    { f : UpToC ( bs length bs + 1) &
     bs res tin,
      TripleT
        (≃≃([right tin = map ( (x:bool) if x then s else b) res
            tape_local_l tin = (map ( (x:bool) if x then s else b) bs[b]) ],[| Custom (eq tin); Contains _ res|]) )
        (f bs)
        M__loop
        ( _ ≃≃([],[|Custom (eq (encBoolsTM s b (rev bsres))) ; Contains _ (rev bs res)|])) }.
  Proof.
    evar ( : );evar ( :).
    exists_UpToC ( bs * length bs + ). 2:now smpl_upToC_solve.
    intros bs res tin.
    unfold M__loop.
    eapply While_SpecTReg with
      (PRE := '(bs,res,tin) (_,_))
      (INV := '(bs,res,tin) y
      ([match y with None bs nil | _ bs = nil end;
      right tin = map ( (x:bool) if x then s else b) res;
      tape_local_l tin = (map ( (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 := '(bs,res,tin) y (_,_))
    (f__step := '(bs,res,tin) _) (f__loop := '(bs,res,tin) _) (x := (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 ( 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 as (?&?&?&?&&?&). rewrite .
        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 as (?&?&?&?&?);congruence.
          f_equal. destruct ;decide _. all:congruence. } cbv. reflexivity.
      }
      cbn. intros ? . destruct bs. 2:reflexivity. nia.
    }
    split.
    - intros [Hres Hbs] _;cbn. split. 2:{ cbn. []:exact 14. subst . 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 ;cbn;ring_simplify. []:exact 15. unfold ;nia.
     + cbn. rewrite !app_assoc. reflexivity.
  Qed.


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

  Lemma SpecT (H__neq : s b):
    { f : UpToC ( bs length bs + 1) &
       bs,
      TripleT
        (≃≃([],[| Custom (eq (encBoolsTM s b bs)); Void|]) )
        (f bs)
        M
        ( _ ≃≃([],[|Custom (eq (encBoolsTM s b bs)) ; Contains _ bs|])) }.
  Proof.
    evar (f : ).
    exists_UpToC ( 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 ( (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 as (?&&).
      tspec_solve. 2:rewrite ;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 . smpl_upToC_solve.
  Qed.


  Theorem Realise (H__neq : s b):
    Realise M ( t '(r, t')
                      (l : list bool),
                        t[@] = encBoolsTM s b l
                        isVoid t[@]
                        t[@] = t'[@]
                         t'[@] l).
  Proof.
    repeat (eapply RealiseIntroAll;intro). eapply Realise_monotone.
    -eapply TripleT_Realise,( (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.