Stream: Hierarchy Builder devs & users

Topic: "criss-cross" inheritance


view this post on Zulip Christian Doczkal (Jul 20 2020 at 08:23):

It seems there is a problem with using HB for the following "criss-cross" inheritance pattern:

O   O
|\ /|
| X |
|/ \|
O   O

That is, if I try the following:

From HB Require Import structures.

HB.mixin Record Setoid_of_Type A :=
  { eqv : A -> A -> Prop }.
HB.structure Definition Setoid := { A of Setoid_of_Type A }.
Infix "≡" := eqv (at level 79).

HB.mixin Record Ops_of_Type A (* of Setoid_of_Type A *) :=
  { par: A -> A -> A }.
HB.structure Definition Ops := { A of Ops_of_Type A}.
Notation "x ∥ y" := (par x y) (left associativity, at level 40, format "x ∥ y").

HB.mixin Record Pttdom_of_Ops A of Ops_of_Type A & Setoid_of_Type A :=
  { parA: forall x y z: A, x  (y  z)  (x  y)  z }.
HB.structure Definition Pttdom := { A of Pttdom_of_Ops A & }.

HB.mixin Record Ptt_of_Ops A of Ops_of_Type A & Setoid_of_Type A :=
  { parC: forall x y: A, x  y  y  x }.
HB.structure Definition Ptt := { A of Ptt_of_Ops A & }.

I get the following (somewhat uninformative) error message:

The command has indeed failed with message:
You must declare
class (indt «axioms») (global (indt «type»))
 (w-params.nil `A` (sort (typ «bug.9333»)) c0 \
   [triple (indt «Ops_of_Type.axioms_») [] c0,
    triple (indt «Setoid_of_Type.axioms_») [] c0,
    triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»

Is this pattern inherently problematic, or is this just a current limitation of the tool?

view this post on Zulip Christian Doczkal (Jul 20 2020 at 08:25):

If I, somewhat arbitrarily, make Ops depend on Setoid, then the problem disappears.

view this post on Zulip Enrico Tassi (Jul 20 2020 at 09:21):

I've opened an issue about the error message: https://github.com/math-comp/hierarchy-builder/issues/91 but I don't recall why the invariant is needed, we will need to wait for @Cyril Cohen or @Kazuhiko Sakaguchi in order to get an answer

view this post on Zulip Kazuhiko Sakaguchi (Jul 20 2020 at 11:29):

@Christian Doczkal In your hierarchy diagram, the join of Setoid and Ops is ambiguous. The join of Setoid and Ops (without any extra axiom) has to be defined first, and Pttdom and Ptt should inherit from it. See Sect. 4 (in particular Fig. 3 and 4) of https://arxiv.org/abs/2002.00620. CC: @Enrico Tassi

view this post on Zulip Enrico Tassi (Jul 20 2020 at 12:08):

After all, it's a matter of replacing a x with a o in the picture ;-)

view this post on Zulip Christian Doczkal (Jul 20 2020 at 12:20):

Yes, except that (a) then two of the links become transitive/redundant, and (b) in my case making one of the two upper structures inherit the other is more natural. Thanks Anyway.

view this post on Zulip Cyril Cohen (Jul 20 2020 at 14:37):

My plan was to fix that by making anonymous structures and remapping cs (for which we need overloading of canonical instances asap!) when possible ambiguous joins are created.


Last updated: Jan 29 2023 at 15:02 UTC