Coq Call 2023 09 19

• September 19th 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• CEP #72 and PR #17888 on discharging on the fly (Hugo)

Notes

Participants: Cyril, Emilio, Enrico, Gaëtan, Guillaume, Hugo, Matthieu, Pierre-Marie.

Short summary:

• Pierre-Marie is interested in having access in "real time" to the fully discharged form of a declaration to improve the efficiency of vm_compute
• Enrico, Cyril and Emilio mentioned Georges' proposal of representing declarations of a section as instances of their most generalized form; this proposal was implemented in Lean3 but Lean4 backtracked (see documentation on sections in Lean4; Lean4 design notes, paragraph "parameters"; an explanation of why "parameters" were finally not implemented)
• Further discussions on how to get the convertibility of an inductive/opaque-constant in section with the instantiation of its generalization (ad hoc mechanism, kernel aliases, definition of the specific one from the generalized one, ...)
• Hugo reports about the difficulties to get compatibility if all generalizations of hints, canonical projections, instances, coercions are declared at the same time (but he does not exclude that a fine study of how to put priority on them can help)
• Decision taken to first submit the internal kernel part
• Decision taken of collecting examples of needs so that we know better what to later propose at the user level (with inputs from Cyril in particular), e.g. whether the discharged versions are made available on demand or systematically, and similarly for the various objects
• Emilio noted that declaring multiple versions of the same definition / inductive can also pose some extra work to adapt it to UIs / exploration features, document outline, Search, etc...