What do you think of Hierachy Builder (https://github.com/math-comp/hierarchy-builder). Is this something that you could use in your own projects? Is it something that we could recommend blindly to mathematician newcomers?

I dont know much about it. From what @Robbert Krebbers says, it is basically a generalization of what math-comp/ssreflect are doing?

unfortunately their approach doesn't work for us because we need the hierarchy to interact well with typeclasses, and the unification algorithm that typeclasses use is incompatible with ssreflect heirarchies. that's okay for them as they use their own `apply:`

tactic everywhere which uses the new(er) unification, and they dont use type classes at all. but we are mixing canonical structures and typeclasses (for various reasons, one of them being entirely out of our control: `Proper`

instances so we can `rewrite`

-- ssreflect uses normal `=`

everywhere but we really need setoids), and so we have no choice, things have to work with old unification.

so we had to heavily tweak their approach to make it work "most of the time", and even then about once a month we discover a situation where one of our instances doesnt fire and using `apply:`

instead makes it work. it is quite painful.

so based on that @Théo Zimmermann I would answer your question about recommending it blindly with "no". there are some major caveats.

OK, thanks! Indeed, the incompatibility with setoid rewrite is quite a bummer given how important the latter is (especially to mathematicians who are used to work with quotients).

correspondingly, https://github.com/coq/coq/issues/6294 is easily #1 on the list of coq bugs that we'd *really* like to see fixed.^^ (but yes I know it's a really hard problem.)

@Cyril Cohen @Kazuhiko Sakaguchi you may be interested in the points made by Ralf. Can we do something to make HB more setoid friendly? (apart from reimplementing setoids...)

@Ralf Jung is setoids the only issue you have? I imagine it is because of binders in Iris, am I correct? ("newcomer mathematician" -> "needs setoids" seems a quite strong assumption to me, this is why I'm asking for more details)

BTW: I tried porting the iris hierarchy to the hierarchy builder to see what whould happen but a) it really doesn't do type class resolution (so the field types are basically the `Set Printing All`

output of the original version) and b) after some fields it just started reporting internal errors to me. I might still have the branch somewhere.. I should probably report bugs?

Enrico Tassi said:

Ralf Jung is setoids the only issue you have? I imagine it is because of binders in Iris, am I correct? ("newcomer mathematician" -> "needs setoids" seems a quite strong assumption to me, this is why I'm asking for more details)

we use typeclasses for a lot of things, not just setoids. setoids is just the thing we control least.^^

not sure what you mean by binders here. iris has tons of objects where Coq's `=`

is just not the right notion of equality, we need something more extensional. on top of that we use step-indexing which gives rise to a family `dist: nat -> T -> T -> Prop`

of equivalence relations, and we also need good support for rewriting with `dist n`

.

@Janno Please open an issue about your porting experience, it can be interesting to us developing it. HB does nothing about type classes, nothing at all, so it is not clear to me what you expect.

(maybe we should move these messages in the HB stream)

(Is there such a stream?)

There is!

This topic was moved here from #Coq users > Hierarchy builders and type classes by Théo Zimmermann

Enrico Tassi said:

Cyril Cohen Kazuhiko Sakaguchi you may be interested in the points made by Ralf. Can we do something to make HB more setoid friendly? (apart from reimplementing setoids...)

I am not sure there would be an issue with setoid. HB only handles hierarchies themselves, fields can be anything, in particular a setoid equality that you can base instances of Proper on, I think.

Interaction issues between canonical structures and typeclasses appear mainly when you rely on both of them at the same time to infer one object. If it happens with HB, I am curious to see how exactly...

@Cyril Cohen

I am not sure there would be an issue with setoid. HB only handles hierarchies themselves, fields can be anything, in particular a setoid equality that you can base instances of Proper on, I think.

as mentioned before, the issue with this is that TC search is unable to apply many lemmas whose statement involves canonical structures, including in some cases the projections of the structures themselves.

the only reason ssreflect works at all is that they use `apply:`

instead of `apply`

this is a long-standing problem in Coq's unification algorithm (https://github.com/coq/coq/issues/6294)

What is the status of the hierarchy builder and type classes? Did anyone experiment? Is there a detailed proposal on what to do?

@Janno Did you ever write down your experience?

@Enrico Tassi @Cyril Cohen @Kazuhiko Sakaguchi you write:

We believe it would take a minor coding effort to retarget HB to another bundling approach.

https://hal.inria.fr/hal-02478907v5/document

Is more information available?

We did not try. I still think it would not be too hard, but my priority is to have math-comp be ported to HB. We are getting close, but we are not there yet. For example we managed to compile the odd order theorem on top of MC+HB, but we still have some performance issues to solve before declaring victory.

If you really want TC support in HB, we happily accept contributions ;-)

We could try to have a look at it, but it would be good to have some guidance on the "minor coding effort".

Last updated: Jan 29 2023 at 16:02 UTC