Require Import Undecidability.Shared.Libs.PSL.Bijection MetaCoq.Template.All Strings.Ascii.
From Undecidability.L Require Import Prelim.StringBase.
From Undecidability.L.Tactics Require Import Lproc Computable ComputableTime Lsimpl mixedTactics Lbeta Lrewrite.
Require Export Ring Arith Lia.
Import L_Notations.

Module Intern.

Ltac visibleHead t :=
  match t with
    ?h _ => visibleHead h
  | _ => t
  end.

Ltac fold_encs :=
  match goal with
    x:_ |- _ =>
    revert x;fold_encs;intros x;
    let H := fresh "H" in
    try (assert (H:@enc _ _ x= @enc _ _ x) by reflexivity;
         try (unfold enc in H at 1; cbn in H;rewrite !H);clear H)
  | _ => idtac
  end.

Ltac recRem P:=
  match goal with
  | |- context[rho ?s] =>
    let rP := fresh "rP" in
    set (rP:=s);
    assert (proc rP);[unfold rP;solve [Lproc]|
                      set (P := rho rP);
                      assert (proc P);[unfold P;solve [Lproc]|]]
end.

Ltac recStepInit P:=
   once lazymatch eval lazy [P] in P with
   | rho ?rP =>
     once lazymatch goal with
     | |- evalLe _ _ _ =>
       let rec loop :=
           once lazymatch goal with
           | |- ARS.pow step _ (app P _) _ =>unfold P;apply rho_correctPow;now Lproc
           | |- ARS.pow step _ (app _ _) _ => eapply pow_step_congL;[loop|reflexivity]
           end
       in
       eapply evalLe_trans;[apply pow_redLe_subrelation;loop|fold P; unfold rP]
     | |- evalIn _ _ _ =>
       let rec loop :=
           once lazymatch goal with
           | |- ARS.pow step _ (app P _) _ =>unfold P;apply rho_correctPow;now Lproc
           | |- ARS.pow step _ (app _ _) _ => eapply pow_step_congL;[loop|reflexivity]
           end
       in
       eapply evalIn_trans;[loop|fold P; unfold rP]
     | |- eval _ _ =>
       let rec loop :=
           once lazymatch goal with
           | |- ARS.star step (app P _) _ =>unfold P;apply rho_correct;now Lproc
           | |- ARS.star step (app _ _) _ => eapply star_step_app_proper;[loop|reflexivity]
           end
       in
       eapply eval_helper;[loop|fold P; unfold rP]
     end
   end.

Ltac recStepNew P := recStepInit P.

Ltac destructRefine :=
  once lazymatch goal with
    |- ?R ?s _ =>
    match s with
    | context C [match ?x with _ => _ end]=>
      let t := type of x in
      refine (_:R _ ((fun y:t => ltac:(destruct y)) x));
      
      once lazymatch goal with
        |- (?R' ?i ?s1 ?s2) => tryif is_evar i then
          refine (_:R' ((fun (y:t) => ltac:(destruct y)) x ) s1 s2)
        else idtac
      | _ => idtac
      end;
      once lazymatch goal with
       | |- ?R2 ?i ?s ?t =>
         let i':= eval cbn zeta in i in
             refine (_:R2 i' s t) + match goal with |- ?G => let G' := constr:(R2 i' s t) in idtac "could not refine" G "with" G' end
       | _ => idtac
      end;
      let eq := fresh "eq" in destruct x eqn:eq
    end
  end.

Ltac shelveIfUnsolved msg:= first[let n:= numgoals in guard n=0|
                                  match goal with
                                    |- ?G => idtac "Could not solve some subgoal("msg"):";idtac G;shelve
                                  end].

Ltac ugly_fix_fix IH n :=
  
  once lazymatch eval cbn in n with
    0 => fix IH 1
  | 1 => fix IH 4
  | 2 => fix IH 7
  | 3 => fix IH 10
  | _ => let m := eval cbn in (1+3*n) in
            fail 1000 "please add '| "n" => fix IH"m"'" " in the definition of Ltac-tactic ugly_fix_fix!"
  end.

Ltac ugly_fix_fix2 IH n :=
  
  once lazymatch eval cbn in n with
    0 => fix IH 1
  | 1 => fix IH 5
  | 2 => fix IH 9
  | 3 => fix IH 13
  | _ => let m := eval cbn in (1+4*n) in
            fail 1000 "please add '| "n" => fix IH"m"'" " in the definition of Ltac-tactic ugly_fix_fix2!"
  end.

Ltac intro_to_assumed x :=
  once lazymatch goal with
    H : Lock _ |- _ =>
    let tx := type of x in
    revert x;unlock H;revert H;
    refine (_ : (forall (x:tx), _:Prop) -> _);
    intros H x;specialize (H x);lock H
  end.

Ltac split_assumed :=
  once lazymatch goal with
    H : Lock _ |- _ =>
    unlock H;
    split;[eapply proj1 in H|eapply proj2 in H];lock H
  end.

Ltac clean_assumed :=
  repeat
    once lazymatch goal with
      H : Lock (_/\_) |- ?G =>
      unlock H; apply proj2 in H;lock H
    end.

Ltac is_assumed_add :=
  once lazymatch goal with
    H : Lock _ |- ?G =>
    unlock H; refine (proj1 H);shelve
  end.

Ltac is_assumed :=
  once lazymatch goal with
    H : Lock _ |- ?G =>
    unlock H; refine H;shelve
  end.

Ltac close_assumed :=
  once lazymatch goal with
    H : Lock _ |- ?G =>unlock H;assert True by exact H
  end.

Ltac cstep' extractSimp:=
  let x := fresh "x" in
  once lazymatch goal with
  | |- computes _ _ (match ?x with _ => _ end)=>
    let eq := fresh "eq" in destruct x eqn:eq
  | |- computes (TyArr ?tt1 ?tt2) ?f ?intF=>
    let fRep := constr:(ltac:(quote_term f (fun x => exact x))) in
    once lazymatch fRep with
      
      Ast.tFix (_::_::_) => fail 1000 "mutual recursion not supported"
    | Ast.tFix [BasicAst.mkdef _ _ _ _ ?recArg] 0 =>
      (let P := fresh "P" in
      recRem P;
      eapply computesExpStart;[solve [Lproc]|];
      let n:= (eval cbn in (S recArg)) in
      let rec step n:=
          (once lazymatch n with
           | S ?n =>
              eexists;
              eapply computesExpStep;[try recStep P;extractSimp;shelveIfUnsolved "pos5"|Lproc;shelveIfUnsolved "pos6"|];
              
              let x := fresh "x" in
              let xInt := fresh x "Int" in
              let xInts := fresh x "Ints" in
              intros x xInt xInts;
              change xInt with (@ext _ _ x (Build_computable xInts));
              once lazymatch type of xInts with
                computes (@TyB _ ?reg) _ _ =>
                rewrite (ext_is_enc (Build_computable xInts)) in *;
                clear xInt xInts;assert (xInt:True) by constructor; assert (xInts:True) by constructor
              | computes (TyArr _ _) _ _ => idtac
              end;
              step n;
              revert x xInt xInts
           | 0 => idtac
           end) in
      step n;
        let IH := fresh "IH" P in
        ugly_fix_fix IH recArg;
          let rec loop n :=
              once lazymatch n with
                0 => intros [] ? ?
              | S ?n' => intros ? ? ?;loop n'
              end in
          loop recArg;
          eexists;
          (split;[try recStepNew P;extractSimp;shelveIfUnsolved "pos7"|]))

    
    | _=>
      let xInt := fresh x "Int" in
      let xNorm := fresh x "Norm" in
      let xInts := fresh x "Ints" in
      let vProc := fresh "vProc" in
      
      eapply computesTyArr;[try Lproc;shelveIfUnsolved "pos1"|idtac];
      intros x xInt xInts;
      change xInt with (@ext _ _ x (Build_computable xInts));
      once lazymatch tt1 with
        TyB _ => rewrite (ext_is_enc (Build_computable xInts)) in *;
                clear xInt xInts;assert (xInt:True) by constructor; assert (xInts:True) by constructor
      | _ => idtac
      end;
      eexists;split;[extractSimp;shelveIfUnsolved "pos2" | intros vProc]
    end

  | |- computes (TyB _) _ ?t=> has_no_evar t;apply computesTyB

  | |- computes _ _ (@ext _ _)=> apply extCorrect


  
  | H : Lock _ |- computesTime _ _ (match ?x with _ => _ end) _=>
    let t := type of x in
    unlock H;revert H;(refine (_: ((fun z:t => ltac:(destruct z):Prop) x) -> _);intros H;lock H);
    let eq := fresh "eq" in destruct x eqn:eq
  | H:Lock _ |- computesTime (TyArr ?tt1 ?tt2) ?f ?intF ?T=>
    let fRep := constr:(ltac:(quote_term f (fun x => exact x))) in
    once lazymatch fRep with
      Ast.tFix (_::_::_) => fail 1000 "mutual recursion not supported"
    | Ast.tFix [BasicAst.mkdef _ _ _ _ ?recArg] 0 =>
      let P := fresh "P" in
      let H' := fresh H "'" in
      recRem P;
      eapply computesTimeExpStart;[solve [Lproc]|];
      let n:= (eval cbn in (S recArg)) in
      let rec step n:=
          (once lazymatch n with
           | S ?n' =>
              eexists;
              let x := fresh "x" in
              let xInt := fresh x "Int" in
              let xT := fresh x "T" in
              let xInts := fresh x "Ints" in
              (refine (computesTimeExpStep (fT:=fun x xT => _) _ _ _ _) ;
               [|try recStepNew P;extractSimp;shelveIfUnsolved "pos8"|Lproc;shelveIfUnsolved "pos9"|]);
              [try reflexivity;is_assumed_add|];clean_assumed;
              
              intros x xInt xT; intro_to_assumed x;intro_to_assumed xT;intro xInts;
              change xInt with (@extT _ _ x _ (Build_computableTime xInts));
              once lazymatch type of xInts with
                computesTime (@TyB _ ?reg) _ _ _=>
                rewrite (extT_is_enc (Build_computableTime xInts)) in *;
                destruct xT;
                clear xInt xInts;assert (xInt:True) by constructor; assert (xInts:True) by constructor; assert (xT:True) by constructor
              | computesTime (TyArr _ _) _ _ _=> idtac
              end;
              step n';
              revert x xInt xT xInts
           | 0 => idtac
           end) in
      step n;
        
      let IH := fresh "IH" P in
      ugly_fix_fix2 IH recArg;
        let rec loop n :=
            (clean_assumed;
             let x := fresh "x" in
             let xT := fresh x "T" in
             intros x ? xT ? ;
             let tx := type of x in
             let txT := type of xT in
             unlock H; revert H;refine (_ : (forall (x:_) (xT:_) , (_ :Prop)) -> _ );
             intros H;specialize (H x xT);lock H;
             once lazymatch n with
               0 => unlock H;revert H;(refine (_: ((fun z:tx => ltac:(destruct z):Prop) x) -> _);intros H;lock H);
                   eexists (ltac:(destruct x));destruct x;(split;unlock H;
                   [
                     once lazymatch goal with
                       |- evalLe ?k _ _ =>
                       refine (le_evalLe_proper _ eq_refl eq_refl _);[refine (proj1 H);shelve|apply proj2 in H;lock H];
                       try recStepNew P;extractSimp;shelveIfUnsolved "pos10"
                     end
                    |apply proj2 in H;lock H])
             | S ?n' => loop n'
             end ) in
        loop recArg
    
    | _ =>
      let xInt := fresh x "Int" in
      let xNorm := fresh x "Norm" in
      let xInts := fresh x "Time" in
      let xInts := fresh x "Ints" in
      let xT := fresh x "T" in
      let vProc := fresh "vProc" in
      
      eapply computesTimeTyArr_helper with (time := fun x xT => _);[try Lproc;shelveIfUnsolved "pos3"|];
      intros x xT;intro_to_assumed x;intro_to_assumed xT;
      split_assumed;[now is_assumed|];
      intros xInt xInts;
      change xInt with (@extT _ _ x _ (Build_computableTime xInts));
      once lazymatch tt1 with
        TyB _ => rewrite (extT_is_enc (Build_computableTime xInts)) in *;
                clear xInt xInts;assert (xInt:True) by constructor; assert (xInts:True) by constructor
      | _ => idtac
      end;
      eexists;split;[extractSimp;shelveIfUnsolved "pos4"| intros vProc]
    end
  

  | H : Lock _ |- computesTime (TyB _) _ ?t ?tt=> has_no_evar t;close_assumed; destruct tt;apply computesTimeTyB
  | H : Lock _ |-computesTime _ _ (@extT _ _) _ => apply extTCorrect

  | |- computesTime _ _ _ _ =>
    match goal with
    | H : Lock _ |- _ => fail 1
    | |- _ =>
      refine (computesTimeIfStart (P:= fun fT => _) _ _);
      [let H := fresh "H" in
       let fT := fresh "fT" in
       intros fT H; lock H|]
    end
  end.

Tactic Notation "progress'" tactic(t) :=
  once lazymatch goal with
    | |- ?R ?s _ =>idtac "now";print_goal;
    t tt;idtac"then";print_goal;
    once lazymatch goal with
      |- R s _ => fail "noprogress"
    | |- _ => idtac
    end
  end.

Ltac extractCorrectCrush :=
  idtac;
   try Lsimpl;try Lreflexivity;
   try repeat' (repeat' Intern.destructRefine;Lsimpl;try Lreflexivity);
  try Lreflexivity.

Ltac extractSimple :=
  lazymatch goal with
    |- eval _ _ => extractCorrectCrush
  | |- evalLe _ _ _ => extractCorrectCrush
  | |- evalIn _ _ _ => Lsimpl_old;fail "evalIn does not support full Lrewrite and should only occur when simplifying rho/recursion"
  | |- ?G => idtac "cstep found unexpected" G
  end;try (idtac;[idtac "could not simplify some occuring term, shelved instead"];shelve).

Ltac cstep := cstep' extractSimple.

Ltac computable_match:=
  intros;
  once lazymatch goal with
  | |- ?R ?lhs ?rhs =>
    once lazymatch lhs with
    | context C [@enc _ ?reg ?x] =>
      induction x;
      let encf := (eval hnf in (@enc _ reg)) in
      change (@enc _ reg) with encf;
      cbn -[enc];
      repeat change encf with (@enc _ reg);
      fold_encs;
      Lsimpl_old
    end
  end.

Ltac infer_instances :=
  repeat match goal with
         | [ |- context [ int_ext ?t ] ] => first [change (int_ext t) with (ext t) | fail 3 "Could not fold int-instance for " t]
         | [ |- context [ extT ?t ] ] => first [change (extT t) with (ext t) | fail 3 "Could not fold int-instance for " t]
         end.

Ltac infer_instancesT :=
  repeat match goal with
         | [ |- context [ int_ext ?t ] ] => first [change (int_ext t) with (extT t) | fail 3 "Could not fold extT-instance for " t]
         | [ |- context [ ext ?t ] ] => first [change (ext t) with (extT t) | fail 3 "Could not fold extT-instance for " t]
         end.

Ltac computable_prepare t :=
  let h := visibleHead t in
  tryif is_const h then unfold h else idtac.

Ltac computable_using_noProof Lter:=
  once lazymatch goal with
  | [ |- computable ?t ] =>
    eexists Lter;unfold Lter;try clear Lter;
    let t' := eval hnf in t in
        let h := visibleHead t' in
        try unfold h;computable_prepare t;infer_instances
  | [ |- computableTime ?t _] =>
    eexists Lter;unfold Lter;try clear Lter;
    let t' := (eval hnf in t) in
    let h := visibleHead t' in
    try unfold h; computable_prepare t; infer_instancesT
  end.

Ltac extractAs s :=
  once lazymatch goal with
  | [ H : @extracted _ |- _ ] => idtac "WARNING: extraction is buggy if used while a term of type 'extracted _' is in Context"
  | [ |- computable ?t ] =>
    (run_template_program (tmExtract None t)
                         (fun e => pose (s:= ( e : extracted t))))
  | [ |- computableTime ?t _] =>
    (run_template_program (tmExtract None t)
                         (fun e => pose (s:= ( e : extracted t))))
  end.

Ltac extractThis t s :=
    (run_template_program (tmExtract None t)
                         (fun e => pose (s:= ( e : extracted t)))).

End Intern.

Import Intern.

Ltac register_inj := abstract (intros x; induction x; let y := fresh "y" in destruct y;simpl; intros eq; try (injection eq || discriminate eq);intros;f_equal;auto;try apply inj_enc;try easy).

Ltac register_proc :=
  solve [
  unfold enc_f; let x := fresh "x" in
  (((intros x;induction x || intros *);
    cbn; fold_encs;Lproc
                        ))].

Ltac register encf := refine (@mk_registered _ encf _ _);[
                          (((let x := fresh "x" in induction x || intros);(let f := visibleHead encf in unfold f;cbn [f]);
                            fold_encs;Lproc
                        )) | try register_inj].

Tactic Notation "computable" "using" open_constr(Lter) :=
  computable_using_noProof Lter;repeat cstep.

Tactic Notation "computable" "instead" open_constr(t) :=
  let s := fresh "s" in
  extractThis t s; computable using s.

Tactic Notation "computable" "infer" :=
  once lazymatch goal with
  | [ |- computable ?t ] =>
    let e := constr:(int_ext t) in let e' := eval unfold int_ext in e in computable using e'
  | [ |- computableTime ?t _] =>
    let e := constr:(int_ext t) in let e' := eval unfold int_ext in e in computable using e'
  end.

Tactic Notation "extract" :=
  unshelve
    let term := fresh "used_term" in
    extractAs term;computable using term.

Tactic Notation "extract" "constructor":=
  let term := fresh "used_term" in
        once lazymatch goal with
        | [ |- computable ?t ] =>
          run_template_program (tmExtractConstr' None t)
                                 (fun e => pose (term:= ( e : extracted t)); computable using term)
        | [ |- computableTime ?t _] =>
          run_template_program (tmExtractConstr' None t)
                               (fun e => pose (term:= ( e : extracted t)); computable using term)
          
   end.

Tactic Notation "extract" "match" := computable_match.

Lemma recRel_prettify_drop A B C:
  (A -> B) -> (A -> (C -> B)).
Proof.
  tauto.
Qed.

Lemma recRel_prettify_forall X (P Q : X -> Prop) :
  (forall x, Q x -> P x) -> ((forall x, Q x) -> (forall x, P x)).
Proof.
  firstorder.
Qed.

Lemma recRel_prettify_conj (P P' Q Q' : Prop) :
  (P-> P') -> (Q -> Q') -> (P /\ Q -> P' /\ Q').
Proof.
  firstorder.
Qed.

Lemma recRel_prettify_conj_drop_r (P P' Q' : Prop) :
  Q' -> (P-> P') -> (P -> (P' /\ Q')).
Proof.
  firstorder.
Qed.

Lemma recRel_prettify_rel X R (x x' y y' : X):
  x = x' -> y = y' -> (R x' y' -> R x y).
Proof.
  firstorder congruence.
Qed.

Ltac recRel_ring_simplify_arith_enterRel :=
  once lazymatch goal with
    |- _ -> ?R ?x ?y =>
    let X := type of x in
    let x' := fresh "x'" in
    let y' := fresh "y'" in
    evar (x' : X);
    evar (y' : X);
    refine (@recRel_prettify_rel X R x x' y y' _ _);subst x' y'
  end.

Ltac recRel_prettify_arith_step :=
  progress
    once lazymatch goal with
    
    | |- _ -> (_ /\ _) =>
      refine (@recRel_prettify_conj _ _ _ _ _ _)
    | |- _ -> (forall (x:?t),@?P x) =>
      let x := fresh "x" in
      refine (@recRel_prettify_forall t P (fun (x:t) => _) _)
      ;intros x
    | |- _ -> match ?x with _ => _ end =>
      let t := type of x in
      refine (_:(((fun y : t => ltac:(destruct y)) x : Prop) -> _));

      once lazymatch t with
        nat => destruct x;
            [
            once lazymatch goal with
              |- ?G -> _ =>
              let H := fresh in
              pose G as H; instantiate (1:=ltac:(clear x)) in (value of H); subst H
            end|]
      | _ => destruct x
      end
                     
    | |- _ -> (?x <= ?y)%nat =>
      recRel_ring_simplify_arith_enterRel
    | |- match ?x with _ => _ end = ?evar =>
      let t := type of x in
      refine (_:(_ = ((fun y : t => ltac:(destruct y)) x)));

      once lazymatch t with
        nat => destruct x;
            [
            once lazymatch goal with
              |- _ = ?G =>
              let H := fresh in
              pose G as H; instantiate (1:=ltac:(clear x)) in (value of H); subst H
            end|]
      | _ => destruct x
      end
    | |- ?x = ?evar =>
      ring_simplify x;
      let rec patternMatches:= once lazymatch goal with
                                 |- context C [match _ with _ => _ end] =>
                                 let C' := constr:(fun y => ltac:(let C' := context C[y] in exact C')) in
                                 refine (@eq_rect _ _ C' _ _ _);[patternMatches|symmetry]
                               | |- _ => reflexivity
                               end
      in patternMatches
    | |- _ -> _ => exact (@impl_Reflexive _)
    | |- _ => idtac "DEBUG";print_goal
    end.

Ltac recRel_prettify_arith_loop := repeat recRel_prettify_arith_step;[>idtac "recRel_prettify_arith_step";shelve..].

Ltac recRel_prettify_arith_prepare := cbn [id fst snd];
                                      eapply Basics.apply.

Ltac recRel_prettify_arith :=
  recRel_prettify_arith_prepare;[recRel_prettify_arith_loop|cbn beta].

Ltac recRel_prettify := recRel_prettify_arith.

 Ltac recRel_prettify2 :=
      cbn [timeComplexity fst snd] in *;
      (repeat (intros; intuition idtac;
               repeat match goal with
                      | t:unit |- _ =>
                        destruct t
                      end;
               try (let H:= fresh "H" in destruct _ eqn:H)));cbn [fst snd];ring_simplify.

Local Ltac solverecTry := cbn [timeComplexity] in *;
                                (repeat (intros; intuition idtac;
                                         repeat match goal with
                                                | t:unit |- _ =>
                                                  destruct t
                                                end;
                                         try (let H:= fresh "H" in destruct _ eqn:H);cbn -[mult plus];try ring_simplify);try lia).
Ltac solverec := try abstract (solverecTry);solverecTry.

Lemma cast_computable X Y `{registered Y} (cast : X -> Y) (Hc : injective cast) :
  let _ := registerAs cast Hc in
  computable cast.
Proof.
  cbn.
  pose (t:=lam 0).
  computable using t.
Qed.

Lemma cast_computableTime X Y `{registered Y} (cast : X -> Y) (Hc : injective cast):
  let _ := registerAs cast Hc in
  computableTime' cast (fun _ _ => (1,tt)).
Proof.
  cbn.
  pose (t:=lam 0).
  computable using t. solverec. Unshelve.
Defined.
Ltac computable_casted_result :=
  match goal with
    |- @computable _ _ _ =>
    simple notypeclasses refine (cast_registeredAs _ _);
    [ | | | |
      cbn - [registerAs];reflexivity| ];
    cbn
  | |- @ComputableTime.computableTime _ _ _ _=>
    simple notypeclasses refine (cast_registeredAs_TimeComplexity _ _);
    [ | | | |
      cbn - [registerAs];reflexivity| ];
    cbn
  end.