Stream: math-comp users

Topic: Instance seem to be ignored.

view this post on Zulip Florent Hivert (Nov 26 2023 at 20:47):

I'm stuck with some canonical instance which doesn't have the expected effect. Here is an extract of the code

Check padic_int p_pr : comUnitRingType.
HB.instance Definition _ :=
  GRing.ComUnitRing_isIntegral.Build (padic_int p_pr) padic_mul_eq0.

Check padic_int p_pr : idomainType.

The last command gives:

he term "padic_int p_pr" has type "Type" while it is expected to have type
 "idomainType".

Unfortunately, I don't know how to reduce the problem.

To reproduce it : make a clone of
https://github.com/hivert/FormalPowerSeries/tree/mathcomp-2
and then make. The error is line 184 of the file padic.v

There is a seemingly similar problem in fps.v

HB.instance Definition _ :=
  isInvLim.Build _ _ _ _ fps_invsys {fps R} fpsprojP fpsindP fpsindE.

Check {fps R} : invLimType fps_invsys.

The term "{fps R}" has type "Type" while it is expected to have type
 "invLimType fps_invsys".

I've no idea what to do. Thanks in advance for any help.

view this post on Zulip Florent Hivert (Nov 26 2023 at 20:49):

Sorry. Wrong stream... But I don't have the right to move it to another stream...

view this post on Zulip Pierre Roux (Nov 27 2023 at 07:42):

What is the output of the HB.instance command? Is it building what you expect?

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:45):

No it's not. The call to

HB.instance Definition _ :=
  GRing.ComUnitRing_isIntegral.Build (padic_int p_pr) padic_mul_eq0.

only answers

HB_unnamed_factory_6 is defined

where it usually define a lot more stuff... I've no idea why nor how to search why ?

view this post on Zulip Pierre Roux (Nov 27 2023 at 07:50):

What does Check GRing.ComUnitRing_isIntegral.Build (padic_int p_pr) padic_mul_eq0. give?

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:51):

GRing.MathCompCompatIntegralDomain.IntegralDomain.Mixin padic_mul_eq0
     : GRing.MathCompCompatIntegralDomain.IntegralDomain.mixin_of
         (padic_int p_pr) (HB_unnamed_mixin_152 (padic_invsys p_pr))
         (HB_unnamed_factory_144 (padic_invsys p_pr))
         (HB_unnamed_factory_142 (padic_invsys p_pr))
         (HB_unnamed_mixin_161 (padic_invsys p_pr))
         (HB_unnamed_mixin_170 (padic_invsys p_pr))
         (HB_unnamed_mixin_153 (padic_invsys p_pr))
         (HB_unnamed_mixin_178 (padic_invsys p_pr))

view this post on Zulip Pierre Roux (Nov 27 2023 at 07:54):

Maybe one of the mixins doesn't match the one in the comUnitRing, I should reproduce to investigate, will try to do it today.

view this post on Zulip Florent Hivert (Nov 27 2023 at 07:58):

Thanks ! Not that this is a side statement which is not preventing me to go further. So if you need more time...

view this post on Zulip Pierre Roux (Nov 28 2023 at 09:29):

So here is the patch:

diff --git a/theories/padic.v b/theories/padic.v
index a2d3df6..c334a0c 100644
--- a/theories/padic.v
+++ b/theories/padic.v
@@ -177,12 +177,13 @@ move: xmod;  rewrite -/(dvdn _ _) pfactor_dvdn // -leqNgt => logx.
 by apply contraLR; rewrite -!leqNgt; exact: leq_add.
 Qed.

-(* Check padic_int p_pr : comUnitRingType. *)
+Check padic_int p_pr : comUnitRingType.

+HB.instance Definition _ := GRing.ComUnitRing.on (padic_int p_pr).
 HB.instance Definition _ :=
   GRing.ComUnitRing_isIntegral.Build (padic_int p_pr) padic_mul_eq0.

-(* TODO : Check padic_int p_pr : idomainType. *)
+Check padic_int p_pr : idomainType.

 End PadicTheory.

--

The explanation is that Coq is able to find the instance of comUnitRingType on padic_int p_pr by unfolding padic_int but that instance is not registered in the database of HB. Registering it with GRing.ComUnitRing.on makes things work.

view this post on Zulip Pierre Roux (Nov 28 2023 at 09:30):

This is a known limitation of HB. I thought there was an issue already opened but couldn't find it. @Cyril Cohen do you remember?

view this post on Zulip Cyril Cohen (Nov 28 2023 at 16:19):

I believe this is not an issue and that it should be documented as the intended behavior.

view this post on Zulip Cyril Cohen (Nov 28 2023 at 16:36):

@Pierre Roux do you disagree?

view this post on Zulip Pierre Roux (Nov 28 2023 at 19:23):

I don't know, having instances automatically built without explicitly asking for them could indeed be surprising. But I agree that this should be documented. Ideally, we could have an error message telling something like "Try HB.instance Definition _ := missingStruct.on key before the current command"

view this post on Zulip Florent Hivert (Nov 28 2023 at 23:34):

@Pierre Roux Thanks for the fix ! This was quite unexpected to me. Indeed having an error message could be of great help. Is there a way of knowing all the instance registered on (padic_int p_pr) ? With this I could maybe have figured out what was wrong.

view this post on Zulip Pierre Roux (Nov 29 2023 at 08:08):

I usually do Print Canonical Projections padic_int but HB.about padic_int or something like that is probably nicer.

view this post on Zulip Cyril Cohen (Nov 29 2023 at 09:36):

Pierre Roux said:

I don't know, having instances automatically built without explicitly asking for them could indeed be surprising. But I agree that this should be documented. Ideally, we could have an error message telling something like "Try HB.instance Definition _ := missingStruct.on key before the current command"

I agree! Furthermore, it is totally something HB can detect. We could actually have an attribute (e.g.#[upto] ?) that HB can suggest, so that the user does not have a long command to type.

Last updated: Oct 13 2024 at 01:02 UTC