Stream: Hierarchy Builder devs & users

Topic: packing structures


view this post on Zulip Aleksandar Nanevski (Sep 11 2024 at 14:29):

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?

view this post on Zulip Pierre Roux (Sep 11 2024 at 14:43):

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).

view this post on Zulip Aleksandar Nanevski (Sep 11 2024 at 15:14):

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

view this post on Zulip Pierre Roux (Sep 16 2024 at 13:15):

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).

view this post on Zulip Pierre Roux (Sep 16 2024 at 13:15):

Maybe HB.saturate would work too, I haven't tested

view this post on Zulip Aleksandar Nanevski (Sep 16 2024 at 17:15):

Thanks, this worked!

view this post on Zulip Pierre Roux (Sep 16 2024 at 18:57):

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