Stream: Equations devs & users

Topic: `funelim` overflow and function extensionality


view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 10:07):

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?

view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 10:08):

Ping @Théo Winterhalter who originally wrote the code

view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 11:28):

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?

view this post on Zulip Paolo Giarrusso (Apr 20 2023 at 12:18):

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

view this post on Zulip Paolo Giarrusso (Apr 20 2023 at 12:22):

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

view this post on Zulip Paolo Giarrusso (Apr 20 2023 at 12:22):

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

view this post on Zulip Matthieu Sozeau (Apr 20 2023 at 12:44):

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

view this post on Zulip Matthieu Sozeau (Apr 20 2023 at 12:44):

There is an option of Equations for that

view this post on Zulip Matthieu Sozeau (Apr 20 2023 at 12:45):

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

view this post on Zulip Matthieu Sozeau (Apr 20 2023 at 12:46):

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

view this post on Zulip Matthieu Sozeau (Apr 20 2023 at 12:47):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 12:57):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 12:59):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 13:00):

So I guess the solution will be to inline orec_inst somehow

view this post on Zulip Meven Lennon-Bertrand (Apr 20 2023 at 13:02):

Thanks for the heads-up!

view this post on Zulip Matthieu Sozeau (Apr 20 2023 at 14:14):

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