Stream: Coq users

Topic: Implementing hierarchies of theories in modern coq

Shea Levy (Oct 09 2020 at 10:10):

Is the Packaging Mathematical Structures paper still a good starting point for implementing a hierarchy of theories in a composable way? Are there modern features in the intervening 11 years that can make it nicer?

Reynald Affeldt (Oct 09 2020 at 10:14):

I think that this paper is now nicely complemented by https://arxiv.org/abs/2002.00620.

Reynald Affeldt (Oct 09 2020 at 10:16):

and the future might be https://github.com/math-comp/hierarchy-builder but it depends on what your purpose is

Shea Levy (Oct 09 2020 at 10:17):

Awesome! These look great

Reynald Affeldt (Oct 09 2020 at 10:19):

(there is also https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/ but that might be more specialized)

Christian Doczkal (Oct 09 2020 at 10:30):

@Shea Levy I recently gave hierarchy-builder a try and it can already do more than I would want to do manually. There may be some minor issues here and there (like documentation being scarce and not always up to date), but it's definitely worth trying.

Enrico Tassi (Oct 09 2020 at 10:38):

There is a zulip channel for hierarchy builder, if you have any troubles.
Also, the master branch is in heavy development, so not very stable, but supports structures with parameters.

Paolo Giarrusso (Oct 09 2020 at 11:24):

@Shea Levy the other approach is https://arxiv.org/abs/1102.1323

Paolo Giarrusso (Oct 09 2020 at 11:26):

And tradeoffs are complex.

Paolo Giarrusso (Oct 09 2020 at 11:27):

But if you want to live in the math-comp ecosystem, CSes are probably what you want.

Shea Levy (Oct 09 2020 at 11:59):

@Paolo Giarrusso Ah, I don't really have any dependency on math-comp, just trying to learn best practices. Just described my use case a bit more here

Shea Levy (Oct 09 2020 at 12:46):

Paolo Giarrusso said:

But if you want to live in the math-comp ecosystem, CSes are probably what you want.

What does "CS" refer to here by the way?

Karl Palmskog (Oct 09 2020 at 12:47):

canonical structures

Last updated: Oct 03 2023 at 21:01 UTC