@Paolo Giarrusso , I'm moving your question here. So if you look at the code in Declare.declare_mutually_recursive
, you can see that
you can see:
let csts = CList.map2
(fun CInfo.{ name; typ; impargs; using } body ->
let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
cinfo fixdecls
so indeed, an entry is declared for each component of the fixpoint; this makes sense due to the way the terms are built before. Unsure if the kernel is doing some sharing here?
I’m unfamiliar with the internal APIs, but in Gallina abstract syntax, IIUC, fix decls for decl1
and fix decls for decl2
don’t seem to have a shared decls
subnode — or at least, decls
is not a term
worse, a naive kernel, which works well elsewhere but not here, would provide as API “give me a Gallina AST of a closed term (up to top-level defs. etc) to typecheck and add to the environment”, which isn’t good enough here.
the “shared subproblems” are the typechecking of each body decl_i
in decls
, which are open wrt all the other decl_j
, j <> i
for a user, the question is whether qed-checking for proofs by mutual fixpoint incurs an Nx slowdown when done directly, without induction principles.
right now for me this is just a curiosity, but before I’ve had cases where it mattered
that part of the code / design is one of the oldest in Coq, the problem is that you need to check the projection indeed, however that's tricky as you cannot have a global let as definitions are top-level entries; ideas on how to update this part are open, we have done significant work in the last times to actually allow to work on this without breaking clienets
The goal of my question is to make sure whether there's a potential issue to workaround ;-)
And potentially, to mention this in the manual
(but I can't promise I'll file the docs MR myself soon)
Okay, Herbelin's answer confirms that too.
There is a CEP on global fixpoints (and a preliminary branch) which could help to address this by sending the tuple of fixpoints once.
Indeed, also we could extend the current kernel to take a fixpoint and generate the projections efficiently
would likely be cleaner than the current approach
Last updated: Oct 13 2024 at 01:02 UTC