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