Stream: Hierarchy Builder devs & users

Topic: adapting to HB.dev


view this post on Zulip Christian Doczkal (Apr 15 2021 at 14:44):

I'm trying to adapt my development from HB-0.10 (which compiled fine with HB.1.0.0 but nut 1.1.0) to the current state. On one of my structures, I get the following error:

Error: You must declare the current class indt «axioms_» before
indt «Pttdom.axioms_»

This happens in the HB.structure command for Ptt. Both structures have one mixin, and the mixins for the two structures are similar (they overlap in 10 of the 12 resp 13 axioms). Has there been a change in how overlapping structures are handled?

view this post on Zulip Cyril Cohen (Apr 15 2021 at 14:45):

Can you provide a link?

view this post on Zulip Enrico Tassi (Apr 15 2021 at 14:45):

This error message is perfectible https://github.com/math-comp/hierarchy-builder/issues/225 , maybe you need to declare a join structure

view this post on Zulip Christian Doczkal (Apr 15 2021 at 14:50):

Cyril Cohen said:

Can you provide a link?

https://github.com/coq-community/graph-theory/blob/master/theories/ptt.v#L18-L34
https://github.com/coq-community/graph-theory/blob/master/theories/pttdom.v#L45-L61

view this post on Zulip Christian Doczkal (Apr 15 2021 at 14:52):

So, neither structure includes the other, but they do contain a bunch of shared axioms. Do I need to declare the shared axioms as a separate stucture?

view this post on Zulip Christian Doczkal (Apr 15 2021 at 14:54):

Apparently I fooled the older versions of HB by using different names for the same axioms. Indeed, as the comments suggest, I probably should turn one of them into a Factory, as the Pttdom laws are all derivable in Ptt. So the current setup is a bit of a hack anyway.

view this post on Zulip Enrico Tassi (Apr 15 2021 at 14:57):

The design pattern is to have the largest possible mixin, then have a smaller factory which deduces all the fields which are redundant

view this post on Zulip Enrico Tassi (Apr 15 2021 at 14:57):

Anyway, the error message is still broken

view this post on Zulip Christian Doczkal (Apr 15 2021 at 14:58):

Enrico Tassi said:

Anyway, the error message is still broken

That we can agree on :grinning_face_with_smiling_eyes:

view this post on Zulip Cyril Cohen (Apr 15 2021 at 14:58):

Christian Doczkal said:

So, neither structure includes the other, but they do contain a bunch of shared axioms. Do I need to declare the shared axioms as a separate stucture?

Yes you should put common fields in a a common mixin

view this post on Zulip Christian Doczkal (Apr 15 2021 at 15:00):

Is it also possible to keep the large Pttdom Mixin, then declare Ptt as a substructure (inheriting vom Pttdom) and provide a factory that does not require the derivable fields?

view this post on Zulip Cyril Cohen (Apr 15 2021 at 15:06):

Christian Doczkal said:

Is it also possible to keep the large Pttdom Mixin, then declare Ptt as a substructure (inheriting vom Pttdom) and provide a factory that does not require the derivable fields?

Then you need to turn the current Ptt_of_Ops into a factory, make a mixin Ptt_of_Pttdom which is the bare minimum to add to Pttdom to turn it into a Ptt.

view this post on Zulip Christian Doczkal (Apr 15 2021 at 15:07):

Yes, that's what I'm trying right now :grinning:

view this post on Zulip Christian Doczkal (Apr 15 2021 at 16:29):

Okay, the factory works nicely, with the slight annoyance that one has to redeclare the Proper instances both within the builders section and on the new structure.

view this post on Zulip Christian Doczkal (Apr 15 2021 at 16:39):

Next question: how do chained instances work? I have that term is a pttdom, and I have that every pttdom is also an elabelType. So I have this instance:

pttdom_Pttdom__canonical__structures_Elabel: pttdom -> elabelType

and Check [the pttdom of term] works but Check [the elabelType of term] fails. What's the missing piece?

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:03):

then it must not be an instance but inheritance

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:05):

Can you be more specific or point me to an example?

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:05):

we will soon forbid things such as
https://github.com/coq-community/graph-theory/blob/master/theories/pttdom.v#L208-L209
with error message:

this instance declaration breaks forgetfull inheritance (see doc), use #[nonforgetful] if that's really what you wish to do, but we recommend that you put it inside a module that could be imported on demand.

unless you put an attribute #[nonforgetful]

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:06):

But this does not exist. The rationale is that instances from a structure to another in the same hierarchy must not exist.

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:06):

(you would have to redeclare it several times, and functorial constructions would lead to non-definitionally equal terms which look the same)

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:07):

you should make pttdom a subclass of elabelType

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:07):

it isn't because it does not even have the operation, the operation is derived.

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:09):

The elabelType has two equivalences, which in the paricular case of a type with converse can be defined as x = y°.

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:18):

I'd be okay with making term/pttdom canonically elabelTypes, even if I have to redeclare this again for every instance. But I don't know how to do this without relying on internal names.

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:20):

If you can derive a structure from another, then it must be a substructure

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:20):

I do not understand yet you usecase I think

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:21):

can you point me to the code of elabelType ?

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:21):

And what is the internal name you are relying on?

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:22):

https://github.com/coq-community/graph-theory/blob/master/theories/structures.v#L84-L95

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:24):

Cyril Cohen said:

And what is the internal name you are relying on?

So far none, but I thought I could put the canonical structure for term as pttom into the construction of elabelTypes from pttdom. But that looks messy.

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:27):

you can always refer to canonical instances through [the st of ty]

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:28):

what would prevent you from making pttdom inherit from elabelType?

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:32):

  1. I would need an extra axiom stating that the second equivalence of elabelType is indeed defined as xy°x \equiv y°
  2. This adds clutter to the definition of pttdom, making it different from the algebra on would have on paper.

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:34):

I am looking for the analog of "In particular, every (X:pttdom) can be seen as elabelType by defining xy:=xyx \equiv' y := x \equiv y^\circ."

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:37):

Christian Doczkal said:

  1. I would need an extra axiom stating that the second equivalence of elabelType is indeed defined as xy°x \equiv y°
  2. This adds clutter to the definition of pttdom, making it different from the algebra on would have on paper.
  1. yes, and for most concrete instance it would hold definitionally
  2. does not stand if you make a factory

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:37):

Christian Doczkal said:

I am looking for the analog of "In particular, every (X:pttdom) can be seen as elabelType by defining xy:=xyx \equiv' y := x \equiv y^\circ."

That's dangerous because if someone already put another elabelType on your type X this will not hold...

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:37):

This is explained in https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:38):

(or at least we tried)

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:38):

And if you really want to do it that way, I strongly advise it is contained in a module, and you will need to repeat the instance for every single concrete type as well as the abstract types that inherit pttdom.

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:40):

Cyril Cohen said:

And if you really want to do it that way, I strongly advise it is contained in a module, and you will need to repeat the instance for every single concrete type as well as the abstract types that inherit pttdom.

Currently, I have exactly one concrete instance (the term algebra), so please tell me how. (I take note of your warnings and choose to ignore them for now). :shrug:

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:42):

HB.instance Definition _ := Elabel.copy term [the pttdom of term]

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:48):

Thank you! Now everything compiles with the dev versions again. So let's see how backwards compatible these solutions are...

view this post on Zulip Cyril Cohen (Apr 15 2021 at 17:51):

Cyril Cohen said:

HB.instance Definition _ := Elabel.copy term [the pttdom of term]

That won't work for HB < 1.1.0

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:54):

Yes, I realized that instead of < 1.1.0 I now have to require >= 1.1.0, which seem preferable to me :grinning:

view this post on Zulip Christian Doczkal (Apr 15 2021 at 17:55):

At least it does compile with a released version and dev. That's all I ask.


Last updated: Jan 29 2023 at 16:02 UTC