Stream: math-comp users

Topic: Defining HB instance inside a proof.

view this post on Zulip Florent Hivert (Nov 22 2023 at 22:37):

I had a proof of the following implication (this is actually an equivalence):

Variables R : unitRingType.
Goal rmorphism (@ratr R) -> (forall i, i.+1%:R \is a @GRing.unit R).

Inside the proof I used to write

apply: (rmorph_unit (RMorphism ratr_morph))

where ratr_morph is the name of the assumption rmorphism (@ratr R)
With MathComp 2, not only rmorphism is not defined anymore -- I can easily replace it by

(additive (@ratr R) /\ multiplicative (@ratr R))

but I can't manage to build the instance (RMorphism ratr_morph). Precisely

HB.instance Definition _ := GRing.isAdditive.Build rat _ _ ratr_add.

tells me that ratr_add is not in the environment, though it is in the assumptions of my current goal.

So my question is: is it possible to build local instances inside a proof using the assumption ?
If not, how would you prove my goal ?

view this post on Zulip Kazuhiko Sakaguchi (Nov 22 2023 at 22:44):

You have to put the instance to the proof context by pose in that case. Some examples can be found in algebraics_fundamentals.v.

view this post on Zulip Florent Hivert (Nov 22 2023 at 23:13):

@Kazuhiko Sakaguchi Thanks to your pointer, I've found a solution. It is largely more complicated than before:

have ratrAM := GRing.isAdditive.Build _ _ _ ratr_add.
have ratrMM := GRing.isMultiplicative.Build _ _ _ ratr_mult.
pose ratr_morph : {rmorphism rat -> R} := HB.pack (@ratr R) ratrAM ratrMM.
apply: (rmorph_unit ratr_morph).

Is there a shortcut ?

view this post on Zulip Pierre Roux (Nov 23 2023 at 07:01):

Not that I know (we used HB.pack exactly like that in mathcomp itself).

view this post on Zulip Cyril Cohen (Nov 23 2023 at 08:25):

The shortcut is work in progress.

view this post on Zulip Florent Hivert (Nov 23 2023 at 08:32):

Ha ! ha ! An even more powerful HB to come ! I can't wait ;-)

view this post on Zulip Florent Hivert (Nov 30 2023 at 09:16):

Trying to mark as resolved...

Last updated: Jul 15 2024 at 21:02 UTC