From Undecidability Require Import ProgrammingTools Hoare.
From Undecidability Require Import CaseNat CaseList CaseSum.
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 Nth'.


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

  Variable (retr1 : Retract (sigList sigX) sig) (retr2 : Retract sigNat sig).
  Local Instance retr_X_list' : Retract sigX sig := ComposeRetract retr1 (Retract_sigList_X _).


  Definition Nth'_Step_size {sigX X : Type} {cX : codable sigX X} (n : nat) (l : list X) : Vector.t (nat -> nat) 3 :=
    match n, l with
    | S n', x :: l' =>
      [| CaseList_size0 x; S; CaseList_size1 x >> Reset_size x|]
    | 0, x :: x' =>
      [|fun s0 => CaseList_size0 x s0; id; fun s2 => CaseList_size1 x s2|]
    | 0, nil => [|id; id; id|]
    | S n', nil => [|id; fun s1 => S s1; id|]
    end.

  Definition Nth'_Step : pTM sig^+ (option bool) 3 :=
    If (LiftTapes (ChangeAlphabet CaseNat _) [|Fin1|])
       (If (LiftTapes (ChangeAlphabet (CaseList sigX) _) [|Fin0; Fin2|])
           (Return (LiftTapes (Reset _) [|Fin2|]) None)
           (Return Nop (Some false)))
       (Relabel (LiftTapes (ChangeAlphabet (CaseList sigX) _) [|Fin0; Fin2|]) Some)
  .

  Definition Nth'_Step_steps {sigX X : Type} {cX : codable sigX X} (l : list X) (n : nat) :=
    match n, l with
    | S n', x :: l' =>
      2 + CaseNat_steps + CaseList_steps_cons x + Reset_steps x
    | S n', nil =>
      2 + CaseNat_steps + CaseList_steps_nil
    | O, x :: l' =>
      1 + CaseNat_steps + CaseList_steps_cons x
    | O, nil =>
      1 + CaseNat_steps + CaseList_steps_nil
    end.

    Definition Nth'_Step_steps_CaseList (xs : list X) :=
      match xs with
      | x :: xs' => 1 + CaseList_steps_cons x + Reset_steps x
      | nil => 1 + CaseList_steps_nil
      end.

    Lemma Nth'_Step_SpecT_size (n : nat) (xs : list X) (ss : Vector.t nat 3) :
      TripleT
        (≃≃([],withSpace ([|Contains _ xs; Contains _ n; Void|]) ss))
        (Nth'_Step_steps xs n) Nth'_Step
        (fun yout =>
           ≃≃([yout = match xs,n with [],_ => Some false | _ , 0 => Some true | _,__ => None end ],
                      withSpace
                    match xs,n with
                    | nil,_ => [|Contains _ xs; Contains _ (pred n); Void|]
                    | x::xs', S n' => [|Contains _ xs'; Contains _ n'; Void|]
                    | x::xs', 0 => [|Contains _ xs'; Contains _ 0; Contains _ x|]
                    end (appSize (Nth'_Step_size n xs) ss))).
    Proof.
      start_TM.
      unfold Nth'_Step.
      eapply If_SpecTReg with (k1 := CaseNat_steps) (k2 := Nth'_Step_steps_CaseList xs) (k3 := CaseList_steps xs).
      - unfold_abbrev. hstep; cbn.
        hstep; cbn.         hstep; cbn. cbn. tspec_ext.
      - cbn. hintros ?. destruct n as [ | n'];cbn. nia.
        + eapply If_SpecTReg.
          * hstep; cbn. hstep; cbn. hstep; cbn. cbn. tspec_ext.
          * cbn. hintros H'.
            refine (_ : TripleT _ (match xs with x::xs => _ | _ => 0 end) _ _).
            destruct xs. easy. hstep; cbn. hstep; cbn.
            now apply Reset_SpecT_space. cbn. tspec_ext.
          * cbn. hintros H'.
            destruct xs. 2:easy.
            hstep; cbn. hstep; cbn. cbn. tspec_ext.
          * cbn. intros ? ->. destruct xs; cbn in *; auto.
      - cbn. hintros ->. cbn.
        hstep; cbn.
        { hstep; cbn. hstep; cbn. hstep; cbn. cbn. tspec_ext. }
        cbn. hintros yout ->. destruct xs as [ | x xs'];cbn.
        + tspec_ext.
        + tspec_ext.
      - cbn. unfold Nth'_Step_steps. intros b Hb. destruct b,xs,n;cbn;unfold CaseList_steps. all:lia.
    Qed.

  Fixpoint Nth'_Loop_size {sigX X : Type} {cX : codable sigX X} (n : nat) (l : list X) {struct n} : Vector.t (nat -> nat) 3 :=
    match n, l with
    | S n', x :: l' => Nth'_Step_size n l >>> Nth'_Loop_size n' l'
    | _, _ => Nth'_Step_size n l
    end.

  Definition Nth'_Loop := While Nth'_Step.

  Fixpoint Nth'_Loop_steps {sigX X : Type} {cX : codable sigX X} (l : list X) (n : nat) { struct l } :=
    match n, l with
    | S n', x :: l' => S (Nth'_Step_steps l n) + Nth'_Loop_steps l' n'
    | S n', nil => Nth'_Step_steps l n
    | O, x :: l' => Nth'_Step_steps l n
    | O, nil => Nth'_Step_steps l n
    end.

    Lemma Nth'_Loop_SpecT_size (xs:list X) n (ss : Vector.t nat 3) :
    TripleT
      ≃≃([],withSpace ([|Contains _ xs; Contains _ n; Void|]) ss)
      (Nth'_Loop_steps xs n) Nth'_Loop
      (fun yout =>
         ≃≃([yout = match nth_error xs n with None => false | _ => true end],
              withSpace match nth_error xs n with
              | Some x => [|Contains _ (skipn (S n) xs); Contains _ (n - (S (length xs))); Contains _ x|]
              | None => [|Contains _ (skipn (S n) xs); Contains _ (n - (S (length xs))); Void|]
              end
              (appSize (Nth'_Loop_size n xs) ss))).
  Proof.
    eapply While_SpecTReg with (PRE := fun '(xs,n,ss) => (_,_)) (INV := fun '(xs,n,ss) y => (_,_)) (POST := fun '(xs,n,ss) y => _)
       (f__step := fun '(xs,n,ss) => _) (f__loop := fun '(xs,n,ss) => _) (x := (xs,n,ss));
      clear xs n ss; intros ((xs,n),ss).
    { apply Nth'_Step_SpecT_size. }
    cbn. split.
    - intros b Hb. split.
      + destruct xs, n;inv Hb. all:cbn [nth_error]. all:tspec_ext. f_equal. cbn;nia.
      + unfold Nth'_Loop_steps. destruct xs,n;inv Hb. all:cbn;nia.
    - destruct xs as [ | ? xs'],n as [ | n']. all:intros [=].
      eexists (xs', n', _). repeat apply conj; cbn.
      all:reflexivity.
  Qed.

  Definition Nth' : pTM sig^+ bool 4 :=
    LiftTapes (CopyValue _) [|Fin0; Fin3|];;
    If (LiftTapes (Nth'_Loop) [|Fin3; Fin1; Fin2|])
       (Return (LiftTapes (Reset _) [|Fin3|];;
                LiftTapes (Reset _) [|Fin1|]
               ) true)
       (Return (LiftTapes (Reset _) [|Fin3|];;
                LiftTapes (Reset _) [|Fin1|]
               ) false)
  .

  Definition Nth'_size {sigX X : Type} {cX : codable sigX X} (l : list X) (n : nat) :=
    [| id;
       (Nth'_Loop_size n l)[@Fin1] >> Reset_size (n - (S (length l)));
       (Nth'_Loop_size n l)[@Fin2];
       CopyValue_size l >> (Nth'_Loop_size n l)[@Fin0] >> Reset_size (skipn (S n) l)
     |].


  Definition Nth'_steps {sigX X : Type} {cX : codable sigX X} (l : list X) (n : nat) :=
    3 + CopyValue_steps l + Nth'_Loop_steps l n + Reset_steps (skipn (S n) l) + Reset_steps (n - S (length l)).


  Lemma Nth'_SpecT_size (xs : list X) (n : nat) (ss : Vector.t nat 4) :
    TripleT
      (≃≃([],withSpace ([|Contains _ xs; Contains _ n; Void; Void|]) ss))
      (Nth'_steps xs n) Nth'
      (fun yout =>
    ≃≃([yout = match nth_error xs n with None => false | _ => true end],
      withSpace match nth_error xs n with
      | Some x => [|Contains _ xs; Void; Contains _ x;Void|]
      | None => [|Contains _ xs; Void; Void;Void|]
      end
       (appSize (Nth'_size xs n) ss))).
  Proof.
    unfold Nth'.
    hstep; cbn. hstep; cbn. apply CopyValue_SpecT_size.
    cbn. intros _. eapply If_SpecTReg; cbn.
    - hstep; cbn. eapply ConsequenceT_pre. apply Nth'_Loop_SpecT_size. tspec_ext. reflexivity.
    - cbn. destruct (nth_error xs n) as [ x | ]. all:hintros [=].
      hstep; cbn. hstep; cbn. hstep; cbn. apply Reset_SpecT_space with (X := list X).
      cbn. intros []. eauto. hstep; cbn. apply Reset_SpecT_space with (X := nat). reflexivity.
      cbn. intros _. cbn. tspec_ext.
    - cbn. destruct (nth_error xs n) as [ x | ]. all:hintros [=].
      hstep; cbn. hstep; cbn. hstep; cbn. apply Reset_SpecT_space with (X := list X).
      cbn. intros []. eauto. hstep; cbn. apply Reset_SpecT_space with (X := nat). reflexivity.
      cbn. intros _. tspec_ext.
    - cbn. destruct b;reflexivity.
    - unfold Nth'_steps. lia.
  Qed.

  Section Legacy.

    Definition Nth'_Rel : pRel sig^+ bool 4 :=
      fun tin '(yout, tout) =>
        forall (l : list X) (n : nat) s0 s1 s2 s3,
          tin[@Fin0] ≃(;s0) l ->
          tin[@Fin1] ≃(;s1) n ->
          isVoid_size tin[@Fin2] s2 ->
          isVoid_size tin[@Fin3] s3 ->
          match yout with
          | true =>
            exists (x : X),
            nth_error l n = Some x /\
            tout[@Fin0] ≃(;(Nth'_size l n)[@Fin0]s0) l /\
            isVoid_size tout[@Fin1] ((Nth'_size l n)[@Fin1]s1) /\
            tout[@Fin2] ≃(;(Nth'_size l n)[@Fin2]s2) x /\
            isVoid_size tout[@Fin3] ((Nth'_size l n)[@Fin3]s3)
          | false =>
            nth_error l n = None /\
            tout[@Fin0] ≃(;(Nth'_size l n)[@Fin0]s0) l /\
            isVoid_size tout[@Fin1] ((Nth'_size l n)[@Fin1]s1) /\
            isVoid_size tout[@Fin2] ((Nth'_size l n)[@Fin2]s2) /\
            isVoid_size tout[@Fin3] ((Nth'_size l n)[@Fin3]s3)
          end.

    Lemma Nth'_Realise : Nth' Nth'_Rel.
    Proof.
      repeat (eapply RealiseIntroAll;intro). eapply Realise_monotone.
      -eapply TripleT_Realise. eapply Nth'_SpecT_size with (ss:=[| _;_;_;_|]) (xs:=x) (n:=x0).
      -cbn. unfold Nth'_Rel. intros ? [] H **. modpon H.
      {unfold "≃≃",withSpace;cbn. intros i; destruct_fin i;cbn. exact H3. all:eassumption. }
      repeat destruct _;unfold "≃≃",withSpace in H;cbn in H.
      all:destruct H as [Heq H].
      2,3:discriminate Heq.
      all:specializeFin H;eauto 6.
    Qed.

    Definition Nth'_T : tRel sig^+ 4 :=
      fun tin k => exists (l : list X) (n : nat),
          tin[@Fin0] l /\
          tin[@Fin1] n /\
          isVoid tin[@Fin2] /\ isVoid tin[@Fin3] /\
          Nth'_steps l n <= k.

    Lemma Nth'_Terminates : projT1 Nth' Nth'_T.
    Proof.
      repeat (eapply TerminatesInIntroEx;intro). eapply TerminatesIn_monotone.
      -eapply TripleT_TerminatesIn. eapply TripleT_RemoveSpace,Nth'_SpecT_size.
      -intros ? k H **. modpon H.
      split. 2:eassumption.
      unfold "≃≃",withSpace;cbn. intros i; destruct_fin i;cbn. all:assumption.
    Qed.
  End Legacy.

End Nth'.

Arguments Nth'_steps {sigX X cX} : simpl never.
Arguments Nth'_size {sigX X cX} : simpl never.