## Stream: Equations devs & users

### Topic: Computing with well founded recursion

#### 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_subterm`which 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))
``````

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

#### 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)
``````

#### Théo Winterhalter (Jun 10 2020 at 10:07):

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: Jan 29 2023 at 16:02 UTC