The Equations package uses FE (functional extensionality) to prove the unfolding equation needed for the realization of well-founded recursion. It seems that this generous use of the axiom functional_extensionality_dep could be traded for a proof obligation for an extensionality property for the defining functional (like F_ext in Init/Wf.v), and that the obligation can be shown without FE in many cases.
I’m curious about the design philosophy here. Is the idea that FE should be standard axiom in Coq as it simplifies many things and doesn’t cost much? In contrast to K where great effort has been invested in Equations to avoid it? It seems inspiration comes from HoTT where FE holds and K is inconsistent.
Gert
1 Like
Indeed, the F_ext proof could be automatically proved in many cases just by following the structure of the program. The only issue is when we use the recursive function in higher-order combinators (e.g. map), then we have to unfold those as well to show that they are extensional. So funext brings us modularity in that sense. I refrained from pursuing this up to now also because funext is a commonly accepted axiom, and it is only used in the unfolding equation, which is anyway kept opaque, so it does not matter for computation. Another thing is that F_ext is trivial if the relation is in SProp, which could be a common case in the future. Otherwise, I’m happy to leave the F_ext proof as an obligation and give the option to prove it by any means to the user if that’s desired!
This would be my preference (though i haven’t actually used Equations yet, so take my preference with a grain of salt).
2 Likes
Leaving the F_ext proof as a proof obligation is also what I would prefer. With Equations we can now routinely define functions with wf recursion and no-one should get the impression that this requires an extra axiom. Given that Equations separates neatly between structural and well-founded recursion, it seems tempting to define all recursive functions through Equations for clarity.
Alright, I’ll look into that after the ICFP deadline 