From Undecidability.L Require Import Tactics.Computable Lproc Lbeta ComputableTime mixedTactics.
Import L_Notations.
Lemma redLe_app_helper s s' t t' u i j k:
s >(<= i) s' -> t >(<= j) t' -> s' t' >(<=k) u -> s t >(<=i+j+k) u.
Proof.
intros (i' & ? & R1) (j' & ? & R2) (k' & ? & R3).
exists ((i'+j')+k'). split. lia. apply pow_trans with (t:=s' t').
apply pow_trans with (t:=s' t).
now apply pow_step_congL.
now apply pow_step_congR. eauto.
Qed.
Lemma pow_app_helper s s' t t' u:
s >* s' -> t >* t' -> s' t' >* u -> s t >* u.
Proof.
now intros -> -> -> .
Qed.
Lemma LrewriteTime_helper s s' t i :
s' = s -> s >(<= i) t -> s' >(<= i) t.
Proof.
intros;now subst.
Qed.
Lemma Lrewrite_helper s s' t :
s' = s -> s >* t -> s' >* t.
Proof.
intros;now subst.
Qed.
Lemma Lrewrite_equiv_helper s s' t t' :
s >* s' -> t >* t' -> s' == t' -> s == t.
Proof.
intros -> ->. tauto.
Qed.
Ltac find_Lrewrite_lemma :=
once lazymatch goal with
| |- ?R (lam _) => fail
| |- ?R (enc _) => fail
| |- ?R (extT (ty:=TyB _) _) => fail
| |- ?R (ext (ty:=TyB _) _) => fail
| |- ?R ?s _ => has_no_evar s;solve [eauto 20 with Lrewrite nocore]
end.
Create HintDb Lrewrite discriminated.
Hint Constants Opaque : Lrewrite.
Hint Variables Opaque : Lrewrite.
Hint Extern 0 (proc _) => solve [Lproc] : Lrewrite.
Hint Extern 0 (lambda _) => solve [Lproc] : Lrewrite.
Hint Extern 0 (closed _) => solve [Lproc] : Lrewrite.
Lemma pow_redLe_subrelation' i s t : pow step i s t -> redLe i s t.
Proof. apply pow_redLe_subrelation. Qed.
Hint Extern 0 (_ >(<= _ ) _) => simple eapply pow_redLe_subrelation' : Lrewrite.
Hint Extern 0 (_ >* _) => simple eapply redLe_star_subrelation : Lrewrite.
Hint Extern 0 (_ >* _) => simple eapply eval_star_subrelation : Lrewrite.
Ltac Ltransitivity :=
once lazymatch goal with
| |- _ >(<= _ ) _ => refine (redLe_trans _ _);[shelve.. | | ]
| |- _ >* _ => refine (star_trans _ _);[shelve.. | | ]
| |- _ >(_) _ => eapply pow_add with (R:=step)
| |- ?t => fail "not supported by Ltransitivity:" t
end.
Ltac Lrewrite_generateGoals :=
once lazymatch goal with
| |- app _ _ >(<= _ ) _ => eapply redLe_app_helper;[instantiate;Lrewrite_generateGoals..|idtac]
| |- app _ _ >* _ => eapply pow_app_helper ;[instantiate;Lrewrite_generateGoals..|idtac]
| |- ?s >(<= _ ) _ => (is_evar s;fail 10000) ||idtac
| |- ?s >* _ => (is_evar s;reflexivity) ||idtac
end.
Ltac useFixHypo :=
once lazymatch goal with
|- ?s >* ?t =>
has_no_evar s;
let IH := fresh "IH" in
unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:term & computesExp _ _ s v}));solve [once auto with nocore]|];
let v := constr:(projT1 IH) in
assert (IHR := fst (projT2 IH));
let IHInts := constr:( snd (projT2 IH)) in
once lazymatch type of IHInts with
computes ?ty _ ?v =>
change v with (@ext _ ty _ (Build_computable IHInts)) in IHR;exact (proj1 IHR)
end
| |- ?s >(<= ?i ) ?t=>
has_no_evar s;
let IH := fresh "IH" in
unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:term & computesTimeExp _ _ s _ v _}));solve [once auto with nocore]|];
let v := constr:(projT1 IH) in
assert (IHR := fst (projT2 IH));
let IHInts := constr:( snd (projT2 IH)) in
once lazymatch type of IHInts with
computesTime ?ty _ ?v _=>
change v with (@extT _ ty _ _ (Build_computableTime IHInts)) in IHR;exact (proj1 IHR)
end
end.
Ltac LrewriteTime_solveGoals :=
try find_Lrewrite_lemma;
try useFixHypo;
once lazymatch goal with
| |- @ext _ (@TyB _ _) _ ?inted >* _ =>
(progress rewrite (ext_is_enc);[>LrewriteTime_solveGoals..]) || Lreflexivity
| |- app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => etransitivity;[apply extApp|LrewriteTime_solveGoals]
| |- app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);LrewriteTime_solveGoals
| |- @extT _ (@TyB _ _) _ _ ?inted >(<= _ ) _ =>
(progress rewrite (extT_is_enc);[>LrewriteTime_solveGoals..]) || Lreflexivity
| |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => eapply redLe_trans;
[let R := fresh "R" in
specialize (extTApp fInts xInts) as R;
once lazymatch type of R with
?s >(<= ?n) ?t => let n' := eval unfold evalTime in n in
change (s >(<= n') t) in R
end; exact R
|LrewriteTime_solveGoals]
| |- app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
change (app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);LrewriteTime_solveGoals
| |- _ >(<= _ ) _ => Lreflexivity
| |- _ >* _ => reflexivity
end.
Ltac Lrewrite' :=
once lazymatch goal with
|- ?rel ?s _ =>
once lazymatch goal with
| |- _ >(<=_) _ =>
try (eapply redLe_trans;[Lrewrite_generateGoals;[>LrewriteTime_solveGoals..]|])
| |- _ >* _ =>
try (etransitivity;[Lrewrite_generateGoals;[>LrewriteTime_solveGoals..]|])
end;
once lazymatch goal with
|- ?rel s _ => fail "No Progress (progress in indices are not currently noticed...)"
| |- _ => idtac
end
| |- _ => idtac
end.
Tactic Notation "Lrewrite_wrapper" tactic(k):=
once lazymatch goal with
| |- _ >(<= _) _ => k
| |- _ ⇓(<= _) _ => (eapply evalLe_trans;[k;Lreflexivity|])
| |- _ ⇓( _) _ => idtac "Lrewrite_prepare does not support s ⇓(k) y, only s ⇓(<=k) t)"
| |- _ >(_) _ => idtac "Lrewrite_prepare does not support s >(k) y, only s >(<=k) t)"
| |- _ >* _ => k
| |- eval _ _ => (eapply eval_helper;[k;Lreflexivity|])
| |- _ == _ => progress ((eapply Lrewrite_equiv_helper;[try k;reflexivity..|]))
end.
Ltac Lrewrite := Lrewrite_wrapper Lrewrite'.
Lemma Lrewrite_in_helper s t s' t' :
s >* s' -> t >* t' -> s == t -> s' == t'.
Proof.
intros R1 R2 E. now rewrite R1,R2 in E.
Qed.
Tactic Notation "Lrewrite" "in" hyp(_H) :=
once lazymatch type of _H with
| _ == _ => eapply Lrewrite_in_helper in _H; [ |try Lrewrite;reflexivity |try Lrewrite;reflexivity]
| _ >* _ => idtac "not supported yet"
end.
Lemma ext_rel_helper X `(H:registered X) (x:X) (inst : computable x) (R: term -> term -> Prop) u:
R (enc x) u -> R (@ext _ _ _ inst) u.
Proof.
now rewrite ext_is_enc.
Qed.
Lemma extT_rel_helper X `(H:registered X) (x:X) xT (inst : computableTime x xT) (R: term -> term -> Prop) u:
R (enc x) u -> R (@extT _ _ _ _ inst) u.
Proof.
now rewrite extT_is_enc.
Qed.
Ltac LrewriteSimpl_old':=
idtac;
(
once lazymatch goal with
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => eapply ext_rel_helper
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => eapply extT_rel_helper
| |- ?R ?s _ => has_no_evar s
end;
once lazymatch goal with
| |- ?R (L.app _ _) _ =>
(once lazymatch R with
| star step => refine (pow_app_helper _ _ _)
| redLe _ => refine (redLe_app_helper _ _ _)
end);[LrewriteSimpl_old';Lreflexivity..| ];
once lazymatch goal with
| |- _ (L.app (lam _) ?t) _ =>
let valt := fresh "valt" in
assert (valt:proc t) by Lproc;
Lbeta;
clear valt;LrewriteSimpl_old'
| |- _ =>
let appTimeHelper tt:=
(once lazymatch goal with
| |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _
=> let R := fresh "R" in
specialize (extTApp fInts xInts) as R;
once lazymatch type of R with
?s >(<= ?n) ?t => (
let n' := eval unfold evalTime in n in
change (s >(<= n') t) in R)
end; Ltransitivity;[exact R|]
end) in
once lazymatch goal with
| |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => Ltransitivity;[apply extApp|]
| |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);
Ltransitivity;[apply extApp|]
| |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => appTimeHelper tt
| |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
change (L.app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);appTimeHelper tt
| |- _ => idtac
end
end
| |- _ => idtac
end;
try repeat' (Ltransitivity;[find_Lrewrite_lemma|LrewriteSimpl_old']);
try (once (Ltransitivity;[useFixHypo|]));
once lazymatch goal with
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => eapply ext_rel_helper
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => eapply extT_rel_helper
| |- _ => idtac
end).
Lemma LrewriteTime_helper_index:
forall [s t : term] [i i' : nat], i = i' -> s >(<=i) t -> s >(<=i') t.
Proof. intros. now subst. Qed.
Lemma redLe_app_helperL s s' t u i j:
s >(<= i) s' -> app s' t >(<=j) u -> app s t >(<=i+j) u.
Proof. intros ? H'. eapply redLe_app_helper in H'. 2:eassumption. 2:Lreflexivity. now rewrite Nat.add_0_r in H'. Qed.
Lemma redLe_app_helperR s t t' u i j:
t >(<= i) t' -> app s t' >(<=j) u -> app s t >(<=i+j) u.
Proof. intros ? H'. eapply redLe_app_helper in H'. 3:eassumption. 2:Lreflexivity. eassumption. Qed.
Lemma pow_app_helperL s s' t u:
s >* s' -> app s' t >* u -> app s t >* u.
Proof. now intros -> -> . Qed.
Lemma pow_app_helperR s t t' u:
t >* t' -> app s t' >* u -> app s t >* u.
Proof. now intros -> -> . Qed.
Ltac LrewriteSimpl_appL R:=
lazymatch R with
| star step => refine (pow_app_helperL _ _)
| redLe _ => refine (redLe_app_helperL _ _)
end.
Ltac LrewriteSimpl_appR R:=
lazymatch R with
| star step => refine (pow_app_helperR _ _)
| redLe _ => refine (redLe_app_helperR _ _)
end.
Ltac appTimeHelper tt:=
(once lazymatch goal with
| |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _
=> Ltransitivity;[refine (LrewriteTime_helper_index _ (extTApp fInts xInts));[unfold evalTime;reflexivity]| ]
end ).
Ltac isValue s:=
lazymatch s with
| lam _ => idtac
| app _ _ => fail
| @ext _ _ _ _ => idtac
| @extT _ _ _ _ _ => idtac
| @enc _ _ _ => idtac
| I => idtac
| ?P => tryif (is_var P;lazymatch eval unfold P in P with rho _ => idtac end) then idtac
else
lazymatch goal with
| H : proc s |- _ => idtac
| H : lambda s |- _ => idtac
| _ => idtac
end
end.
Ltac LrewriteSimpl'' canReduceFlag :=
idtac;
once lazymatch goal with
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => refine (ext_rel_helper _ _)
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => refine (extT_rel_helper _ _)
| |- ?R ?s _ => has_no_evar s;
repeat' (idtac;
lazymatch goal with
| |- _ (lam _) _ => fail
| |- _ (enc _) _ => fail
| |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => Ltransitivity;[apply extApp|]
| |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);
Ltransitivity;[refine (extApp _ _)|]
| |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => appTimeHelper tt
| |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
change (L.app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);appTimeHelper tt
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => refine (ext_rel_helper _ _)
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => refine (extT_rel_helper _ _)
| |- ?R (L.app _ _) _ =>
let progressFlag := fresh in
let recCanReduceFlag := fresh in
let tmp := fresh in
assert (progressFlag:=tt);
assert (tmp:=tt);
assert (recCanReduceFlag:=tt);
try (LrewriteSimpl_appR R;[solve [LrewriteSimpl'' tmp;Lreflexivity]|try clear progressFlag]);
try clear tmp;
try (LrewriteSimpl_appL R;[solve [LrewriteSimpl'' canReduceFlag;Lreflexivity]|try clear progressFlag]);
lazymatch goal with
| |- ?R (L.app ?s ?t) _ =>
let maybeBeta _ := lazymatch s with lam _ => Lbeta end in
try (maybeBeta ();try clear progressFlag);
tryif (tryif is_var recCanReduceFlag then isValue t else fail)
then
try (
Ltransitivity;[solve [find_Lrewrite_lemma|useFixHypo]|];
try clear progressFlag ;
try (clear canReduceFlag;pose (canReduceFlag:=tt))
)
else clear canReduceFlag
end;
tryif is_var progressFlag then fail else idtac
| |- ?H => Ltransitivity;[solve[find_Lrewrite_lemma]|]
end)
end.
Ltac LrewriteSimpl' := let flag := fresh in assert (flag:=tt);
(tryif Lbeta then try LrewriteSimpl'' flag else LrewriteSimpl'' flag);try clear flag.
Ltac LrewriteSimpl := Lrewrite_wrapper ltac:(idtac;LrewriteSimpl').
Import L_Notations.
Lemma redLe_app_helper s s' t t' u i j k:
s >(<= i) s' -> t >(<= j) t' -> s' t' >(<=k) u -> s t >(<=i+j+k) u.
Proof.
intros (i' & ? & R1) (j' & ? & R2) (k' & ? & R3).
exists ((i'+j')+k'). split. lia. apply pow_trans with (t:=s' t').
apply pow_trans with (t:=s' t).
now apply pow_step_congL.
now apply pow_step_congR. eauto.
Qed.
Lemma pow_app_helper s s' t t' u:
s >* s' -> t >* t' -> s' t' >* u -> s t >* u.
Proof.
now intros -> -> -> .
Qed.
Lemma LrewriteTime_helper s s' t i :
s' = s -> s >(<= i) t -> s' >(<= i) t.
Proof.
intros;now subst.
Qed.
Lemma Lrewrite_helper s s' t :
s' = s -> s >* t -> s' >* t.
Proof.
intros;now subst.
Qed.
Lemma Lrewrite_equiv_helper s s' t t' :
s >* s' -> t >* t' -> s' == t' -> s == t.
Proof.
intros -> ->. tauto.
Qed.
Ltac find_Lrewrite_lemma :=
once lazymatch goal with
| |- ?R (lam _) => fail
| |- ?R (enc _) => fail
| |- ?R (extT (ty:=TyB _) _) => fail
| |- ?R (ext (ty:=TyB _) _) => fail
| |- ?R ?s _ => has_no_evar s;solve [eauto 20 with Lrewrite nocore]
end.
Create HintDb Lrewrite discriminated.
Hint Constants Opaque : Lrewrite.
Hint Variables Opaque : Lrewrite.
Hint Extern 0 (proc _) => solve [Lproc] : Lrewrite.
Hint Extern 0 (lambda _) => solve [Lproc] : Lrewrite.
Hint Extern 0 (closed _) => solve [Lproc] : Lrewrite.
Lemma pow_redLe_subrelation' i s t : pow step i s t -> redLe i s t.
Proof. apply pow_redLe_subrelation. Qed.
Hint Extern 0 (_ >(<= _ ) _) => simple eapply pow_redLe_subrelation' : Lrewrite.
Hint Extern 0 (_ >* _) => simple eapply redLe_star_subrelation : Lrewrite.
Hint Extern 0 (_ >* _) => simple eapply eval_star_subrelation : Lrewrite.
Ltac Ltransitivity :=
once lazymatch goal with
| |- _ >(<= _ ) _ => refine (redLe_trans _ _);[shelve.. | | ]
| |- _ >* _ => refine (star_trans _ _);[shelve.. | | ]
| |- _ >(_) _ => eapply pow_add with (R:=step)
| |- ?t => fail "not supported by Ltransitivity:" t
end.
Ltac Lrewrite_generateGoals :=
once lazymatch goal with
| |- app _ _ >(<= _ ) _ => eapply redLe_app_helper;[instantiate;Lrewrite_generateGoals..|idtac]
| |- app _ _ >* _ => eapply pow_app_helper ;[instantiate;Lrewrite_generateGoals..|idtac]
| |- ?s >(<= _ ) _ => (is_evar s;fail 10000) ||idtac
| |- ?s >* _ => (is_evar s;reflexivity) ||idtac
end.
Ltac useFixHypo :=
once lazymatch goal with
|- ?s >* ?t =>
has_no_evar s;
let IH := fresh "IH" in
unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:term & computesExp _ _ s v}));solve [once auto with nocore]|];
let v := constr:(projT1 IH) in
assert (IHR := fst (projT2 IH));
let IHInts := constr:( snd (projT2 IH)) in
once lazymatch type of IHInts with
computes ?ty _ ?v =>
change v with (@ext _ ty _ (Build_computable IHInts)) in IHR;exact (proj1 IHR)
end
| |- ?s >(<= ?i ) ?t=>
has_no_evar s;
let IH := fresh "IH" in
unshelve epose (IH:=_);[|(notypeclasses refine (_:{v:term & computesTimeExp _ _ s _ v _}));solve [once auto with nocore]|];
let v := constr:(projT1 IH) in
assert (IHR := fst (projT2 IH));
let IHInts := constr:( snd (projT2 IH)) in
once lazymatch type of IHInts with
computesTime ?ty _ ?v _=>
change v with (@extT _ ty _ _ (Build_computableTime IHInts)) in IHR;exact (proj1 IHR)
end
end.
Ltac LrewriteTime_solveGoals :=
try find_Lrewrite_lemma;
try useFixHypo;
once lazymatch goal with
| |- @ext _ (@TyB _ _) _ ?inted >* _ =>
(progress rewrite (ext_is_enc);[>LrewriteTime_solveGoals..]) || Lreflexivity
| |- app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => etransitivity;[apply extApp|LrewriteTime_solveGoals]
| |- app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);LrewriteTime_solveGoals
| |- @extT _ (@TyB _ _) _ _ ?inted >(<= _ ) _ =>
(progress rewrite (extT_is_enc);[>LrewriteTime_solveGoals..]) || Lreflexivity
| |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => eapply redLe_trans;
[let R := fresh "R" in
specialize (extTApp fInts xInts) as R;
once lazymatch type of R with
?s >(<= ?n) ?t => let n' := eval unfold evalTime in n in
change (s >(<= n') t) in R
end; exact R
|LrewriteTime_solveGoals]
| |- app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
change (app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);LrewriteTime_solveGoals
| |- _ >(<= _ ) _ => Lreflexivity
| |- _ >* _ => reflexivity
end.
Ltac Lrewrite' :=
once lazymatch goal with
|- ?rel ?s _ =>
once lazymatch goal with
| |- _ >(<=_) _ =>
try (eapply redLe_trans;[Lrewrite_generateGoals;[>LrewriteTime_solveGoals..]|])
| |- _ >* _ =>
try (etransitivity;[Lrewrite_generateGoals;[>LrewriteTime_solveGoals..]|])
end;
once lazymatch goal with
|- ?rel s _ => fail "No Progress (progress in indices are not currently noticed...)"
| |- _ => idtac
end
| |- _ => idtac
end.
Tactic Notation "Lrewrite_wrapper" tactic(k):=
once lazymatch goal with
| |- _ >(<= _) _ => k
| |- _ ⇓(<= _) _ => (eapply evalLe_trans;[k;Lreflexivity|])
| |- _ ⇓( _) _ => idtac "Lrewrite_prepare does not support s ⇓(k) y, only s ⇓(<=k) t)"
| |- _ >(_) _ => idtac "Lrewrite_prepare does not support s >(k) y, only s >(<=k) t)"
| |- _ >* _ => k
| |- eval _ _ => (eapply eval_helper;[k;Lreflexivity|])
| |- _ == _ => progress ((eapply Lrewrite_equiv_helper;[try k;reflexivity..|]))
end.
Ltac Lrewrite := Lrewrite_wrapper Lrewrite'.
Lemma Lrewrite_in_helper s t s' t' :
s >* s' -> t >* t' -> s == t -> s' == t'.
Proof.
intros R1 R2 E. now rewrite R1,R2 in E.
Qed.
Tactic Notation "Lrewrite" "in" hyp(_H) :=
once lazymatch type of _H with
| _ == _ => eapply Lrewrite_in_helper in _H; [ |try Lrewrite;reflexivity |try Lrewrite;reflexivity]
| _ >* _ => idtac "not supported yet"
end.
Lemma ext_rel_helper X `(H:registered X) (x:X) (inst : computable x) (R: term -> term -> Prop) u:
R (enc x) u -> R (@ext _ _ _ inst) u.
Proof.
now rewrite ext_is_enc.
Qed.
Lemma extT_rel_helper X `(H:registered X) (x:X) xT (inst : computableTime x xT) (R: term -> term -> Prop) u:
R (enc x) u -> R (@extT _ _ _ _ inst) u.
Proof.
now rewrite extT_is_enc.
Qed.
Ltac LrewriteSimpl_old':=
idtac;
(
once lazymatch goal with
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => eapply ext_rel_helper
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => eapply extT_rel_helper
| |- ?R ?s _ => has_no_evar s
end;
once lazymatch goal with
| |- ?R (L.app _ _) _ =>
(once lazymatch R with
| star step => refine (pow_app_helper _ _ _)
| redLe _ => refine (redLe_app_helper _ _ _)
end);[LrewriteSimpl_old';Lreflexivity..| ];
once lazymatch goal with
| |- _ (L.app (lam _) ?t) _ =>
let valt := fresh "valt" in
assert (valt:proc t) by Lproc;
Lbeta;
clear valt;LrewriteSimpl_old'
| |- _ =>
let appTimeHelper tt:=
(once lazymatch goal with
| |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _
=> let R := fresh "R" in
specialize (extTApp fInts xInts) as R;
once lazymatch type of R with
?s >(<= ?n) ?t => (
let n' := eval unfold evalTime in n in
change (s >(<= n') t) in R)
end; Ltransitivity;[exact R|]
end) in
once lazymatch goal with
| |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => Ltransitivity;[apply extApp|]
| |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);
Ltransitivity;[apply extApp|]
| |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => appTimeHelper tt
| |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
change (L.app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);appTimeHelper tt
| |- _ => idtac
end
end
| |- _ => idtac
end;
try repeat' (Ltransitivity;[find_Lrewrite_lemma|LrewriteSimpl_old']);
try (once (Ltransitivity;[useFixHypo|]));
once lazymatch goal with
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => eapply ext_rel_helper
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => eapply extT_rel_helper
| |- _ => idtac
end).
Lemma LrewriteTime_helper_index:
forall [s t : term] [i i' : nat], i = i' -> s >(<=i) t -> s >(<=i') t.
Proof. intros. now subst. Qed.
Lemma redLe_app_helperL s s' t u i j:
s >(<= i) s' -> app s' t >(<=j) u -> app s t >(<=i+j) u.
Proof. intros ? H'. eapply redLe_app_helper in H'. 2:eassumption. 2:Lreflexivity. now rewrite Nat.add_0_r in H'. Qed.
Lemma redLe_app_helperR s t t' u i j:
t >(<= i) t' -> app s t' >(<=j) u -> app s t >(<=i+j) u.
Proof. intros ? H'. eapply redLe_app_helper in H'. 3:eassumption. 2:Lreflexivity. eassumption. Qed.
Lemma pow_app_helperL s s' t u:
s >* s' -> app s' t >* u -> app s t >* u.
Proof. now intros -> -> . Qed.
Lemma pow_app_helperR s t t' u:
t >* t' -> app s t' >* u -> app s t >* u.
Proof. now intros -> -> . Qed.
Ltac LrewriteSimpl_appL R:=
lazymatch R with
| star step => refine (pow_app_helperL _ _)
| redLe _ => refine (redLe_app_helperL _ _)
end.
Ltac LrewriteSimpl_appR R:=
lazymatch R with
| star step => refine (pow_app_helperR _ _)
| redLe _ => refine (redLe_app_helperR _ _)
end.
Ltac appTimeHelper tt:=
(once lazymatch goal with
| |- app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _
=> Ltransitivity;[refine (LrewriteTime_helper_index _ (extTApp fInts xInts));[unfold evalTime;reflexivity]| ]
end ).
Ltac isValue s:=
lazymatch s with
| lam _ => idtac
| app _ _ => fail
| @ext _ _ _ _ => idtac
| @extT _ _ _ _ _ => idtac
| @enc _ _ _ => idtac
| I => idtac
| ?P => tryif (is_var P;lazymatch eval unfold P in P with rho _ => idtac end) then idtac
else
lazymatch goal with
| H : proc s |- _ => idtac
| H : lambda s |- _ => idtac
| _ => idtac
end
end.
Ltac LrewriteSimpl'' canReduceFlag :=
idtac;
once lazymatch goal with
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => refine (ext_rel_helper _ _)
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => refine (extT_rel_helper _ _)
| |- ?R ?s _ => has_no_evar s;
repeat' (idtac;
lazymatch goal with
| |- _ (lam _) _ => fail
| |- _ (enc _) _ => fail
| |- L.app (@ext _ (_ ~> _ ) _ _) (ext _) >* _ => Ltransitivity;[apply extApp|]
| |- L.app (@ext _ (_ ~> _ ) _ ?ints) (@enc _ ?reg ?x) >* ?v =>
change (app (@ext _ _ _ ints) (@ext _ _ _ (reg_is_ext reg x)) >* v);
Ltransitivity;[refine (extApp _ _)|]
| |- L.app (@extT _ (_ ~> _ ) _ _ ?fInts) (@extT _ _ _ _ ?xInts) >(<= _ ) _ => appTimeHelper tt
| |- L.app (@extT _ (_ ~> _ ) _ _ ?ints) (@enc _ ?reg ?x) >(<= ?k ) ?v =>
change (L.app (@extT _ _ _ _ ints) (@extT _ _ _ _ (reg_is_extT reg x)) >(<= k) v);appTimeHelper tt
| |- _ (@ext _ (@TyB _ ?reg) _ _) _ => refine (ext_rel_helper _ _)
| |- _ (@extT _ (@TyB _ ?reg) _ _ _) _ => refine (extT_rel_helper _ _)
| |- ?R (L.app _ _) _ =>
let progressFlag := fresh in
let recCanReduceFlag := fresh in
let tmp := fresh in
assert (progressFlag:=tt);
assert (tmp:=tt);
assert (recCanReduceFlag:=tt);
try (LrewriteSimpl_appR R;[solve [LrewriteSimpl'' tmp;Lreflexivity]|try clear progressFlag]);
try clear tmp;
try (LrewriteSimpl_appL R;[solve [LrewriteSimpl'' canReduceFlag;Lreflexivity]|try clear progressFlag]);
lazymatch goal with
| |- ?R (L.app ?s ?t) _ =>
let maybeBeta _ := lazymatch s with lam _ => Lbeta end in
try (maybeBeta ();try clear progressFlag);
tryif (tryif is_var recCanReduceFlag then isValue t else fail)
then
try (
Ltransitivity;[solve [find_Lrewrite_lemma|useFixHypo]|];
try clear progressFlag ;
try (clear canReduceFlag;pose (canReduceFlag:=tt))
)
else clear canReduceFlag
end;
tryif is_var progressFlag then fail else idtac
| |- ?H => Ltransitivity;[solve[find_Lrewrite_lemma]|]
end)
end.
Ltac LrewriteSimpl' := let flag := fresh in assert (flag:=tt);
(tryif Lbeta then try LrewriteSimpl'' flag else LrewriteSimpl'' flag);try clear flag.
Ltac LrewriteSimpl := Lrewrite_wrapper ltac:(idtac;LrewriteSimpl').