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 :
        Finite.axiom
          (T:={|
                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 https://github.com/math-comp/math-comp/blob/1a09520497a1bac2fd2f12778ed1dba119407c91/mathcomp/ssreflect/choice.v#L46 , 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 https://github.com/math-comp/analysis/blob/2a51379c7c7cabe51e2bcf3e0f6b9111fba6e560/classical/boolp.v#L65) to have that B -> A is finite. There is {ffun _ -> _} from https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/finfun.v that might do what you want.


Last updated: Jul 25 2024 at 15:02 UTC