My investigations in universes have shown that in interactive mutual fixpoints, the result of the Qed-time minimization is applied to the first statement of the mutual fixpoint but not to the other statements. Thanks to the cleaning of declaration paths (which is a pleasure to navigate in) it seems to me that this (apparently) long-standing issue could be solved by letting
Declare.Proof.close_proofmanage itself the production of the
n entries of the mutual entry rather than building one and letting
declare_mutdef build the others. Does it make sense? Any objections or recommendations about trying to fix that?
I think @Hugo Herbelin the main problem there is users of
close_proof do not know about multiple entries; actually, isn't the interactive case doing the right thing already?
A first step could be actually to unify more the interactive / non-interactive path
Side question: do you know if the mutual inductive is typechecked only once, instead of N times for the N mutual fixpoints, even tho Coq must produce N separate proof terms?
(sorry to hijack the thread)
(no problem, digressing is natural)
As far as I can tell, the kernel do N distinct checks, one for each component of the mutual fixpoint. answered in Code path in mutual definition
@ejgallego: I don't know the code as well as you do,
close_proof returns a list of entries, so it is easy to know if there is one. What are the users of
close_proof which do not know about multiple entries?
@Hugo Herbelin many clients don't support multiple entries, as of today the multiple entries system is only used by equations and derive, but indeed it needs some tweaks as the api still needs improvement
it needs some tweaks as the api still needs improvement
So the simplest is maybe to wait first for further API improvements on your side.
There was a plan to discuss with @Matthieu Sozeau about how to evolve the API, I don't have many concrete plans as of now, so IMHO this is something we could do at CUDW.
many clients don't support multiple entries, as of today the multiple entries system is only used by equations and derive
Are you saying that the
End_derive, ...) should be known from
close_proof already, so that
close_proof can use this information to produce the appropriate entries? But maybe this is the same as saying that
finalize_proof could be merged?
Indeed, these are two mechanism that are similar yet disjoint; unfortunately it doesn't seem trivial to do, but we'd like to discuss how to do it.
Last updated: Oct 15 2021 at 19:03 UTC