Stream: Hierarchy Builder devs & users

Topic: Porting dioid

Pierre Roux (Mar 02 2021 at 11:55):

I recently ported dioid to Hierarchy Builder. This was great but I still have a few questions:

• I had to redeclare notations at the end of my file because they were overloaded by HB (for instance + was printed as Builders_1.Super.add)
• is there a way to build on top of existing hierarchies (something like HB.register if that makes any sense), I ended up doing a few wrappers over choiceType, porderType and latticeType (c.f. https://github.com/math-comp/dioid/blob/master/HB_wrappers.v) which works but is not ideal since I need to add Canonical instances by hand for each non HB structures I rely on
• building substructures for subType (and some closed properties for the operators of the structure) requires some amount of painful boiler plate, could HB be of any help here?
• I got a few warnings (below), could it be an indication that I made something wrong?

```
Warning: Ignoring canonical projection to WrapPOrder.class by
WrapPOrder.class in join_ComDioid_between_ComSemiRing_and_WrapPOrder:
redundant with join_Dioid_between_SemiRing_and_WrapPOrder

Warning: Projection value has no head constant:

Warning: Ignoring canonical projection to SemiRing.Class by SemiRing.class in
eenat_is_a_SemiRing: redundant with enat_is_a_SemiRing

Cyril Cohen (Mar 02 2021 at 12:57):

Hi @Pierre Roux, some notation problems will be solved by the next release, just wait a little bit. There is no way to use HB on top of existing hierarchies because we had to slightly alter the packed class design pattern to make it more regular. Making a robust HB.register would probably take more time than porting the hierarchy. You might be interested in the following mail I recently sent to the mathcomp-dev mailing list. We already have a partial port of mathcomp in this branch which I believe is sufficient to try dioids on top. It is based on the soon to be released next version of HB. Subtypes are already addressed in this branch (they used not to follow the packed-class discipline, in the HB version, they do)

Cyril Cohen (Mar 02 2021 at 12:58):

The warnings are due to a missing feature in HB to ignore class as a canonical projection. Every message of the form
Warning: Ignoring canonical projection .*(to|by).* .*.class can be safely ignored. Sorry about that.

Cyril Cohen (Mar 02 2021 at 13:04):

Finally, Canonical is banned for HB handled structures. If you are using it you are not only doing it wrong but potentially breaking things. You must use HB.instance instead.

EDIT: I see you are using Canonical only for compatibility purposes, I guess that's a necessary evil, and as long as it works I guess it is ok-ish... Things will be better soon though.

Cyril Cohen (Mar 02 2021 at 13:12):

BTW @Pierre Roux you are welcome to the porting sprint.

Pierre Roux (Mar 03 2021 at 10:56):

@Cyril Cohen great, you can count me in for the porting sprint (those are the dates of JFLA http://jfla.inria.fr/jfla2021.html but I guess it'll have to be cancelled once again unfortunately)
I'll try building dioid on top of the hierarchy-builder branch

Cyril Cohen (Mar 05 2021 at 22:05):

The discussion on the error on PredSubZmodule was moved here and an issue was opened here: math-comp/hierarchy-builder#182

Pierre Roux (Mar 06 2021 at 11:51):

Thanks to the support of function types for keys ( https://github.com/math-comp/hierarchy-builder/tree/demo-2021-03-05 ), this PredSubThing business now becomes really easy:

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

HB.mixin Record IsSemiRing R := {
  zero : R;
  add : R -> R -> R;
  add0d : left_id zero add;
}.
HB.structure Definition SemiRing := {R of IsSemiRing R}.

Notation "0" := (@zero _).
Infix "+" := (@add _).

HB.mixin Record IsAddClosed (R : SemiRing.type) (S : R -> bool) := {
  add_closed0 : S 0;
  add_closedD : {in S &, forall u v, S (u + v)};
}.
HB.structure Definition AddClosed R := {S of IsAddClosed R S}.

HB.factory Record PredSubSemiRing (V : SemiRing.type) (S : AddClosed.type V) U
           of SUB V S U := {}.

HB.builders Context (V : SemiRing.type) (S : AddClosed.type V) U
            of PredSubSemiRing V S U.

Let inU v Sv : U := Sub v Sv.
Let zeroU := inU add_closed0.
Let addU (u1 u2 : U) := inU (add_closedD _ _ (valP u1) (valP u2)).

Program Definition semiringU := @IsSemiRing.Build U zeroU addU _.
Next Obligation. by move=> x; apply: val_inj; rewrite !SubK add0d. Qed.
HB.instance Definition _ := semiringU.

HB.end.

(* test *)

HB.instance Definition _ := IsSemiRing.Build nat add0n.

Definition evennat (x : nat) : bool := ~~ odd x.

Record enat := { enat_val :> nat; enat_prop : evennat enat_val }.

HB.instance Definition _ := BuildSubTypeFor enat enat_val.

Program Definition enat_add_closed := IsAddClosed.Build _ evennat _ _.
Next Obligation.
by move=> x y /negbTE Hx /negbTE Hy; rewrite /evennat oddD Hx Hy.
Qed.
HB.instance Definition _ := enat_add_closed.

HB.instance Definition _ := PredSubSemiRing.Build _ _ enat.

Enrico Tassi (Mar 06 2021 at 13:33):

HB.instance Definition _ := enat_add_closed. This is what I meant @Cyril Cohen , even if the instance is existing you can still do HB.instance Definition on it (ok, here there is no section business... but that is the the idea)

Cyril Cohen (Mar 06 2021 at 14:38):

Yes cf this

Cyril Cohen (Mar 06 2021 at 14:41):

@Pierre Roux unfortunately predicates cannot be handled like this on the scale of mathcomp run because various interferences with predtypes, we will have to tune hierarchy builder to account for this.

Pierre Roux (Mar 06 2021 at 14:49):

I don't get why you would need a predType here, but I'm certainly missing something.

Pierre Roux (Mar 29 2021 at 10:09):

@Cyril Cohen sorry, I still don't get why this wouldn't be usable in ssralg for instance. It seems to me that the current implementation of substructures in ssralg requires to use a predType whereas the above solution enables it, hence being more generic. Where am I wrong?

Cyril Cohen (Mar 30 2021 at 09:48):

Hi @Pierre Roux the current implementation in ssralg is indeed quite involved and has multiple purposes, the main focus being on usability. In that sense it is "quite hard" to add a new structure and not so natural to add a new lemma, but in exchange, when doing proofs you can use them transparently: it will work in both applicative (P x) and collective form (x \in P) and the output looks uncluttered (you do not see canonical instance names for the predicates you used).
Hence the solution you propose makes the implementation simpler but it will not cover as many usecases as the one currently in ssralg, and in particular it will not interact with \in yet (and there will be the main difficulties I think).

Cyril Cohen (Mar 30 2021 at 12:53):

We intend to extend HB in the future to support mathcomp ssralg discipline

Pierre Roux (Mar 31 2021 at 08:01):

@Cyril Cohen thanks for the more precise answer.. I had a deeper look. Indeed, the above solution works with

HB.instance Definition _ := IsSemiRing.Build nat add0n.

Definition evennat := [qualify x | ~~ odd x].

Record enat := { enat_val :> nat; enat_prop : (mem evennat) enat_val }.

HB.instance Definition _ := BuildSubTypeFor enat enat_val.

Program Definition enat_add_closed :=
  IsAddClosed.Build _ (mem evennat) _ _.
Next Obligation.
by move=> x y /negbTE Hx /negbTE Hy; rewrite /in_mem /= oddD Hx Hy.
Qed.

HB.instance Definition _ := enat_add_closed.

HB.instance Definition _ := PredSubSemiRing.Build _ _ enat.

and if we replace mem evennat by \in in the definition of enat, the inference in the last line fails (the following works though PredSubSemiRing.Build _ (AddClosed.clone _ (mem evennat) _) enat.). One would then want to replace mem evennat in the definition of enat_add_closed by in_mem^~ (mem evennat) (so as to match the definition of enat) but then HB fails on HB.instance Definition _ := enat_add_closed. (with a not so nice error message).

Pierre Roux (Mar 31 2021 at 08:04):

@Enrico Tassi here is a reduced example for the last error message

From HB Require Import structures.

HB.mixin Record IsPred (R : Type) (S : R -> bool) := {}.
HB.structure Definition Pred R := {S of IsPred R S}.

Definition bool_pred := IsPred.Build bool (fun x => true).

HB.instance Definition _ := bool_pred.

last line fails with Error: elpi: term->gref: input has no global reference: fun x (global (indt «bool»)) c0 \ global (indc «true»)
After putting a few spy-do here and there, it appears the error happens in get-local-structures. I don't know if we want a better error message or try to handle this case.

Enrico Tassi (Mar 31 2021 at 09:53):

thanks, I'll look into it.

Enrico Tassi (Mar 31 2021 at 10:18):

https://github.com/math-comp/hierarchy-builder/pull/195

Enrico Tassi (Mar 31 2021 at 10:18):

It is not super clear if I should error, or not, but at least it does not crash

Enrico Tassi (Mar 31 2021 at 10:19):

This example now gives a warning:

Warning: Projection value has no head constant: fun _ : bool => true in
canonical instance Fun4_canonical_Pred of Pred.sort, ignoring it.
[projection-no-head-constant,typechecker]

Cyril Cohen (Mar 31 2021 at 10:34):

For now, I see no way not to error on this... one should make progress on coq/coq#12329 ...

Enrico Tassi (Mar 31 2021 at 11:40):

I think we should put the error very early, but leave the rest of the code roughly as I wrote, so that when coq adds support for this we can just remove the error

Enrico Tassi (Mar 31 2021 at 11:41):

@Pierre Roux maybe you have some energy for finishing @Janno 's PR... it was not in a bad state IIRC

Enrico Tassi (Mar 31 2021 at 11:50):

(assuming you need that, and that it was not just a typo)

Last updated: May 28 2023 at 18:29 UTC