Stream: Hierarchy Builder devs & users

Topic: Using a coerced `eqType` to instantiate a structure


view this post on Zulip Julien Puydt (Oct 17 2022 at 12:29):

I'm sure the following doesn't work, and I'm not sure it's even going in the direction I want:

From HB Require Import structures.

From mathcomp Require Import all_ssreflect.
From mathcomp.analysis Require Import boolp.

HB.mixin Record MyType {L: eqType} (E: Type) := {
  my_l: L;
}.
HB.structure Definition My {L: eqType} := { E of MyType L E}.

Inductive foo_type := foo_singleton.
Canonical foo_eqType := EqType foo_type gen_eqMixin.
Canonical foo_choiceType := ChoiceType foo_type gen_choiceMixin.

Check MyType.Build _ _. (* looks ok *)

HB.instance Definition My_nat := MyType.Build foo_type nat.

(notice that replacing foo_type by foo_eqType in the last line gives another error message I don't get either).

view this post on Zulip Enrico Tassi (Oct 17 2022 at 12:39):

You can't mix the old hand made hierarchy.
If you are based on https://github.com/math-comp/math-comp/pull/733 then you can probably do something along these lines, maybe look at ssralg and the module structure

view this post on Zulip Julien Puydt (Oct 17 2022 at 12:45):

I'm not based on this ; I'm using the last released version.

view this post on Zulip Enrico Tassi (Oct 17 2022 at 13:11):

If it is just an experiment, then copy/paste for that PR the mixin/structure for eqType, and so as for modules (which have a parameter which is another structure)

view this post on Zulip Julien Puydt (Oct 17 2022 at 13:20):

@Enrico Tassi I sometimes get the impression that now isn't a particularly good time to try to dig into mathcomp: it's evolving pretty fast... on the other hand, that's also probably the best moment to make suggestions for the same reason...

view this post on Zulip Julien Puydt (Oct 24 2022 at 19:22):

@Enrico Tassi nope, couldn't make it fly

view this post on Zulip Julien Puydt (Oct 27 2022 at 06:20):

Here is what I tried to do to get HB-enabled eqType:

(* this comes from MC's git because I need HB-enabled eqType *)

Require Import ssrbool.

From HB Require Import structures.

Definition eq_axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).

HB.mixin Record HasDecEq T := { eq_op : rel T; eqP : eq_axiom eq_op }.

and the last line fails because eq_op has type rel T while Type was expected... but rel comes from Coq's ssrbool, so it's again a case of mixed HB/non-HB, isn't it?

view this post on Zulip Enrico Tassi (Oct 27 2022 at 06:34):

maybe eq_axiom does not have the right implicits? look like you are passing eq_op as the first and not second argument

view this post on Zulip Julien Puydt (Oct 27 2022 at 06:41):

Oh dear, writing {T} instead of T in eq_axiom's definition indeed gives a better result... thanks!

view this post on Zulip Julien Puydt (Oct 27 2022 at 06:42):

btw in the following lines:

#[mathcomp(axiom="eq_axiom"), short(type="eqType")]
HB.structure Definition Equality := { T of HasDecEq T }.

what does the first one do?

view this post on Zulip Enrico Tassi (Oct 27 2022 at 08:52):

Here: https://github.com/math-comp/hierarchy-builder/blob/6598dc82ec9f9070bcea39fe5520c64fb7ec93d3/structures.v#L538-L594
(although mathcomp.axiom is not properly documented)

view this post on Zulip Julien Puydt (Oct 27 2022 at 09:07):

Nice

view this post on Zulip Paolo Giarrusso (Oct 27 2022 at 09:55):

Seems you needed {T} because you're not using the Set Implicit Arguments dance.


Last updated: Jan 29 2023 at 16:02 UTC