Stream: math-comp users

Topic: 'Declaring' a type to be finite

view this post on Zulip Julin Shaji (Mar 01 2024 at 04:57):

I have a type foo:

Inductive foo: Type :=
| Foo0 | Foo1 | Foo2.

How can I 'declare' it to be a finType?

I guess I need to use isFinite.Build for this.

But how can it be done?

HB.about finType.
HB: isFinite.Build is a factory constructor (from "./fintype.v", line 161)

HB: isFinite.Build requires its subject to be already equipped with:
    - hasDecEq

HB: isFinite.Build provides the following mixins:
    - isFinite

HB: arguments: isFinite.Build T [enum_subdef] enumP_subdef
    - T : Type
    - enum_subdef : seq T
    - enumP_subdef :
                Equality.sort := T;
                Equality.class :=
                  {| Equality.eqtype_hasDecEq_mixin := Finite.class T |}
              |}) enum_subdef

I suppose this means, I need to produce a enum_subdef and enumP_subdef.

I think I get how enum_subdef should be like: [Foo0; Foo1; Foo2]

But how should enumP_subdef be? Does it mean, I first need to make
foo an eqtype?

view this post on Zulip Pierre Roux (Mar 01 2024 at 07:27):

Yes. Alternatively, you can also "copy" the finType structure of another type if you have an injective function to it, see can_type and pcan_type in , the code will be something like Finite.copy foo (pcan_type foo_natK) where foo_natK will be some proof of cancelation of some ffunctions foo -> nat and nat -> foo (for instance).

view this post on Zulip Julin Shaji (Mar 26 2024 at 04:23):

Given a type A: finType, does it make sense to say that f: (B: Type) -> A is finite?

view this post on Zulip Julin Shaji (Mar 26 2024 at 04:23):

As in, being able to state that f is also a finType.

view this post on Zulip Quentin VERMANDE (Mar 26 2024 at 09:19):

You would need for B to be finite and the functional_extentionality axiom (see to have that B -> A is finite. There is {ffun _ -> _} from that might do what you want.

Last updated: Jul 25 2024 at 15:02 UTC