Stream: Equations devs & users

Topic: Computing with well founded recursion


view this post on Zulip 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?

view this post on Zulip Kenji Maillard (Jun 10 2020 at 10:03):

wouldn't simp eta_expand in H work ?

view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Jun 10 2020 at 10:04):

(Also Equations can provide subterm relations automatically.)

view this post on Zulip 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))

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 10:06):

lazy also seems to reduce to full normal form, so it expands eta_expand a into something unreadable as well

view this post on Zulip 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)

view this post on Zulip Théo Winterhalter (Jun 10 2020 at 10:07):

Ah I see, sorry. :/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 16:59):

I would suggest adding a lemma eta_expand tBox = tBox to the eta_expand rewrite database

view this post on Zulip Matthieu Sozeau (Jun 10 2020 at 17:00):

Simplifying wf definitions applied to open terms using conversion is bound to be painful...

view this post on Zulip Jakob Botsch Nielsen (Jun 10 2020 at 17:31):

That seems like a reasonable solution, I'll try it out


Last updated: Jan 29 2023 at 16:02 UTC