Stream: math-comp users

Topic: Using canonical instances in mathcomp2


view this post on Zulip Sebastian Ertel (Feb 21 2024 at 11:17):

Hi,

I'm trying to port a project to mathcomp 2/HB following the recommended porting guide.

According to the guide, canonical structures are represented in mathcomp 2 via hierarchy builder instances, i.e., they are created via HB.instance.
But instances are never named. In fact, the guide states that they should not be named to let the hierarchy builder do the job of finding the canonical instance:

Note that the instance need not be named and better not be since it is the job of HB to figure out instances automatically.

But the guide never says how I can actually use a canonical instance of a structure for a certain type.

For example, assume I would like to define a cast from unit to choiceType:

Definition cast (t:unit) : choiceType := t.

Here, I would like to use the canonical instance for unit. I thought maybe the coercions that HB generates would do this job for me but that does not seem to be the case.

What am I missing?

view this post on Zulip Cyril Cohen (Feb 21 2024 at 11:28):

Hi @Sebastian Ertel supposing you could name the canonical choice type for unit (e.g. unit_choiceType : choiceType, what would your cast function look like now?

view this post on Zulip Cyril Cohen (Feb 21 2024 at 11:31):

Anyway, with HB and Coq >= 8.16 (and preferably >= 8.18 because of printing features), you can now write unit : choiceType to mean the choiceType structure on unit, formerly called unit_choiceType or [choiceType of unit].

view this post on Zulip Cyril Cohen (Feb 21 2024 at 11:31):

E.g. you may define Definition unit_choiceType : choiceType := unit.

view this post on Zulip Sebastian Ertel (Feb 21 2024 at 12:11):

Hi @Cyril Cohen ,

thanks for your response.

Definition unit_choiceType : choice := unit. gives me the following error:

The term "unit" has type "Type" while it is expected to have type "choiceType".

Also Definition unit_choiceType : choiceType := [choiceType of unit]. gives me the following error:

The term "id_phant" has type "phantom Type unit → phantom Type unit" while it is expected to have type "unify Type Type unit ?cT nomsg".

I'm on Coq 8.18 and mathcomp 2.1.0.

view this post on Zulip Pierre Roux (Feb 21 2024 at 12:15):

You probably need to From mathcomp Require Import choice.?

view this post on Zulip Sebastian Ertel (Feb 21 2024 at 13:10):

No, I do have that already.

view this post on Zulip Sebastian Ertel (Feb 21 2024 at 13:11):

(Otherwise using choiceType itself would already fail resolution.)

view this post on Zulip Pierre Roux (Feb 21 2024 at 14:09):

Then we would need a minimal example to understand because here, the following works:

From mathcomp Require Import ssreflect ssrfun ssrbool choice.
Check unit : choiceType.

view this post on Zulip Sebastian Ertel (Feb 22 2024 at 08:22):

Hi @Pierre Roux ,
Indeed what you wrote there is the minimal example. It fails for me with

The term "unit" has type "Type" while it is expected to have type "choiceType".

Let me prepare a nix flake that I can share.

view this post on Zulip Pierre Roux (Feb 22 2024 at 08:49):

Yes, that indeed sounds like some bad version of something.


Last updated: Jul 25 2024 at 15:02 UTC