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`

?

wouldn't `simp eta_expand in H`

work ?

What about `lazy`

? It is sometimes much more efficient than the others, especially since it won't reduce proof terms that are irrelevant?

(Also Equations can provide subterm relations automatically.)

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

(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. :/

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.

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.

Well, I spoke too soon. Now it just hangs forever on `eta_expand (tApp a b)`

. Back to the drawing board...

I would suggest adding a lemma `eta_expand tBox = tBox`

to the eta_expand rewrite database

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

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

Last updated: Oct 13 2024 at 01:02 UTC