From Undecidability.TM Require Import ProgrammingTools.
From Undecidability Require Import CaseNat CaseList CaseSum 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".

Section Rev.

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

  Definition Rev_Step : pTM (sigList sigX)^+ (option unit) 3 :=
    If (CaseList _ @[|;|])
       (Return (Constr_cons _ @[|; |];; Reset _ @[||]) None)
       (Return ( _ @[||]) (Some tt)).

  Definition Rev_Step_size (xs : list X) :=
    match xs with
    | nil [| ResetEmpty1_size; id; id |]
    | x :: xs' [| CaseList_size0 x; Constr_cons_size x; CaseList_size1 x >> Reset_size x |]
    end.

  Definition Rev_Step_Rel : pRel (sigList sigX)^+ (option unit) 3 :=
     tin '(yout, tout)
       (xs ys : list X) (sx sy sz : ),
        let size := Rev_Step_size xs in
        tin[@] ≃(;sx) xs
        tin[@] ≃(;sy) ys
        isVoid_size tin[@] sz
        match yout, xs with
        | (Some tt), nil
          isVoid_size tout[@] (size@> sx)
          tout[@] ≃(;size@> sy) ys
          isVoid_size tout[@] (size@> sz)
        | None, x :: xs'
          tout[@] ≃(;size@> sx) xs'
          tout[@] ≃(;size@> sy) x :: ys
          isVoid_size tout[@] (size@> sz)
        | _, _ False
        end.

  Lemma Rev_Step_Realise : Rev_Step Rev_Step_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Rev_Step. TM_Correct.
      - eapply RealiseIn_Realise. apply ResetEmpty1_Sem with (X := list X). }
    {
      intros tin (yout, tout) H. cbn. intros xs ys sx sy sz Hxs Hys Hright. destruct H as [H|H]; TMSimp.
      - modpon H. destruct xs as [ | x xs]; cbn in *; auto. TMSimp. modpon . modpon . repeat split; auto.
      - modpon H. destruct xs as [ | x xs]; cbn in *; auto. TMSimp. modpon . repeat split; auto.
    }
  Qed.


  Definition Rev_Step_steps (xs : list X) : :=
    match xs with
    | nil 1 + CaseList_steps xs + ResetEmpty1_steps
    | x :: xs' 2 + CaseList_steps xs + Constr_cons_steps x + Reset_steps x
    end.

  Definition Rev_Step_T : tRel (sigList sigX)^+ 3 :=
     tin k (xs ys : list X),
        tin[@] xs tin[@] ys isVoid tin[@] Rev_Step_steps xs k.

  Lemma Rev_Step_Terminates : Rev_Step Rev_Step_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold Rev_Step. TM_Correct.
      - eapply RealiseIn_TerminatesIn. apply ResetEmpty1_Sem with (X := X). }
    {
      intros tin k. intros (xs&ys&Hxs&Hys&Hright&Hk). destruct xs; cbn in *.
      - eexists (CaseList_steps _), ResetEmpty1_steps. repeat split; try ; eauto.
        intros tmid b (&H1Inj); TMSimp. modpon . destruct b; cbn in *; auto.
      - exists (CaseList_steps (x::xs)), (1 + Constr_cons_steps x + Reset_steps x). repeat split; try ; eauto.
        intros tmid b (H&HInj); TMSimp. modpon H. destruct b; cbn in *; auto. modpon H.
        exists (Constr_cons_steps x), (Reset_steps x). repeat split; try ; eauto.
        intros tmid0_ [] (?H&?HInj); TMSimp. modpon . TMSimp. eexists; split; eauto.
    }
  Qed.


  Definition Rev_Append := While Rev_Step.

  Fixpoint Rev_Append_size (xs : list X) : Vector.t () 3 :=
    match xs with
    | nil Rev_Step_size xs
    | x :: xs' Rev_Step_size xs >>> Rev_Append_size xs'
    end.

  Definition Rev_Append_Rel : pRel (sigList sigX)^+ unit 3 :=
     tin '(yout, tout)
       (xs ys : list X) (sx sy sz : ),
        let size := Rev_Append_size xs in
        tin[@] ≃(;sx) xs
        tin[@] ≃(;sy) ys
        isVoid_size tin[@] sz
        isVoid_size tout[@] (size@> sx)
        tout[@] ≃(;size@> sy) rev xs ys
        isVoid_size tout[@] (size@> sz).

  Lemma Rev_Append_Realise : Rev_Append Rev_Append_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Rev_Append. TM_Correct.
      - apply Rev_Step_Realise. }
    {
      apply WhileInduction; intros.
      - TMSimp. intros. modpon HLastStep. destruct xs as [ | x xs]; cbn in *; auto.
      - TMSimp. intros. modpon HStar. destruct xs as [ | x xs]; cbn in *; auto. modpon HStar.
        modpon HLastStep. simpl_list. repeat split; auto.
    }
  Qed.


  Fixpoint Rev_Append_steps (xs : list X) : :=
    match xs with
    | nil Rev_Step_steps xs
    | x :: xs' 1 + Rev_Step_steps xs + Rev_Append_steps xs'
    end.

  Definition Rev_Append_T : tRel (sigList sigX)^+ 3 :=
     tin k (xs ys : list X),
        tin[@] xs tin[@] ys isVoid tin[@] Rev_Append_steps xs k.

  Lemma Rev_Append_Terminates : Rev_Append Rev_Append_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold Rev_Append. TM_Correct.
      - apply Rev_Step_Realise.
      - apply Rev_Step_Terminates. }
    { apply WhileCoInduction; intros.
      destruct HT as (xs&ys&Hxs&Hys&Hright&Hk).
      exists (Rev_Step_steps xs). repeat split.
      - hnf; eauto 6.
      - intros ymid tmid H. cbn in *. modpon H. destruct ymid as [ [] | ].
        + destruct xs as [ | x xs]; cbn in *; auto.
        + destruct xs as [ | x xs]; cbn in *; auto. modpon H.
          exists (Rev_Append_steps xs). repeat split; try .
          hnf; eauto 6.
    }
  Qed.



  Lemma Rev_Append_SpecT (xs ys:list X) ss:
  TripleT ≃≃([],withSpace [|Contains _ xs;Contains _ ys;Void|] ss) (Rev_Append_steps xs) Rev_Append
  ( _ ≃≃([],withSpace [|Void;Contains _ (rev xsys);Void|] (appSize (Rev_Append_size xs) ss))).
  Proof.
    unfold withSpace in *.
    eapply Realise_TripleT. now apply Rev_Append_Realise. now apply Rev_Append_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 *. hnf. eexists _,_. repeat split.
       1,2:now contains_ext. now isVoid_mono. easy.
  Qed.


  Definition Rev := Constr_nil _ @[||];; Rev_Append.

  Definition Rev_size (xs : list X) := [| Rev_Append_size xs @>; pred >> Rev_Append_size xs @>; Rev_Append_size xs @> |].

  Definition Rev_Rel : pRel (sigList sigX)^+ unit 3 :=
     tin '(yout, tout)
       (xs : list X) (s0 s1 s2 : ),
        let size := Rev_size xs in
        tin[@] ≃(;) xs
        isVoid_size tin[@]
        isVoid_size tin[@]
        isVoid_size tout[@] (size@> )
        tout[@] ≃(;size@> ) rev xs
        isVoid_size tout[@] (size@> ).

  Lemma Rev_Realise : Rev Rev_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Rev. TM_Correct.
      - apply Rev_Append_Realise. }
    { intros tin ([], tout) H. TMSimp. intros. modpon H. modpon .
      repeat split; auto. contains_ext. now simpl_list. }
  Qed.


  Definition Rev_steps (xs : list X) := 1 + Constr_nil_steps + Rev_Append_steps xs.

  Definition Rev_T : tRel (sigList sigX)^+ 3 :=
     tin k (xs : list X),
        tin[@] xs isVoid tin[@] isVoid tin[@] Rev_steps xs k.

  Lemma Rev_Terminates : Rev Rev_T.
  Proof.
    eapply TerminatesIn_monotone.
    { unfold Rev. TM_Correct.
      - apply Rev_Append_Terminates. }
    { intros tin k (xs&Hxs&&&Hk).
      exists (Constr_nil_steps), (Rev_Append_steps xs). repeat split; hnf; eauto.
      intros tmid [] (H&HInj); TMSimp. modpon H. hnf. do 2 eexists; repeat split; TMSimp; eauto. }
  Qed.


  Lemma Rev_SpecT (xs:list X) ss:
  TripleT ≃≃([],withSpace [|Contains _ xs;Void;Void|] ss) (Rev_steps xs) Rev
  ( _ ≃≃([],withSpace [|Void;Contains _ (rev xs);Void|] (appSize (Rev_size xs) ss))).
  Proof.
    unfold withSpace in *.
    eapply Realise_TripleT. now apply Rev_Realise. now apply Rev_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 *. hnf. eexists. repeat split.
       1:contains_ext. 1-2:isVoid_mono. easy.
  Qed.


End Rev.

Import Hoare.

Ltac hstep_App :=
  lazymatch goal with
  | [ |- TripleT ?P ?k (Rev _) ?Q ] eapply Rev_SpecT
  | [ |- TripleT ?P ?k (Rev_Append _) ?Q ] refine (Rev_Append_SpecT _ _ _ _);shelve
  end.

Smpl Add hstep_App : hstep_Spec.