From Undecidability.L Require Export Util.L_facts.
From Undecidability.L.Tactics Require Export LClos_Eval.
From Undecidability.L.Tactics Require Import mixedTactics.
Require Import FunInd.


Open Scope LClos.

Inductive rTerm : Type :=
| rVar (x : ) : rTerm
| rApp (s : rTerm) (t : rTerm) : rTerm
| rLam (s : rTerm)
| rConst (x : ) : rTerm
| rRho (s : rTerm).

Coercion rApp : rTerm >-> Funclass.

Definition denoteTerm (phi : term) :rTermterm :=
  fix denoteTerm s :=
    match s with
    | rVar n var n
    | rApp s t app (denoteTerm s) (denoteTerm t)
    | rLam s lam (denoteTerm s)
    | rConst n n
    | rRho s (denoteTerm s)
    end.

Definition Proc phi := (n:) , proc ( n).

Definition rClosed phi s:= Proc closed (denoteTerm s).

Definition rPow phi n s t :=
  denoteTerm s >(n) denoteTerm t.

Lemma rReduceIntro phi l s t : Proc rClosed s rClosed t denoteTerm s >(l) denoteTerm t rPow l s t.
Proof.
  unfold rPow;tauto.
Qed.


Inductive rComp : Type :=
| rCompVar (x:)
| rCompApp (s : rComp) (t : rComp) : rComp
| rCompClos (s : rTerm) (A : list rComp) : rComp.

Coercion rCompApp : rComp >-> Funclass.

Definition denoteComp (phi : term) :rComp Comp:=
  fix denoteComp s :=
    match s with
    | rCompVar x CompVar x
    | rCompApp s t (denoteComp s) (denoteComp t)
    | rCompClos s A CompClos (denoteTerm s) (map denoteComp A)
    end.

Fixpoint rSubstList (s:rTerm) (x:) (A: list rTerm): rTerm :=
  match s with
  | rVar n if Dec ( n < x )then rVar n else nth (n-x) A (rVar n)
  | rApp s t (rSubstList s x A) (rSubstList t x A)
  | rLam s rLam (rSubstList s (S x) A)
  | rRho s rRho (rSubstList s (S x) A)
  | rConst x rConst x
  end.

Fixpoint rDeClos (s:rComp) : rTerm :=
  match s with
  | rCompVar x rVar x
  | rCompApp s t (rDeClos s) (rDeClos t)
  | rCompClos s A rSubstList s 0 (map rDeClos A)
  end.

Definition rComp_ind_deep'
           (P : rComp Prop)
           (Pl : list rComp Prop)
           (IHVar : x : , P (rCompVar x))
           (IHApp : s : rComp, P s t : rComp, P t P (s t))
           (IHClos : (s : rTerm) (A : list rComp),
               Pl A P (rCompClos s A))
           (IHNil : Pl nil)
           (IHCons : (a:rComp) (A : list rComp),
               P a Pl A Pl (a::A))
           (x:rComp) : P x :=
  (fix f c : P c:=
     match c with
     | rCompVar x IHVar x
     | rCompApp s t IHApp s (f s) t (f t)
     | rCompClos s A IHClos s A
                              ((fix g A : Pl A :=
                                  match A with
                                    [] IHNil
                                  | a::A IHCons a A (f a) (g A)
                                  end) A)
     end) x
.

Definition rComp_ind_deep
           (P : rComp Prop)
           (IHVar : x : , P (rCompVar x))
           (IHApp : s : rComp, P s t : rComp, P t P (s t))
           (IHClos : (s : rTerm) (A : list rComp),
               ( a, a A P a) P (rCompClos s A)) : x, P x.
Proof.
  apply rComp_ind_deep' with (Pl:= A ( a, a A P a));auto.
  -intros. inv ;auto.
Qed.


Definition rValidComp phi s := Proc validComp (denoteComp s).

Lemma rSubstList_correct phi s x A: Proc denoteTerm (rSubstList s x A) = substList (denoteTerm s) x (map (denoteTerm ) A).
Proof.
  revert x. induction s; intros;simpl.
  - decide (x < ); decide ( > x); try ;intuition (try congruence);simpl.
    now rewrite map_nth with (f:= denoteTerm ).
  -now rewrite ,.
  -now rewrite IHs.
  -rewrite substList_closed. auto. apply H.
  -rewrite IHs. 2:tauto. reflexivity.
Qed.


Lemma map_ext' : (A B : Type) (f g : A B) (l:list A),
    ( a : A, a l f a = g a) map f l = map g l.
Proof.
  intros. induction l.
  -reflexivity.
  -simpl. rewrite H;auto. f_equal. apply IHl. intros. apply H. auto.
Qed.


Lemma denoteTerm_correct phi s: Proc deClos (denoteComp s) = denoteTerm (rDeClos s).
Proof.
  intros pp. unfold denoteComp, rDeClos. pattern s. apply rComp_ind_deep;intros;simpl;try congruence.
  -rewrite rSubstList_correct;auto. f_equal.
   rewrite !map_map. now apply map_ext'.
Qed.


Definition rCompBeta s t :=
  match s,t with
  |rCompClos (rLam ls) A,rCompClos (rLam lt) B Some (rCompClos ls (t::A))
  |rCompClos (rLam ls) A,rCompClos (rConst x) B Some (rCompClos ls (t::A))
  |rCompClos (rLam ls) A,rCompClos (rRho lt) B Some (rCompClos ls (t::A))
  |_,_ None
  end.

Definition rCompAppCount :=
   (j : ) (u v : * rComp) let (l, u0) := u in let (k, v0) := v in (j + (l + k), ).

Fixpoint rCompSeval' n (u : *rComp) : ( *rComp)*bool:=
  match n with
    S n
    match u with
    | (l, rCompApp s t)
      match rCompSeval' n (0,s),rCompSeval' n (0,t) with
        (i, s',true),(j, t',true)
        match rCompBeta s' t' with
          Some u rCompSeval' n ((S l)+(i+j),u)
        | None ((l+(i+j),s' t'),false)
        end
      | ((i,s'),_),((j,t'),_) ((l+(i+j),s' t'),false)
      end
    | (l, rCompClos (rApp s t) A )
      rCompSeval' n (l, rCompApp (rCompClos s A) (rCompClos t A))
    | (l , rCompClos (rVar x) A ) (l,nth x A (rCompVar x),true)
    | (l, rCompClos (rConst x) A ) (u,true)
    | (l, rCompVar x ) (u,true)
    | (l, rCompClos (rLam _) A) (u,true)
    | (l, rCompClos (rRho _) A) (u,true)
    end
  | 0 (u,true)
  end.

Definition rCompSeval n u : (*rComp):=
  (fst (rCompSeval' n u)).

Lemma rCompBeta_sound phi (s t u: rComp) : Proc rCompBeta s t = Some u denoteComp (s t) >[(1)] denoteComp u.
Proof with simpl in *;try congruence;auto.
  intros pp eq. destruct s... destruct s... destruct t... destruct ; inv eq...
  -constructor. apply pp.
  -constructor. eexists. reflexivity.
Qed.


Functional Scheme := Induction for rCompSeval' Sort Prop.

Lemma rCompSeval_sound n phi s l:
  Proc let (k,t) := rCompSeval n (l,s) in k l denoteComp s >[(k-l)] denoteComp t.
Proof with (repeat inv_validComp;repeat (eassumption || constructor || intuition|| subst ; eauto using star || rewrite Nat.sub_diag in * || rewrite minus_n_O in *||cbn in * )).
  intros. unfold rCompSeval.
  pose (p:= (l,s)).
  change (let (k, t) := fst (rCompSeval' n p) in k fst p denoteComp (snd p) >[(k-(fst p))] denoteComp t).
  generalize p. clear l s p. intros p.
  functional induction (rCompSeval' n p); intros;cbn...
  -rewrite , in *... eapply rCompBeta_sound in ;try eauto. destruct (rCompSeval' _ (S _,_ ));destruct p... eapply (CPow_trans (t:= denoteComp (s' t')))...
  -rewrite , in *... eapply (CPow_trans (t:= denoteComp (s' t')))...
  -rewrite , in *... eapply (CPow_trans (t:= denoteComp (s' t')))...
  -rewrite , in *... eapply (CPow_trans (t:= denoteComp (s' t')))...
  -rewrite map_nth...
  -repeat destruct (rCompSeval' _ _)... destruct p... eapply CPow_trans...
Qed.


Lemma rCompBeta_rValidComp s t u phi : rValidComp s rValidComp t rCompBeta s t = Some u rValidComp u.
Proof with repeat (congruence || subst || simpl in * || intuition ).
  unfold rValidComp in *. intros vs vt eq. assert (pp:Proc )by (inv vs;auto). split;auto. unfold rCompBeta in eq. destruct s... destruct s... destruct t... destruct ...
  -inv eq. inv ; inv . constructor... rewrite map_length in *. now inv .
  -inv eq. inv ; inv . constructor...
   +destruct (pp x) as [_ H']. inv H'. now rewrite .
   +rewrite map_length in *. now inv .
  -inv eq. inv ; inv . constructor...
   +rewrite map_length in *. now inv .
   +rewrite map_length in *. now inv .
Qed.


Lemma rCompSeval_rValidComp n s phi k : Proc rValidComp s rValidComp (snd (rCompSeval n (k,s))).
Proof with repeat (eapply validCompApp ||apply validCompClos || congruence || subst || simpl in * || intuition).
  intros P. unfold rCompSeval. revert s k. induction n; intros s k [? vs];(split;[auto|])... destruct s;try now inv vs;cbn...
  -inv vs. assert ( := IHn 0 ). assert ( := IHn 0).
   unfold snd,fst in *. do 2 destruct ((rCompSeval' n (_,_)))... destruct p,... unfold rValidComp in *. destruct b,... destruct (rCompBeta r ) eqn:eq;unfold rValidComp in *.
   +apply IHn... eapply rCompBeta_rValidComp;eauto; unfold rValidComp in *...
   +idtac...
  -unfold rValidComp in *. inv vs. destruct s;simpl...
   +rewrite map_nth. apply . apply nth_In. now inv .
   +apply IHn;auto. simpl in *. split;auto. inv . repeat constructor...
Qed.


Lemma rClosed_valid s phi : Proc (rClosed s rValidComp (rCompClos s [])).
Proof.
  intros pp. unfold rClosed. unfold rValidComp. rewrite closed_dcl. split;intros H.
  -repeat constructor;simpl;intuition;apply .
  -inv H. inv . now tauto.
Qed.


Lemma expandDenote phi s: Proc denoteTerm s = deClos (denoteComp (rCompClos s [])).
Proof.
  intros pp. rewrite (denoteTerm_correct _ pp). simpl. rewrite rSubstList_correct;auto. simpl. now rewrite substList_nil.
Qed.


Lemma rDeClos_reduce phi s: Proc rValidComp s deClos (denoteComp s) = deClos (denoteComp (rCompClos (rDeClos s) [])).
Proof.
  intros pp vc. simpl. rewrite denoteTerm_correct;auto. now rewrite substList_nil.
Qed.


Lemma rDeClos_rValidComp phi s: Proc rValidComp s rValidComp (rCompClos (rDeClos s) []).
Proof with repeat (eauto || congruence || subst || simpl in * || intuition).
  intros pp [? H]. unfold rValidComp in *. split;try tauto. simpl. apply deClos_valComp in H. apply validComp_closed. now rewrite denoteTerm_correct.
Qed.


Lemma rStandardize n phi s : Proc rClosed s let (l,s') := (rCompSeval n (0,rCompClos s [])) in rPow l s (rDeClos s').
Proof with eauto.
  intros pp cl. unfold rPow. rewrite rClosed_valid in *;auto. assert (cl': rValidComp (snd (rCompSeval n (0,rCompClos s [])))).
  -apply rCompSeval_rValidComp;auto.
  - destruct rCompSeval eqn:. rewrite !expandDenote;auto. specialize (rCompSeval_sound n (rCompClos s []) 0 pp);intros H. rewrite in H.
    destruct H as [_ H]. rewrite minus_n_O in H. rewrite rDeClos_reduce... apply deClos_correct... destruct cl...
Qed.


Lemma rStandardizeUsePow n phi s:
  Proc rClosed s
  let (l,s') := (rCompSeval n (0,rCompClos s [])) in denoteTerm s >(l) denoteTerm (rDeClos s').
Proof.
  apply rStandardize.
Qed.


Lemma rStandardizeUse n phi s:
  Proc rClosed s
  let (l,s') := (rCompSeval n (0,rCompClos s [])) in denoteTerm s >* denoteTerm (rDeClos s').
Proof.
  intros a b.
  specialize (rStandardizeUsePow n a b). destruct (rCompSeval _ _). rewrite star_pow. firstorder.
Qed.


Fixpoint rClosed_decb' n u : bool:=
  match u with
  | rApp s t andb (rClosed_decb' n s) (rClosed_decb' n t)
  | rVar x negb (leb n x)
  | rConst x true
  | rLam s rClosed_decb' (S n) s
  | rRho s rClosed_decb' (S n) s
  end.

Lemma rClosed_decb'_correct s phi n: Proc rClosed_decb' n s = true bound n (denoteTerm s).
Proof.
  intros pp. revert n. induction s;intros n eq;simpl in *.
  -rewrite Bool.negb_true_iff in eq. apply leb_complete_conv in eq. now constructor.
  -rewrite Bool.andb_true_iff in eq. constructor; intuition.
  -constructor. auto.
  -apply bound_ge with (k:=0);[|]. rewrite closed_dcl. apply pp.
  -unfold ,r.
   repeat (eapply dclApp||eapply dcllam||eapply dclvar).
   all:try . eauto.
Qed.


Definition rClosed_decb s:= rClosed_decb' 0 s.

Lemma rClosed_decb_correct phi s : Proc rClosed_decb s = true rClosed s.
Proof.
  intros. hnf;split;[auto|]. rewrite closed_dcl. apply rClosed_decb'_correct;auto.
Qed.



Definition liftPhi Vars n:=nth n Vars I.

Arguments liftPhi Vars n/.

Lemma liftPhi_correct Vars: ( s, s Vars proc s) Proc (liftPhi Vars).
Proof.
  intros H n. unfold liftPhi. destruct (nth_in_or_default n Vars I) as [?|eq].
  -now apply H.
  -rewrite eq. cbv. split. auto. eexists. eauto.
Qed.


Fixpoint benchTerm x : rTerm :=
  match x with
    0 (rLam (rVar 0))
  | S x (rLam (benchTerm x)) (rLam (rVar 0))
  end.

Close Scope LClos.