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 am looking for the analog of "In particular, every (X:pttdom) can be seen as elabelType
by defining ."
Christian Doczkal said:
- I would need an extra axiom stating that the second equivalence of elabelType is indeed defined as
- This adds clutter to the definition of pttdom, making it different from the algebra on would have on paper.
Christian Doczkal said:
I am looking for the analog of "In particular, every (X:pttdom) can be seen as
elabelType
by defining ."
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