## Stream: math-comp users

### Topic: Defining HB instance inside a proof.

#### 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 ?

#### 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`.

#### 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 ?

#### Pierre Roux (Nov 23 2023 at 07:01):

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

#### Cyril Cohen (Nov 23 2023 at 08:25):

The shortcut is work in progress.

#### Florent Hivert (Nov 23 2023 at 08:32):

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

#### Florent Hivert (Nov 30 2023 at 09:16):

Trying to mark as resolved...

Last updated: Jul 15 2024 at 21:02 UTC