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?

Can you provide a link?

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

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

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?

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.

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

Anyway, the error message is still broken

Enrico Tassi said:

Anyway, the error message is still broken

That we can agree on :grinning_face_with_smiling_eyes:

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

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?

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`

.

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

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.

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?

then it must not be an instance but inheritance

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

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]`

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

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

you should make `pttdom`

a subclass of `elabelType`

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

The `elabelType`

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

.

I'd be okay with making `term`

/`pttdom`

canonically `elabelType`

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

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

I do not understand yet you usecase I think

can you point me to the code of elabelType ?

And what is the internal name you are relying on?

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

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.

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

what would prevent you from making `pttdom`

inherit from `elabelType`

?

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

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

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

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

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

(or at least we tried)

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`

.

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:

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

Thank you! Now everything compiles with the `dev`

versions again. So let's see how backwards compatible these solutions are...

Cyril Cohen said:

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

That won't work for HB < 1.1.0

Yes, I realized that instead of `< 1.1.0`

I now have to require `>= 1.1.0`

, which seem preferable to me :grinning:

At least it does compile with a released version and `dev`

. That's all I ask.

Last updated: Dec 07 2023 at 09:01 UTC