I recently ported dioid to Hierarchy Builder. This was great but I still have a few questions:
```
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
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)
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.
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.
BTW @Pierre Roux you are welcome to the porting sprint.
@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
The discussion on the error on PredSubZmodule
was moved here and an issue was opened here: math-comp/hierarchy-builder#182
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.
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)
Yes cf this
@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.
I don't get why you would need a predType here, but I'm certainly missing something.
@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?
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).
We intend to extend HB in the future to support mathcomp ssralg discipline
@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).
@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.
thanks, I'll look into it.
https://github.com/math-comp/hierarchy-builder/pull/195
It is not super clear if I should error, or not, but at least it does not crash
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]
For now, I see no way not to error on this... one should make progress on coq/coq#12329 ...
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
@Pierre Roux maybe you have some energy for finishing @Janno 's PR... it was not in a bad state IIRC
(assuming you need that, and that it was not just a typo)
Last updated: Sep 25 2023 at 12:01 UTC