Finite list with unknown size

Question

I'm a bit confused trying to define some structures using the math-comp library. I want to define a structure that has a function ranging from a set of values and returning lists of other values. I'm trying to define this structure as finType but it is failing (I assume it is because I am returning a list of unknown size).

For example:

Section MySection.

    Variables F V : finType.

    Structure m := M {
        f : {ffun F -> seq V};
        ...
    }.

(* Using the PcanXXXMixin family of lemmas *)

    Lemma can_m_of_prod : cancel prod_of_m m_of_prod.
      Proof. by case. Qed.

    ...

    Definition m_finMixin := CanFinMixin can_m_of_prod.

This throws the error Unable to unify.

I think the issue is that I am using seq and this is not finite. I am not sure how to describe that it will only return finite lists. I thought I might use n-tuples but this would require specifying a size beforehand (I could include the size along with the F value perhaps? I'm not sure how that would look in this notation).

Is there something I am missing or is there another approach that seems more adequate?

Thanks in advance!

Answer 1

I suggest you specify the bound function directly on the type. This is for example used in Stefania Dumbrava's PhD to bound the maximum arity of a signature and works well if you know the trick:

f : {ffun n -> (bound ...).-tuple A}

Usually bound := \max_S ..., so it works well with the rest of the theory.