Hi.

I've been defining various properties of morphisms on partial commutative monoids (pcm), and I needed to show that function composition preserves these properties. For example, to declare that composition preserves fullness and binormality (it doesn't matter what these are now), this is the way I did that in coq 8.19.2+mathcomp 2.2.0:

HB.instance Definition _ (f : full_binorm_pcm_morph U V)

(g : full_binorm_pcm_morph V W) :=

Full_Binorm_PCM_morphism.copy (g \o f)

(Full_Binorm_PCM_morphism.pack_

(Binorm_PCM_morphism.class (g \o f))

(Norm_PCM_morphism.class (g \o f))

(Full_PCM_morphism.class (g \o f))).

I always thought that the above is way too concrete a solution, it's just that I didn't manage to find a more abstract way to do it.

However, the variants:

HB.instance Definition _ (f : full_binorm_pcm_morph U V)

(g : full_binorm_pcm_morph V W) :=

Full_Binorm_PCM_morphism.copy (g \o f) (g \o f)

and

HB.instance Definition _ (f : full_binorm_pcm_morph U V)

(g : full_binorm_pcm_morph V W) :=

Full_Binorm_PCM_morphism.on (g \o f).

didn't work. For example, the last one retuns the error:

```
Toplevel input, characters 0-151:
> HB.instance Definition _ (f : full_norm_pcm_morph U V)
> (g : full_norm_pcm_morph V W) :=
> Full_Norm_PCM_morphism.on (g \o f).
Error:
Definition illtyped: In environment
U, V, W : pcm
f : full_norm_pcm_morph U V
g : full_norm_pcm_morph V W
The term "Full_Norm_PCM_morphism.phant_on_ (Phantom (U -> W) ?t)" has type
"@Full_Norm_PCM_morphism.axioms_ U W (@Full_Norm_PCM_morphism.sort U W ?t)"
while it is expected to have type
"@Full_Norm_PCM_morphism.axioms_ U W
(@comp (PCM.sort W) (PCM.sort V) (PCM.sort U)
(@Full_Norm_PCM_morphism.sort V W g)
(@Full_Norm_PCM_morphism.sort U V f))".
```

Is there an alternative solution that's more abstract than my first attempt?

Could you please provide a pointer to the code so that we can investigate further. Meanwhile I would try things like `Check (g \o f) : Full_Norm_PCM_morphism.type.`

and simpler structures to find out at which points it breaks. An HB.instance on some simpler structure might also be missing (sometimes Coq can infer and instance but HB doesn't have it in its database and a few more `HB.instance ... simpler_structure.on ...`

are needed).

The code is at git@github.com:imdea-software/fcsl-pcm.git in the master branch. The file is pcm/morphism.v, line 1583.

Sorry for the delayed answer, apparently the following works (tested on Coq 8.20, I can't compile the file on Coq master):

```
HB.instance Definition _ (f : full_norm_pcm_morph U V)
(g : full_norm_pcm_morph V W) :=
PCM_morphism.on (g \o f).
HB.instance Definition _ (f : full_binorm_pcm_morph U V)
(g : full_binorm_pcm_morph V W) :=
PCM_morphism.on (g \o f).
```

Maybe `HB.saturate`

would work too, I haven't tested

Thanks, this worked!

What happens is that most of the instances (full_ and norm_) were already there so the .on just triggers the completion with the join (full_norm_)

Last updated: Oct 13 2024 at 01:02 UTC