Stream: Coq users

Topic: Implementing hierarchies of theories in modern coq


view this post on Zulip 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?

view this post on Zulip Reynald Affeldt (Oct 09 2020 at 10:14):

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

view this post on Zulip 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

view this post on Zulip Shea Levy (Oct 09 2020 at 10:17):

Awesome! These look great

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 11:24):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 11:26):

And tradeoffs are complex.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Oct 09 2020 at 12:47):

canonical structures


Last updated: Jan 29 2023 at 03:28 UTC