From Undecidability.L Require Import Tactics.LTactics Datatypes.LSum Datatypes.LOptions.
From Undecidability.L Require Export Prelim.LoopSum.

Section uiter.
  Variable X Y : Type.
  Context `{registered X}.
  Context `{registered Y}.

  Variable f : X -> X + Y.

  Variable fT : timeComplexity (X -> X + Y).
  Context `{computableTime' f fT}.

  Import HOAS_Notations.
  Definition uiter := Eval cbn -[enc] in rho [L_HOAS (λ uiter x, !!(extT f) x (λ x' _ , uiter x') (λ y _ , y) !!I)].

  Lemma uiter_proc : proc uiter.
  Proof. unfold uiter. Lproc. Qed.
  Hint Resolve uiter_proc : LProc.

  Fixpoint uiterTime n x :=
    match n with
      0 => 0
    | S n' => fst (fT x tt) + 9 + match f x with
                                       inl x' => uiterTime n' x'
                                     | _ => 0
                                     end
    end.

  Lemma uiter_sound n x y:
    loopSum n f x = Some y -> evalLe (uiterTime n x) (app uiter (enc x)) (enc y).
  Proof.
    unfold uiter. Intern.recRem P.
    induction n in x|-*;intros Heq. now easy.
    cbn in Heq|-*.
    eapply (@le_evalLe_proper (match f x with inl x' => _ | _ => _ end)).
    2,3:reflexivity.
    2:{
      destruct (f x) eqn:eqfx.
      -Intern.recStepNew P. Lsimpl. rewrite eqfx. Lsimpl. eapply IHn. eauto.
      -inv Heq. Intern.recStepNew P. Lsimpl. rewrite eqfx. Lsimpl. Lreflexivity.
    }
    destruct (f x).
    all:solverec.
  Qed.


  Lemma uiter_total_instanceTime {Z} `{registered Z} (f': Z -> Y) (preprocess : Z -> X) preprocessT (fuel : Z -> nat)
    `{computableTime' preprocess preprocessT} :
    (forall x, loopSum (fuel x) f (preprocess x) = Some (f' x)) ->
    computesTime (TyArr _ _) f' (convert (λ x, !!uiter (!!(extT preprocess) x))) (fun z _ => (1 + fst (preprocessT z tt) + uiterTime (fuel z) (preprocess z),tt)).
  Proof.
    cbn [convert TH "-"].
    intros total.
    eapply computesTimeTyArr_helper with (time:=(fun x _ => _)).
    { unfold uiter. now Lproc. }
    intros z []. cbn. split. now reflexivity.
    intros ? ->.
    eexists. split. 2:reflexivity.
    eapply le_evalLe_proper. 2-3:reflexivity.
    2:{ eapply evalLe_trans with (t := (L.app uiter (enc (preprocess z)))).
        -now Lsimpl.
        -eapply uiter_sound. apply total. }
    cbn.
    lia.
  Qed.

  Lemma uiterTime_bound_onlyByN (P: nat -> _ -> Prop) boundL boundR n0 x0:
    (forall n x, n < n0
            -> P n x
            -> match f x with
              | inl x' => P (S n) x' /\ fst (fT x tt) <= boundL
              | inr y => forall n', n <= n' -> fst (fT x tt) <= boundL + boundR n'
              end) ->
    P 0 x0 ->
    uiterTime n0 x0 <= n0 * (boundL + 9) + boundR n0.
  Proof.
    intros H'.
    pose (n0':=n0). assert (Hleq : n0<=n0') by (cbn;lia).
    replace 0 with (n0'-n0) at 1 by (cbn;lia).
    change (boundR n0) with (boundR n0').
    change n0 with n0' in H'.
    clearbody n0'.
    induction n0 in x0,Hleq |-*. 1:cbn;Lia.nia.
    intros HPx.
    cbn -[plus].
    specialize H' with (x:=x0).
    destruct (f x0).
    -edestruct H' as [? ->]. 2:eassumption. lia. rewrite IHn0. 2:easy.
     now Lia.lia.
     replace (n0'-n0) with (S (n0'-S n0)) by Lia.nia. eapply H2.
    -rewrite H' with (n:=n0'-S n0) (n':=n0'). all:try now Lia.lia. eassumption.
  Qed.

  Lemma uiterTime_bound_recRel2 (P: nat -> _ -> Prop) (iterT : X -> nat):
    (forall i x, P i x -> match f x with
                    | inl x' => P (S i) x' /\ iterT x' + 9 + fst (fT x tt) <= iterT x
                    | inr y => fst (fT x tt) + 9 <= iterT x
                    end) ->
    forall n x,
      P 0 x ->
      uiterTime n x <= iterT x.
  Proof.
    intros H' n x.
    pose (n':=n). assert (Hleq : n<=n') by (cbn;lia).
    replace 0 with (n'-n) at 1 by (cbn;lia).
    clearbody n'.
    induction n in x,Hleq |-*. 1:cbn;Lia.nia.
    intros HPx.
    cbn -[plus].
    specialize H' with (x:=x).
    destruct (f x) as [x'|y] eqn:eq.
    -edestruct H' as [? H'']. eassumption. rewrite IHn.
2:easy. 2:{ replace (n'-n) with (S (n'-S n)) by Lia.nia. eassumption. } Lia.lia.
    -cbn. rewrite <- H'. 2:easy. all:Lia.lia.
  Qed.

  Lemma uiterTime_bound_recRel (P: nat -> _ -> Prop) (iterT : nat -> X -> nat) n:
    (forall i x, P i x -> match f x with
                    | inl x' => P (S i) x' /\ iterT (n-i-1) x' + 9 + fst (fT x tt) <= iterT (n-i) x
                    | inr y => fst (fT x tt) + 9 <= iterT (n-i) x
                    end) ->
    forall x k,
      k <= n ->
      P (n-k) x ->
      uiterTime k x <= iterT k x.
  Proof.
    intros H' x k.
    induction k in x |-*.
    1:now cbn;Lia.nia.
    intros ? HPx.
    cbn -[plus].
    specialize H' with (x:=x).
    destruct (f x) as [x'|y] eqn:eq.
    -edestruct H' as [? H'']. eassumption. rewrite IHk.
     +replace (n - (n - (S k))) with (1+k) in H'' by Lia.lia.
      cbn in H''. rewrite Nat.sub_0_r in H''.
      Lia.nia.
     +easy.
     +replace (n-k) with (S (n-S k)) by Lia.nia. eassumption.
    -replace (S k) with (n - (n - S k)) by Lia.lia.
     rewrite <- H'. all:easy.
  Qed.

  Lemma uiterTime_computesRel (R : X -> X -> Prop) x0 k0 (t__step t__end : nat):
    (forall k' x, k' < k0 -> pow R k' x0 x ->
             fst (fT x tt) <= t__step + match f x with
                                       | inr _ => t__end | _ => 0
                                       end
             /\ match f x with
                | inl x' => R x x'
                | _ => True
                end) ->
    uiterTime k0 x0 <= k0 * (t__step + 9) + t__end.
  Proof.
    intros H'.
    rewrite uiterTime_bound_onlyByN
      with (P:= fun n x =>pow R n x0 x)
           (boundL := t__step)
           (boundR := fun _ => t__end).
    -Lia.lia.
    -intros n x lt'' R'.
     specialize H' with (1:=lt'') (2:=R') as [H' H''].
     destruct (f x).
     +split. 2:easy.
      replace (S n) with (n+1) by lia.
      eapply pow_add. eexists x. split. eauto. apply rcomp_1 with (R:=R). tauto.
     +intro. lia.
    -reflexivity.
  Qed.

End uiter.

Hint Resolve uiter_proc : LProc.
Arguments uiter _ _ _ _ _ _ _ : clear implicits.
Arguments uiter {X Y H H0} f {fT H1}.