I've been investigating the hierarchy builder after watching your talk and I am really impressed by what it can do. I have some questions:

How tied is it to the coq stdlib? As I understand, it requires coq-elpi (but I am not sure if that is tied to the stdlib). I see that in structures.v there are a lot of registrations going on, but those can probably easily be adapted. I am interested in using HB in the HoTT library, since we follow a similar packed-classes approach in our algebra library.

Hi Ali, thanks for reaching out. HB is not so much tied to Coq stdlib indeed. I do not think it uses any part of coq-elpi that is either... I am very interested in applications to HoTT at some point, the only really problem for the moment is that to this day coq-elpi does not support universe polymorphism (cc @Enrico Tassi ), which I believe is used extensively in HoTT, am I right?

@Ali Caglayan Yes, this would be interesting, also in relation to the work we are doing on universal algebra in HoTT, inspired by math-classes, with @Andreas Lynge and @Philipp G. Haselwarter

@Cyril Cohen

which I believe is used extensively in HoTT, am I right?

Yes, this is correct.

I want to highlight that the HoTT library has a mixed range of styles when it comes to bundling. In @Cyril Cohen's talk he mentions packed classes, examples of which can be found in https://github.com/HoTT/HoTT/tree/master/theories/Algebra

These are built on top of a port of the mathclasses library, which is completely unbundled / uses typeclasses. For many things this is good, but we have noticed performance hits, especially when the typeclass search is not carefully constructed. Cyril mentioned in his talk that this is the kind of problem HB can solve.

We also have a "WildCat" library: https://github.com/HoTT/HoTT/tree/master/theories/WildCat

Which gives a completely unbundled approach to category theory (basically defining a load of mixins). I would be interested to see if HB can help out here, as we often struggle when refactoring core definitions due to their consequences.

We also want to be able to do something like the following (written in HoTT library but is still readable):

```
Require Import Basics Types Algebra.Groups Algebra.AbGroups.
Local Open Scope mc_add_scope.
Local Open Scope mc_mult_scope.
(** G is a group that happens to be commutative. *)
Axiom G : Group.
Axiom commutative_G : Commutative ((.*.) : G -> G -> G).
Global Existing Instance commutative_G.
(** Obviously, coq has no way of knowing that this is an abgroup *)
Fail Check (G : AbGroup).
(** Say we have a lemma about abelian groups *)
Definition ab_is_great (A : AbGroup) (x y : A) : Type
:= x + y = y + x.
(** Coq can't apply this lemma to G because it's not an abelian group. *)
Fail Lemma G_is_great (x y : G) : ab_is_great _ x y.
(** But if we mark the constructor Builld_AbGroup' as a "Canonical Structure" then we can give hints as on how to use G like an abelian group to coq. The commutativity part will be found by typeclasses. *)
Canonical Structure Build_AbGroup'.
(** Now the lemma works! *)
Lemma G_is_great (x y : G) : ab_is_great _ x y.
(** But coq still cannot cast G to an abelian group. *)
Fail Check (G : AbGroup).
```

I constructed this example to highlight how "canonical structures" might be used. But they don't seem to be able to "elaborate with constructors". i.e. coerce a Group to an AbGroup using a constructor for AbGroup.

With HB, you could write `[the AbGroup of G]`

to refer explicitly to the "coerced" type. This is linked to a "missing feature" in Coq that I like to call "reverse coercion", already mentioned here and there

Last updated: Oct 13 2024 at 01:02 UTC