Stream: Hierarchy Builder devs & users

Topic: question about product of structures


view this post on Zulip Aleksandar Nanevski (Sep 07 2023 at 13:02):

Hi.

I'm playing with HB and inheritance, and have a question about creating the product of compound structures.

For concreteness, here's code that defines a structure of monoids, and then on top of it builds a compound structure of eq_monoids (monoids with decidable equality).

From HB Require Import structures.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype seq bigop fintype finset.
Export Set Implicit Arguments.
Export Unset Strict Implicit.
Export Unset Printing Implicit Defensive.

HB.mixin Record isMonoid T := {
  add : T -> T -> T;
  zero : T;
  addA : associative add;
  zeroL : left_id zero add}.

#[short(type="monoid")]
HB.structure Definition Monoid := {T of isMonoid T}.

#[short(type="eq_monoid")]
HB.structure Definition EQMonoid := {U of Equality U & Monoid U}.

I next show that nat is a monoid, and that a product of two monoids is a monoid.

(* explicitly naming the structures for clarity *)
HB.instance Definition natMonoid : isMonoid nat :=
  isMonoid.Build nat addnA add0n.

Section ProdMonoid.
Variables (U V : monoid).

Definition prod_add (x y : U * V) := (add x.1 y.1, add x.2 y.2).
Definition prod_zero : U * V := (zero, zero).

Lemma prod_addA : associative prod_add.
Proof. by move=>x y z; rewrite /prod_add !addA. Qed.

Lemma prod_zeroL : left_id prod_zero prod_add.
Proof. by case=>x1 x2; rewrite /prod_add !zeroL. Qed.

HB.instance Definition prodMonoid : isMonoid (U * V)%type :=
  isMonoid.Build (U * V)%type prod_addA prod_zeroL.

End ProdMonoid.

The inference of Monoid structures works, as the following commands return properly.

Eval hnf in (Monoid.clone nat _).
Eval hnf in (Monoid.clone (nat*nat)%type _).

However, the inference of EQMonoid structure is a bit puzzling. Inference for nats works (which is a nice surprise, because I didn't explicitly declare the nat instance for eq_monoid).

Eval hnf in (EQMonoid.clone nat _).

But such nice inference doesn't extend to products, as the following doesn't typecheck.

Eval hnf in (EQMonoid.clone (nat*nat)%type _).

This is fixed if I explicitly declare:

HB.instance Definition prodEqMonoid (U V : eq_monoid) :=
  isMonoid.Build (U * V)%type (@prod_addA U V) (@prod_zeroL U V).

However, I find the need for this declaration a bit counterintuitive because (1) the body of prodEqMonoid is exactly the same as for prodMonoid, and (2) I didn't need to declare the eq_monoid instance for nats.

My question is thus: is some construction possible where I don't have to make the explicit declaration of prodEqMonoid, or is the above the right approach?

Thanks,
Aleks

view this post on Zulip Pierre Roux (Sep 07 2023 at 15:42):

If you observe the output of your first HB.instance, you should see (with VSCoq it can be hidden in I don't know what tab):

natMonoid is defined
Datatypes_nat__canonical__test_Monoid is defined
Datatypes_nat__canonical__test_EQMonoid is defined

It declares you monoid instance on nat as expected and since there is already an equality instance (defined in file ssrnat.v in MathComp, c.f. HB.about nat) and an EqMonoid is just a join of a Monoid and an Equality, an instance of EqMonoid is also declared.

For you second HB.instance however, you only get

prodMonoid is defined
Datatypes_prod__canonical__test_Monoid is defined

Indeed, U and V are not eqType so the already existing instance for product of eqtypes (c.f. HB.about prod.) cannot be applied and you have to do your third HB.instance to trigger it.
This result is expected. There is certainly room for improvement here in Hierarchy-Builder (we have quite a few instances of this pattern already appearing in mathcomp itself) but this is non trivial to do so noone has tackled it yet.

view this post on Zulip Aleksandar Nanevski (Sep 07 2023 at 23:53):

Thanks. It seems you're saying that I did it the right way. That's all I wanted to confirm.


Last updated: Oct 13 2024 at 01:02 UTC