Stream: math-comp users

Topic: Canonical instance for finType of seq_sub


view this post on Zulip Sebastian Ertel (Feb 23 2024 at 14:06):

Hi,

What would be the proper way to refer to this canonical in MC2?

Canonical seq_sub_finType := Eval hnf in FinType sT (seq_sub_finMixin s).

Trying

Definition seq_sub_finType {T:eqType} (s:seq T): finType := seq_sub s.

gives

The term "seq_sub (T:=T) s" has type "Type" while it is expected to have type "finType".

even though HB.about reports:

HB: seq_sub is canonically equipped with structures:
    - SubChoice
      choice.Choice
      (from "./fintype.v", line 1618)
    - SubType
      (from "./fintype.v", line 1561)
    - SubFinite
      fintype.Finite
      (from "./fintype.v", line 1620)
    - Countable
      SubCountable
      (from "./fintype.v", line 1619)
    - eqtype.Equality
      SubEquality
      (from "./fintype.v", line 1562)

, i.e., claims to be a finType instance.

view this post on Zulip Quentin VERMANDE (Feb 24 2024 at 13:58):

It does not work because the finType structure comes from the subType structure, so you need T to be itself a finType for the inference to work. Since you can have only one canonical instance for a given structure and subject, you will not be able to declare your own on seq_sub. What you can do is declare an alias for seq_sub and declare the instances you want on your alias.
It took some convincing to make it work, but the following compiles:

Definition adhoc_seq_sub := seq_sub.
HB.instance Definition _ (T : eqType) (s : seq T) := Equality.copy (adhoc_seq_sub T s) (seq_sub s).
HB.instance Definition _ (T : eqType) (s : seq T) := isCountable.Build (adhoc_seq_sub T s) (@seq_sub_pickleK T s).
HB.instance Definition _ (T : eqType) (s : seq T) := isFinite.Build (adhoc_seq_sub T s) (@seq_sub_axiom T s).

view this post on Zulip Notification Bot (Feb 26 2024 at 12:12):

Cyril Cohen has marked this topic as unresolved.

view this post on Zulip Cyril Cohen (Feb 26 2024 at 12:17):

Actually seq_sub T type is a finType if T is a choiceType, not a finType
https://github.com/math-comp/math-comp/blob/27b595cee274ade2fdc4a3a8e80213e3bb07a8bf/mathcomp/ssreflect/fintype.v#L1613-L1627

view this post on Zulip Cyril Cohen (Feb 26 2024 at 12:19):

if you can use a choiceType instead of an eqType in your development I would advise you to rely on choiceType instead. Otherwise adhoc_seq_sub choice will be incompatible with the canonical choice function of the base type.


Last updated: Jul 15 2024 at 21:02 UTC