LTactics

Require Export Lvw internalize_def.
Require Import Tactics_old Reflection ListTactics.

Create HintDb LProc discriminated.

Create HintDb LCor discriminated.


(*Used Hint-databases:
LProc : (for auto) proofing that terms are proc/closed/value
LCor : TODO: documentation
LDef : Rewrite: L-Encoding-Definitions

cbv : everything else related with L-terms (should not be used for the crush etc. automatisation, we want more control and only use the other databases)
 *)


Tactic Notation "destruct" "_" :=
  match goal with
    | [ |- context[match ?X with _ => _ end] ] => destruct X
  end.


Tactic Notation "destruct" "*" :=
  repeat destruct _.


Ltac addToList a l := AddFvTail a l.


Lemma rho_dcls n s : dclosed (S n) s -> dclosed n (rho s).

Proof.

  unfold rho,r.
intros H. repeat (apply dcllam || apply dclApp || apply dclvar);try assumption;try omega.
Qed.


Lemma closed_dcl_x x s: closed s -> dclosed x s.

Proof.

  intros.
apply (@dclosed_ge 0). now apply closed_dcl. omega.
Qed.


Ltac has_no_evar s := try (has_evar s;fail 1).


Ltac reflexivity' :=
  match goal with
    | |- ?G => has_no_evar G;reflexivity
  end.


Ltac fvalue :=intros;
  match goal with
    | [ |- proc _ ] => split;try fvalue
    | [ |- lambda _ ] => eexists; reflexivity
    | [ |- closed _ ] => vm_compute; reflexivity
  end.


Ltac value' :=
  match goal with
    | |- lambda (match ?c with _ => _ end) => destruct c;now repeat value';fail 1
    | |- lambda (@enc ?t ?H ?x) => exact (proc_lambda (@proc_enc t H x));fail 1
    | |- lambda (@int ?X ?tt ?x ?H) => exact (proc_lambda (@proc_t X tt x H));fail 1
    | |- lambda _ => (apply proc_lambda;(trivial with nocore LProc || tauto)) || tauto || (eexists;reflexivity);fail 1
    | |- rClosed ?phi _ => solve [apply rClosed_decb_correct;[assumption|vm_compute;reflexivity]]
| |- Lvw.closed _ => apply closed_dcl
    | |- dclosed _ (match ?c with _ => _ end) => destruct c;now repeat value';fail 1
    | |- dclosed _ (Lvw.var _) => solve [constructor;omega]
    | |- dclosed _ (Lvw.app _ _) => constructor
    | |- dclosed _ (Lvw.lam _) => constructor
    | |- dclosed _ (rho ?s) => apply rho_dcls
    | |- dclosed ?k (@int ?X ?tt ?x ?H) =>
      exact (closed_dcl_x k (proc_closed (@proc_t X tt x H)));fail 1
    | |- dclosed ?k (@enc ?t ?H ?x) =>
      exact (closed_dcl_x k (proc_closed (@proc_enc t H x)));fail 1
    | |- dclosed _ ?s => let H := fresh in assert (H:closed s) by (trivial with LProc || (apply proc_closed;trivial with LProc || tauto) || tauto );exact (closed_dcl_x _ H);fail 1
  end.


(* tauto for assumptions and theyr instantiation*)
Ltac value :=
  match goal with
      |- proc _ => split;[|now value];value
    | |- closed _ => try abstract (repeat value')
    | |- lambda _ => value'
  end.


Ltac allVars' vars _s :=
match _s with
| var ?_n => vars
| app ?_s ?_t =>
  let vars := allVars' vars _s in
  allVars' vars _t
| lam ?_s => allVars' vars _s
| _ => addToList (_s:term) (* cast is for coersions to work *) vars
end.


Ltac allVars _s := allVars' (@nil term) _s.


Ltac Find_at' a l :=
  match l with
  | (cons a _) => constr:(0)
  | (cons _ ?l) =>
    let n := Find_at' a l in
    constr:(S n)
  end.


Ltac reifyTerm vars _s :=
  match _s with
    | var ?_n => constr:(rVar _n)
    | app ?_s ?_t =>
      let _s := reifyTerm vars _s in
      let _t := reifyTerm vars _t in
      constr:(rApp _s _t)
    | lam ?_s =>
      let _s := reifyTerm vars _s in
      constr:(rLam _s)
    | _ =>
      let vars' := eval hnf in vars in
          let _n := (Find_at' (_s:term) (* cast is for coersions to work *) vars') in
          constr:(rConst (_n))
  end.


Ltac vm_hypo :=
  match goal with
    | H: ?s == ?t |- _ => revert H;try vm_hypo;intros H; vm_compute in H
  end.


Ltac ProcPhi' H :=
  let eq := fresh "eq" in
  (exfalso;exact H) || (destruct H as [eq|H];[rewrite <-eq;(now value)|ProcPhi' H]).


Ltac ProcPhi :=
  let H := fresh "H" in
  let s := fresh "s" in
  apply liftPhi_correct;intros s H;simpl in H;ProcPhi' H.


Tactic Notation "standardize" ident(R) constr(n) constr(s) :=
  let vars:= allVars s in
  let s' := reifyTerm vars s in
  let phi := fresh "phi" in
  pose (phi := Reflection.liftPhi vars);
  let pp := fresh "pp" in
  let cs := fresh "cs" in
  assert (pp:Proc phi) by ProcPhi;
  assert (cs :rClosed phi s') by (apply rClosed_decb_correct;[exact pp|vm_compute;reflexivity]);
  assert (R := rStandardize n pp cs);
  let s'' := fresh "s''" in
  let eq := fresh "eq" in
  remember ((rDeClos (rCompSeval n (rCompClos s' [])))) as s'' eqn:eq;
  vm_compute in eq;
  rewrite eq in R;
  unfold rReduce in R; lazy -[phi liftPhi] in R;
  lazy [phi liftPhi nth] in R;
  clear eq s'' cs phi pp.


Ltac standardizeGoal' _n:=
  let R:= fresh "R" in
  match goal with (* try etransitivity is for debugging, so we can disable ProcPhi iff needed*)
    | |- ?s == _ => let R:= fresh "R" in standardize R _n s;try (etransitivity;[exact (star_equiv R)|];clear R)
    | |- ?s >* _ => let R:= fresh "R" in standardize R _n s;try (etransitivity;[exact R|];clear R)
  end.


Ltac standardizeGoal _n :=
  try progress standardizeGoal' _n;
    try progress (symmetry;standardizeGoal' _n;symmetry).


Lemma stHypo s s' t : s >* s' -> s == t -> s' == t.

Proof.

  intros R R'.
rewrite R in R'. exact R'.
Qed.


Ltac standardizeHypo _n:=
match goal with
  | eq_new_name : ?s == ?t |- _=>
    revert eq_new_name;try standardizeHypo _n; intros eq_new_name;
    try (progress (let R:= fresh "R" in
                   standardize R _n s;apply (stHypo R) in eq_new_name;clear R ));
      try (progress (let R':= fresh "R'" in
                     symmetry;standardize R' _n s;
                     apply (stHypo R') in eq_new_name;symmetry;clear R' ))
end.


(* for fcrush... *)
Ltac useHypo' :=
match goal with
  | eq : _ == _ |- _ == _=> rewrite eq
  (*| eq : _ == ?s |- _ >* _=> rewrite !eq Todo: do if ?s is value*)
  | eq : _ >* _ |- _ == _=> rewrite eq
  | eq : _ >* _ |- _ >* _=> rewrite eq
end.


(* TODO: use hypo should use Lrewrite, so unify that*)
Ltac useHypo := repeat (progress useHypo').


(*
Ltac reify vars phi pp:=
  collectVars vars;
  pose (phi := liftPhi vars);assert (pp:Proc phi);| reifyGoal phi vars ; repeat reifyHypo phi vars.

Ltac crush1 := let vars := fresh "vars" in
               let phi := fresh "phi" in
               let pp := fresh "pp" in reify vars phi pp.
 *)

Ltac fcrush' _n:= try standardizeGoal _n ; try reflexivity';
                  try ((progress standardizeHypo _n);repeat (progress (useHypo;standardizeGoal _n)); try reflexivity').


Ltac fcrush := intros;try autorewrite with LDef in *;(try vm_hypo;vm_compute;fcrush' 100).

(*
Hint Extern 0 (proc _) => value : LCor.
Hint Extern 0 (lambda _) => value : LCor.
Hint Extern 0 (closed _) => value : LCor.
*)

(* use correctnes lemmas also for ">*" *)
(*
Hint Extern 0 => solve apply equiv_lambda;[|solve [trivial with LCor nocore]];value : LCor.
 *)


(* ugly hack, but works for fixed-arity-functions*)

Ltac solve_proc :=
  match goal with
  | |- proc _ => value || fail 1
  | |- _ => idtac
  end.


Ltac Lrewrite'' :=(eassumption;try reflexivity;try value) || (try trivial with LCor nocore;
    match goal with
    | |- @int ?X ?ty ?x ?H >* _ => (eapply (@correct_t X ty x H);cbn;solve_proc)
    | |- app (@int ?X ?ty ?x ?H) _ >* _ => (eapply (@correct_t X ty x H);cbn;solve_proc)
    | |- app (app (@int ?X ?ty ?x ?H) _) _ >* _ => (eapply (@correct_t X ty x H);cbn;solve_proc)
    | |- app (app (app (@int ?X ?ty ?x ?H) _) _) _>* _ => (eapply (@correct_t X ty x H);cbn;solve_proc)
    | |- app (app (app (app (@int ?X ?ty ?x ?H) _) _) _) _ >* _ => (eapply (@correct_t X ty x H);cbn;solve_proc)
    (* for correctness-lemma premisses:*)
    | |- _ == _ => apply star_equiv
    | H:_|- _ >* _ => eapply H;try reflexivity;try value
    | |- app ?s ?t >* _ => apply star_step_app_proper
    | |- _ >* _ => reflexivity
  end).


Ltac Lrewrite' :=
  match goal with
    | |- ?s == _ => is_evar s;fail 1
    | |- ?s >* _ => is_evar s;fail 1
    | _ => repeat progress (etransitivity;[repeat Lrewrite''|(try instantiate (1:=Logic.I));cbn])
  end.


Ltac Lrewrite := repeat autounfold with LCor in *;(Lrewrite');try (symmetry;(Lrewrite');symmetry).


Tactic Notation "Lrewrite" "in" hyp(_H) :=
  match type of _H with
    | _ == _ => eapply stHypo in _H;[|Lrewrite;reflexivity]
    | _ >* _ => idtac "not supported yet"
  end.


Ltac wcrush' _n := intros;try reflexivity';try standardizeGoal _n ; try reflexivity'.


Ltac wcrush := wcrush' 100.


(* crush uses correctnes lemmas and wcrush*)
Ltac crush' := try Lrewrite;try wcrush' 100.


(*crush that uses correctnes lemmas*)
Ltac crush := intros;repeat crush';try reflexivity'.


Ltac crushHypo := standardizeHypo 100.


Ltac dec :=
  match goal with
    | [ |- context[decision ?X] ] => decide X
  end.


Tactic Notation "closedRewrite" :=
  match goal with
    | [ |- context[subst ?s _ _] ] =>
      let cl := fresh "cl" in assert (cl:closed s);[value|rewrite !cl;clear cl]
                                                     
  end.


Tactic Notation "closedRewrite" "in" hyp(h):=
  match type of h with
    | context[subst ?s _ _] =>
      let cl := fresh "cl" in assert (cl:closed s);[value|rewrite !cl in h;clear cl]
  end.


Tactic Notation "redStep" "at" integer(pos) := rewrite step_value at pos;[simpl;try closedRewrite|value].


Tactic Notation "redStep" "in" hyp(h) "at" integer(pos) := rewrite step_value in h at pos;[simpl in h;try closedRewrite in h|value].

(*
Tactic Notation "redStep" := redStep at 1.
*)

Tactic Notation "redStep" "in" hyp(h) := redStep in h at 1.


(* register needed lemmas:*)

Lemma rho_correct s t : proc s -> lambda t -> rho s t >* s (rho s) t.

Proof.

  intros.
unfold rho, r. redStep at 1. apply star_trans_l. crush.
Qed.


Hint Extern 0 (app (rho _) _ >* _) => apply rho_correct;value : LCor.


(*
Lemma R_correct s t : proc s -> proc t -> R s t == s (lam (R s 0)) t.
Proof.
  fcrush.
Qed.*)


(* Hint Rewrite R_correct rho_correct': LCor. *)

Lemma rho_inj s t: rho s = rho t -> s = t.

Proof.

  unfold rho,r.
congruence.
Qed.


Lemma rho_lambda s : lambda (rho s).

Proof.

  eexists.
reflexivity.
Qed.


Lemma rho_cls s : closed s -> closed (rho s).

Proof.

  intros.
value.
Qed.


Hint Resolve rho_lambda rho_cls : LProc.


Tactic Notation "recStep" constr(P) "at" integer(i):=
  match eval lazy [P] in P with
      | rho ?rP => unfold P;rewrite rho_correct at i;[|value..];fold P;try unfold rP
  end.


Tactic Notation "recStep" constr(P) :=
  intros;recStep P at 1.


(*
Lemma rClosed_closed s: recProc s -> proc s.
  intros ? [? ?]. subst. split; auto with LProc.
Qed.

Hint Resolve rClosed_closed : LProc cbv.
 *)


Lemma I_proc : proc I.

  fvalue.

Qed.


Lemma K_proc : proc K.

  fvalue.

Qed.


Lemma omega_proc : proc omega.

  fvalue.

Qed.


Lemma Omega_closed : closed Omega.

  fvalue.

Qed.


Hint Resolve I_proc K_proc omega_proc Omega_closed: LProc.


Hint Unfold I K : LCor.


Definition convI s := {v|proc v /\ s >* v}.


Lemma intFEquiv ty (tt:TT ty) f s s': internalizesF s tt f -> s == s' -> internalizesF s' tt f.

Proof.

  revert s s'.
induction tt;intros ? ? H' eq;[apply equiv_lambda;try value;now rewrite <- eq, H'..|].
  intros x u pu Hu.
hnf in H'. apply H with (s:= (s u)). now apply H'. now rewrite eq.
Qed.


Lemma intFApp ty (tt:TT ty) (fty : ty -> Type) (ftt : forall x, TT (fty x)) f s x t:
  internalizesF s (TyAll tt ftt) f -> internalizesF t tt x -> proc t -> internalizesF (s t) (ftt x) (f x).

Proof.

  intros H K pt.
now apply H.
Qed.


Instance intApp' ty (tt:TT ty) (fty : ty -> Type) (ftt : forall x, TT (fty x)) f x (Hf : internalizedClass (TyAll tt ftt) f) (Hx : internalizedClass tt x) v (R : (int f) (int x) >* v) (pv : proc v) : internalizedClass (ftt x) (f x).

Proof.

  unfold int in R.
destruct Hf, Hx. exists v. tauto. eapply intFEquiv. eapply intFApp; eassumption. rewrite <- R. reflexivity.
Defined.


Lemma intApp ty (tt:TT ty) (fty : ty -> Type) (ftt : forall x, TT (fty x)) f x (Hf : internalizedClass (TyAll tt ftt) f) (Hx : internalizedClass tt x) v (R : (int f) (int x) >* v) (pv : proc v) :
  (int f) (int x) >* int (H:=intApp' R pv)(f x).

Proof.

  rewrite R.
destruct Hf, Hx. reflexivity.
Qed.


Lemma intAppTest ty (tt:TT ty) (fty : ty -> Type) (ftt : forall x, TT (fty x)) f x (Hf : internalizedClass (TyAll tt ftt) f) (Hx : internalizedClass tt x) v (R : (int f) (int x) >* v) (pv : proc v) u:
  u >* int x -> (int f) u >* int (H:=intApp' R pv)(f x).

Proof.

  intros R'.
rewrite R'. apply intApp.
Qed.