From Undecidability.L Require Export Tactics.Computable.


Fixpoint timeComplexity t (tt: TT t) : Type :=
  match tt with
    ! _ unit
  | @TyArr timeComplexity (*timeComplexity )
  end.

Arguments timeComplexity : clear implicits.
Arguments timeComplexity _ {_}.

Fixpoint computesTime {t} (ty : TT t) : (x:t) (xInt :term) (xTime :timeComplexity t), Type :=
  match ty with
    !_ x xInt _ xInt = enc x
  | @TyArr
     f fInt fTime
      proc fInt *
       (y : ) yInt (yTime:timeComplexity ),
        computesTime y yInt yTime
         let fyTime := fTime y yTime in
          {v : term & (redLe (fst fyTime) (app fInt yInt) v) * computesTime (f y) v (snd fyTime)}
  end%type.

Arguments computesTime {_} _ _ _ _.

Class computableTime {X : Type} (ty : TT X) (x : X) evalTime: Type :=
  {
    extT : extracted x;
    extTCorrect : computesTime ty x extT evalTime
  }.

Global Arguments computableTime {X} {ty} x.
Global Arguments extT {X} {ty} x {_ computableTime} : simpl never.
Global Arguments extTCorrect {X} ty x {_ computableTime} : simpl never.
Definition evalTime X ty x evalTime (computableTime : @computableTime X ty x evalTime):=evalTime.
Global Arguments evalTime {X} {ty} x {evalTime computableTime}.

#[export] Hint Extern 3 (@extracted ?t ?f) let ty := constr:(_ : TT t) in notypeclasses refine (extT (ty:=ty) f) : typeclass_instances.
#[export] Hint Mode computableTime + - + -: typeclass_instances.
Notation "'computableTime'' f" := (@computableTime _ ltac:(let t:=type of f in refine (_ : TT t);exact _) f) (at level 0,only parsing).


Local Fixpoint notHigherOrder t (ty : TT t) :=
  match ty with
    TyArr _ _ (TyB _ _) notHigherOrder
  | TyB _ _ True
  | _ False
  end.

Local Lemma computesTime_computes_intern s t (ty: TT t) f evalTime:
  notHigherOrder ty computesTime ty f s evalTime computes ty f s.
Proof.
  revert s f.
  induction ty;intros s f H int.
  - exact int.
  -destruct ; cbn in H. 2:tauto.
   clear .
   cbn. destruct int as [ps ints]. cbn in ints.
   split. tauto.
   intros. subst.
   edestruct (ints a _ tt eq_refl) as(v&R'&?).
   exists v. split. eapply redLe_star_subrelation. all:eauto.
Defined.

Lemma computableTime_computable X (ty : TT X) (x:X) fT :
  notHigherOrder ty computableTime x fT computable x.
Proof.
  intros H I. eexists (extT x). destruct I. eapply computesTime_computes_intern. all:eauto.
Defined.

#[export] Hint Extern 10 (@computable ?t ?ty ?f)
(solve [let H:= fresh "H" in eassert (H : @computableTime t ty f _) by exact _;
                        ( (exact (computableTime_computable (ty:=ty) Logic.I H))|| idtac "Can not derive computable instance from computableTime for higher-order-function" f)]): typeclass_instances.

Lemma computesTimeProc t (ty : TT t) (f : t) fInt fT:
  computesTime ty f fInt fT proc fInt.
Proof.
  destruct ty.
  -intros . unfold enc. now destruct R.
  -now intros [? _].
Qed.


Lemma proc_extT {X : Type} (ty : TT X) (x : X) fT ( H : computableTime x fT) : proc (extT x).
Proof.
  unfold extT. destruct H as [? H]. now eapply computesTimeProc in H.
Qed.


#[global]
Instance reg_is_extT ty (R : registered ty) (x : ty): computableTime x tt.
Proof.
  exists (enc x). split;constructor.
Defined.

Lemma computesTimeTyB (t:Type) (x:t) `{registered t}: computesTime (TyB t) x (extT x) tt.
Proof.
  unfold extT. now destruct H.
Qed.


#[global]
Instance extTApp' t1 t2 {tt1:TT } {tt2 : TT } (f: ) (x:) fT xT (Hf : computableTime f fT) (Hx : computableTime x xT) : computableTime (f x) (snd (fT x xT)).
Proof.
  destruct Hf as [fInt H], Hx as [xInt xInts].
  eexists ( ((snd H) x xInt xT xInts)).
  destruct H as [p fInts]. cbn in *.
  destruct (fInts x xInt xT xInts) as (v&E&fxInts).
  eassumption.
Defined.

Lemma extTApp t1 t2 {tt1:TT } {tt2 : TT } (f: ) (x:) fT xT (Hf : computableTime f fT) (Hx : computableTime x xT) :
  app (extT f) (extT x) >(<= fst (evalTime f x (evalTime x))) extT (f x).
Proof.
  unfold extT.
  destruct Hf as [fInt [fP fInts]], Hx as [xInt xInts]. cbn.
  destruct (fInts x xInt xT xInts) as (v&E&fxInts). apply E.
Qed.


Lemma extT_is_enc t1 (R:registered ) (x: ) xT (Hf : computableTime x xT) :
  @extT _ _ x xT Hf = enc x.
Proof.
  unfold extT.
  destruct Hf. assumption.
Defined.

Lemma computesTimeTyArr_helper t1 t2 (tt1 : TT ) (tt2 : TT ) f fInt time fT:
  proc fInt
  
  ( (y : ) yT,
      (time y yT fst (fT y yT)) *
   (yInt : term),
    computesTime y yInt yT
     {v : term & evalLe (time y yT) (app fInt yInt) v * (proc v computesTime (f y) v (snd (fT y yT)))})%type
computesTime ( ~> ) f fInt fT.
Proof.
  intros H. split. tauto.
  intros y yInt yT yInts.
  specialize (H y yT) as (lt&H).
  edestruct H as (v&E&Hv). eassumption.
  exists v.
  split. rewrite lt. now apply E.
  apply Hv.
  apply evalLe_eval_subrelation in E. split. rewrite E. apply app_closed. apply . apply computesTimeProc in yInts. apply yInts. apply E.
Qed.


Definition computesTimeIf {t} (ty : TT t) (f:t) (fInt : term) (P:timeComplexity t Prop) : Type :=
   fT, P fT computesTime ty f fInt fT.
Arguments computesTimeIf {_} _ _ _ _.

Lemma computesTimeIfStart t1 (tt1 : TT ) (f : ) (fInt : term) P fT:
  computesTimeIf f fInt P P fT computesTime f fInt fT.
Proof.
  intros ?. cbn. eauto.
Qed.


Definition computesTimeExp {t} (ty : TT t) (f:t) (s:term) (i:) (fInt : term) (fT:timeComplexity t) : Type :=
  evalLe i s fInt * computesTime ty f fInt fT.

Arguments computesTimeExp {_} _ _ _ _ _ _.

Lemma computesTimeExpStart t1 (tt1 : TT ) (f : ) (fInt : term) fT:
  proc fInt
  {v :term & computesTimeExp f fInt 0 v fT} computesTime f fInt fT.
Proof.
  intros ? (?&[e lam]&?). decide (fInt=x). subst x. assumption.
  edestruct n. destruct e as ([]&?&?). assumption. inv .
Qed.


Lemma computesTimeExpStep t1 t2 (tt1 : TT ) (tt2 : TT ) (f : ) (s:term) k k' fInt fT:
  k' = k evalIn k' s fInt closed s
  ( (y : ) (yInt : term) yT, computesTime y yInt yT
                                 {v : term & computesTimeExp (f y) (app s yInt) (fst (fT y yT) +k) v (snd (fT y yT))}%type)
  computesTimeExp ( ~> ) f s k fInt fT.

Proof.
  intros (&) ? H. split. split. eexists;split. 2:eassumption. . tauto. split. split. 2:tauto. rewrite . tauto.
  intros y yInt yT yInted.
  edestruct (H y yInt yT yInted) as (v&&?).
  eexists v. split.
  edestruct (evalLe_trans_rev) as (&). exact . apply pow_step_congL. eassumption. reflexivity.
  destruct fT. cbn in *. replace (n+k-k) with n in by . apply . tauto.
Qed.


Lemma computesTimeExt X (tt : TT X) (x x' : X) s fT:
  extEq x x' computesTime tt x s fT computesTime tt x' s fT.
Proof.
  induction tt in x,x',s,fT |-*;intros eq.
  -inv eq. tauto.
  -cbn in eq|-*. intros [ ]. split. 1:tauto.
   intros y t yT ints.
   specialize ( y t yT ints ) as (v&R&).
   exists v. split. 1:assumption.
   eapply . 2:now eassumption.
   apply eq.
Qed.


Lemma computableTimeExt X (tt : TT X) (x x' : X) fT:
  extEq x x' computableTime x fT computableTime x' fT.
Proof.
  intros ? [s ?]. eexists. eauto using computesTimeExt.
Defined.

Fixpoint changeResType_TimeComplexity t1 (tt1 : TT ) Y {R: registered Y} {struct }:
   (fT: timeComplexity ) , @timeComplexity _ ( (changeResType (TyB Y))):= (
  match with
    @TyB _ fT fT
  | TyArr _ _ fT x xT (fst (fT x xT),changeResType_TimeComplexity (snd (fT x xT)))
  end).

Lemma cast_registeredAs_TimeComplexity t1 (tt1 : TT ) Y (R: registered Y) fT (cast : (resType ) Y) (f:)
      (Hc : injective cast) :
   (resType ) = registerAs cast Hc
  computableTime (ty:= (changeResType (TyB Y))) (insertCast R cast f) (changeResType_TimeComplexity fT)
  computableTime f fT.
Proof.
  intros H [s ints].
  eexists s.
  induction in cast,f,fT,H,s,ints,Hc |- *.
  -cbn in H,ints|-*;unfold enc in *. rewrite H. exact ints.
  -destruct ints as (?&ints). split. assumption.
   intros x s__x int__x T__x.
   specialize (ints x s__x int__x T__x) as (v &?&ints).
   exists v. split. tauto.
   eapply IHtt1_2. all:eassumption.
Qed.


Definition cnst {X} (x:X):. Proof. exact 0. Qed.

Definition callTime X (fT : X unit * unit) x: := fst (fT x tt).
Arguments callTime / {_}.

Definition X Y
           (fT : X unit * (Y unit * unit)) x y : :=
  let '(k,f):= fT x tt in k + fst (f y tt).
Arguments / {_ _}.

Fixpoint timeComplexity_leq (t : Type) (tt : TT t) {struct tt} : timeComplexity t timeComplexity t Prop :=
  match tt in (TT t) return timeComplexity t timeComplexity t Prop with
  | ! _ _ True
  | @TyArr _
     f f' : timeComplexity (_ _) (x:) xT, (fst (f x xT)) (fst (f' x xT)) timeComplexity_leq (snd (f x xT)) (snd (f' x xT))
  end.

Lemma computesTime_timeLeq X (tt : TT X) x s fT fT':
  timeComplexity_leq fT fT' computesTime tt x s fT computesTime tt x s fT'.
Proof.
  induction tt in x,s,fT,fT' |-*;intros eq.
  -inv eq. tauto.
  -cbn in eq|-*. intros [ ]. split. 1:tauto.
   intros y t yT ints.
   specialize ( y t yT ints ) as (v&R&).
   exists v. specialize (eq y yT) as (Hleq&?). split.
   +rewrite Hleq. eassumption.
   +eauto.
Qed.


Lemma computableTime_timeLeq X (tt : TT X) (x:X) fT fT':
  timeComplexity_leq fT fT' computableTime x fT computableTime x fT'.
Proof.
  intros ? []. eexists. eapply computesTime_timeLeq. all:easy.
Qed.