Jakob Botsch Nielsen (Jun 10 2020 at 10:00): Jakob Botsch Nielsen (Jun 10 2020 at 10:00):Are there any tricks for simplifying when using well founded recursion? I have a quite standard subterm relation term_subtermwhich I proved well founded in a fully transparent way. I use this to define a function eta_expand with Equations. However, now I have a hypothesis
H: eta_expand a ▷ eta_expand tBox
that I want to simplify to just H: eta_expand a ▷ tBox, but cbn takes a very long time. I see the following behavior:
Eval cbn in eta_expand a. (* computes to eta_expand a immediately *)
Eval cbn in eta_expand tBox. (* computes to tBox after a very long time *)
Eval cbv in eta_expand a. (* computes to massive normal form after a very long time *)
Eval cbv in eta_expand tBox. (* computes to tBox instantly *)
Any hints to make this less painful than having to use change (eta_expand tBox) with tBox?
Kenji Maillard (Jun 10 2020 at 10:03):wouldn't simp eta_expand in H work ?
Théo Winterhalter (Jun 10 2020 at 10:03):What about lazy? It is sometimes much more efficient than the others, especially since it won't reduce proof terms that are irrelevant?
Théo Winterhalter (Jun 10 2020 at 10:04):(Also Equations can provide subterm relations automatically.)
Jakob Botsch Nielsen (Jun 10 2020 at 10:05):The definition of eta_expand is a bit complicated, simp eta_expand in H ends up giving me
eta_expand_unfold_clause_1 a0 (inspect (decompose_app a0))
▷ eta_expand_unfold_clause_1 tBox (inspect (decompose_app tBox))
lazy also seems to reduce to full normal form, so it expands eta_expand a into something unreadable as well
Jakob Botsch Nielsen (Jun 10 2020 at 10:06):(Also Equations can provide subterm relations automatically.)
My subterm relation is a bit more complicated, for example I have this constructor:
| term_sub_Case_2 t p discr brs : In t (map snd brs) -> term_direct_subterm t (tCase p discr brs)
Ah I see, sorry. :/
Jakob Botsch Nielsen (Jun 10 2020 at 10:10):No worries, thanks for the suggestions anyway. I wonder if there just is some global that I should tell cbn to prioritize unfolding, but I'm not sure how to figure out what.
Jakob Botsch Nielsen (Jun 10 2020 at 10:42):The problem seems to be that my well-foundedness proof is very slow to produce an Acc_intro with cbn. I changed it to use Acc_intro_generator 1000 [proof] and then I marked eta_expand to only be unfolded when the first argument is a constructor. Not unfolding eta_expand is crucial since cbn will endlessly try to compute Acc_intro_generator otherwise it seems. This seems to do what I want.
Jakob Botsch Nielsen (Jun 10 2020 at 10:46):Well, I spoke too soon. Now it just hangs forever on eta_expand (tApp a b). Back to the drawing board...
Matthieu Sozeau (Jun 10 2020 at 16:59):I would suggest adding a lemma eta_expand tBox = tBox to the eta_expand rewrite database
Matthieu Sozeau (Jun 10 2020 at 17:00):Simplifying wf definitions applied to open terms using conversion is bound to be painful...
Jakob Botsch Nielsen (Jun 10 2020 at 17:31):That seems like a reasonable solution, I'll try it out
Last updated: Jun 11 2023 at 00:30 UTC