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 ?

You have to put the instance to the proof context by `pose`

in that case. Some examples can be found in `algebraics_fundamentals.v`

.

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

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

The shortcut is work in progress.

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

Trying to mark as resolved...

Last updated: Jul 15 2024 at 21:02 UTC