Here is some lore about abstraction and modularity mechanisms in Coq and Lean which I think may be relevant for setting conventions for stdlib2:
-
example of where module functors are not good for defining the algebraic hierarchy: the final theorem of a development quantifies over n and talks about the ring of integers mod n, instantiating a library of lemmas about arbitrary rings with that n. If that library is implemented as a module functor, the top-level theorem of the development would also need to be a module functor. Then every other development would need to be defined using functors when calling that theorem with arguments that in turn depend on universally quantified variables. I hear people find this very inconvenient, and there is also the current limitation that a module functor cannot be instantiated by an Ltac script.
-
https://github.com/leanprover/lean/wiki/Refactoring-structures highlights downsides of "bundled" and "unbundled" patters of using typeclasses as modules:
generally, it is relevant in any domain where we have transformations, an identity transformation, a composition operator, and an inverse. It feels weird to tell users that whenever they have a group in their application, they MUST use the constants mul or add. Otherwise, the automation will not work. The list.append and list.nil example emphasizes this issue. It is a monoid, a left_cancel_semigroup, and a right_cancel_semigroup. We want users to be able to use the algebraic normalizer without forcing them to use add for list.append and zero for list.nil.
The unbundled approach doesn't work with the simplifier as is. The problem is that the lemmas are hard to index. For example: the left hand side of the assoc lemma is (?op (?op ?a ?b) ?c)
where ?op, ?a, ?b and ?c are metavariables (aka matching variables). We don't have a single constant that we can use to filter the locations where this lemma can be applied.
mit-plv/fiat-crypto#233 and the RecordImport feature request rocq-prover/rocq#7808 are my half-baked attempt of working around this dilemma...
For an example of emulating this using current Coq features, see mit-plv/bedrock2#14 (later discussion on that issue comes back to other modularity mechanisms which may be also relevant).
Note that the question of modularity interacts with what kind of unification is expected of tactics. For example, if it is expected that code will contain both @ring_add Zring and Z.add, we will likely want tactics to treat them interchangably, and for performance reasons this will likely need to use some restricted form of unification ("alias unification" using Tarjan's algorithm).
Here is some lore about abstraction and modularity mechanisms in Coq and Lean which I think may be relevant for setting conventions for stdlib2:
example of where module functors are not good for defining the algebraic hierarchy: the final theorem of a development quantifies over
nand talks about the ring of integers modn, instantiating a library of lemmas about arbitrary rings with that n. If that library is implemented as a module functor, the top-level theorem of the development would also need to be a module functor. Then every other development would need to be defined using functors when calling that theorem with arguments that in turn depend on universally quantified variables. I hear people find this very inconvenient, and there is also the current limitation that a module functor cannot be instantiated by an Ltac script.https://github.com/leanprover/lean/wiki/Refactoring-structures highlights downsides of "bundled" and "unbundled" patters of using typeclasses as modules:
mit-plv/fiat-crypto#233 and the RecordImport feature request rocq-prover/rocq#7808 are my half-baked attempt of working around this dilemma...
For an example of emulating this using current Coq features, see mit-plv/bedrock2#14 (later discussion on that issue comes back to other modularity mechanisms which may be also relevant).
Note that the question of modularity interacts with what kind of unification is expected of tactics. For example, if it is expected that code will contain both
@ring_add ZringandZ.add, we will likely want tactics to treat them interchangably, and for performance reasons this will likely need to use some restricted form of unification ("alias unification" using Tarjan's algorithm).