adapting to HB.dev · Hierarchy Builder devs & users

Stream: Hierarchy Builder devs & users

Topic: adapting to HB.dev

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?

Cyril Cohen (Apr 15 2021 at 14:45):

Can you provide a link?

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

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

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?

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.

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

Enrico Tassi (Apr 15 2021 at 14:57):

Anyway, the error message is still broken

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:

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

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?

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.

Christian Doczkal (Apr 15 2021 at 15:07):

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

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.

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?

Cyril Cohen (Apr 15 2021 at 17:03):

then it must not be an instance but inheritance

Christian Doczkal (Apr 15 2021 at 17:05):

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

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]

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.

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)

Cyril Cohen (Apr 15 2021 at 17:07):

you should make pttdom a subclass of elabelType

Christian Doczkal (Apr 15 2021 at 17:07):

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

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°.

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.

Cyril Cohen (Apr 15 2021 at 17:20):

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

Cyril Cohen (Apr 15 2021 at 17:20):

I do not understand yet you usecase I think

Cyril Cohen (Apr 15 2021 at 17:21):

can you point me to the code of elabelType ?

Cyril Cohen (Apr 15 2021 at 17:21):

And what is the internal name you are relying on?

Christian Doczkal (Apr 15 2021 at 17:22):

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

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.

Cyril Cohen (Apr 15 2021 at 17:27):

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

Cyril Cohen (Apr 15 2021 at 17:28):

what would prevent you from making pttdom inherit from elabelType?

Christian Doczkal (Apr 15 2021 at 17:32):

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

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 $x \equiv' y := x \equiv y^\circ$ ."

Cyril Cohen (Apr 15 2021 at 17:37):

Christian Doczkal said:

I would need an extra axiom stating that the second equivalence of elabelType is indeed defined as $x \equiv y°$

This adds clutter to the definition of pttdom, making it different from the algebra on would have on paper.

yes, and for most concrete instance it would hold definitionally
does not stand if you make a factory

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 $x \equiv' y := x \equiv y^\circ$ ."

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

Cyril Cohen (Apr 15 2021 at 17:37):

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

Cyril Cohen (Apr 15 2021 at 17:38):

(or at least we tried)

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.

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:

Cyril Cohen (Apr 15 2021 at 17:42):

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

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...

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

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:

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: May 28 2023 at 18:29 UTC