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.
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.