I'm trying to investigate an issue that show up there: https://github.com/TheoWinterhalter/coq-partialfun/blob/4748b804b7e108d3d94bd5da6f8c1fbad4d728b3/theories/PartialFun.v#L491 . Using `funelim`

on a function defined as

```
Equations def_p (x : A) (h : domain x) : image x
by wf x partial_lt :=
def_p x h := orec_inst (a := x) (f x) _ _ _ (λ y hy hr, def_p y _).
```

we get a `Stack overflow.`

error. Replacing `funelim`

by `apply_funelim`

gets rid of the error, but introduces a usage of function extensionality instead, that we'd rather avoid.

Is this a bug? If so, what could be causing it? If not, is there a way, maybe more painful, to try and avoid using funext?

Ping @Théo Winterhalter who originally wrote the code

After investigating, afaict the issue comes from the last argument of `def_p`

, which is higher order… And so requires funext to establish an unfolding equation. Could that be the case?

And you’re invoking def_p recursively in that argument, and it’s defined by WF recursion…

I’ve always needed funext in such scenarios, with program — that was part of program’s tactics for unfolding lemmas

And in general, do unfolding lemmas for WF recursion ever hold definitionally? If not, or if they don’t here, funext seems necessary.

They never hold definitionally, but funext is not necessary in general, an inductive proof can be enough.

There is an option of Equations for that

You just need to prove a theorem showing that the accessibility proof is irrelevant for the functional

Actually Equations tries that strategy as well, but it will fail in higher-order cases, I guess that's what happens here

Also it might be that funelim fails because `def_p`

is transparent? Or the accesibility proof of partial_lt? This might make a tactic go bonkers

I'm not sure I understand the subtleties of what Théo is doing, but indeed, there is probably something like this: the proof of `partial_lt`

is playing with `Acc`

-fueling… Afaict, the tactic that goes crazy is simply `auto`

, so indeed probably uncontrolled unfoldings happen somewhere

And indeed, trying to replay the proof of the equations by hand I end up with a goal which is an equality between functions producing elements in `Acc`

, and after repeated usage of `funext`

I can close said goal trivially by using that `Acc`

is proof-irrelevant. So the issue really seems to boil down to the higher-order character of the function

So I guess the solution will be to inline `orec_inst`

somehow

Thanks for the heads-up!

Rather, show that orec_inst is a morphism for pointwise equality, and use that in the congruence proof instead

Last updated: Oct 13 2024 at 01:02 UTC