Stream: Coq devs & plugin devs

Topic: Combining mutual Fixpoints into a single declaration?

Hugo Herbelin (Feb 06 2022 at 15:15):

I see at least two reasons to declare global fixpoints in one shot:

• to type-check only once the body rather than as many times as they are fixpoints
• to be able to refer to recursive calls in the body of a fixpoint by a global name rather than by a variable

How would we do that?

A possibility would be to add a new entry MutualDefinitionEntry of mutual_definition_entry in constant_entry but the structuration is not exactly the one we want. For instance, we would like the label of the entry to move inside since there would be several labels in the case of mutual definitions. So, this might go with some restructuration of constant_entry?

We would like the possibility for them to be delayed too.

Maybe would we like also to have mutual definitions of parameters and constants?

Hugo Herbelin (Feb 06 2022 at 15:15):

Side question: wouldn't it be worth to put OpaqueEntry at the same level as OpaqueEntry DefinitionEntry and ParameterEntry, e.g. by merging constant_entry and global_declaration?

Gaëtan Gilbert (Feb 06 2022 at 15:24):

Maybe would we like also to have mutual definitions of parameters and constants?

what does that mean?

Hugo Herbelin (Feb 06 2022 at 16:27):

I mean something like that, but without losing the body of f:

Fixpoint f n := match n with 0 => 0 | S n => f n + g n end
with g n {struct n} : nat.
Admitted.

Maybe a bit tortuous though. We would need to distinguish cases according to whether g depends strictly or largely on f.

Matthieu Sozeau (Feb 06 2022 at 22:34):

I think you need to change the structure of global environments so that an entry can bind multiple names indeed. If you think ahead how to acommodate inductive-recursive definitions, you probably want something of the shape

type global_env = mutual_declarations list
type mutual_declarations =  (kername * declaration) list
type declaration =
  | InductiveDecl id
  | ConstantDecl cd

This would model something like the mutual blocks of Agda.

Hugo Herbelin (Feb 08 2022 at 10:03):

Matthieu Sozeau said:

I think you need to change the structure of global environments so that an entry can bind multiple names indeed.

OK for a change of the structure of global environments at some time, especially if there is some model already in mind, but I was looking at the current time for a light modification which affects only the Safe_typing API.

Gaëtan Gilbert (Feb 08 2022 at 10:05):

I mean something like that, but without losing the body of f:

but g cannot depend on f so we can just declare it as an axiom first

Hugo Herbelin (Feb 08 2022 at 14:52):

Gaëtan Gilbert said:

I mean something like that, but without losing the body of f:

but g cannot depend on f so we can just declare it as an axiom first

Yes, let's forget about it. (Maybe with recursive-recursive types where f occurs in the type of g, but let's forget also.)

Hugo Herbelin (Feb 08 2022 at 21:01):

I was typically thinking at an extension of Safe_typing like:

val add_fixpoint : fixpoint_entry -> safe_environment -> safe_environment
val add_cofixpoint : cofixpoint_entry -> safe_environment -> safe_environment

with

type fixpoint_entry = {
  fixpoint_entry_prefix : rel_context;
  fixpoint_entry_secctx : Id.Set.t;
  fixpoint_entry_names : Id.t array;
  fixpoint_entry_bodies : constr array;
  fixpoint_entry_types : types array;
  fixpoint_entry_types : universe_entry;
  fixpoint_entry_opaque : bool;

or to add a FixpointEntry to add_constant.

Then, the effect on the environment would have been the same (except for constants referring to themselves). Ready to consider alternatives which would eventually help induction-recursion though.

Last updated: Apr 16 2024 at 20:02 UTC