Конечный список с неизвестным размером

Question

Я немного запутался, пытаясь определить некоторые структуры, используя библиотеку math-comp. Я хочу определить структуру, которая имеет функцию, начиная от набора значений и возвращая списки других значений. Я пытаюсь определить эту структуру как finType но это терпит неудачу (я предполагаю, что это потому, что я возвращаю список неизвестного размера).

Например:

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.

Это выдает ошибку Unable to unify,

Я думаю, проблема в том, что я использую seq и это не конечно. Я не уверен, как описать, что он будет возвращать только конечные списки. Я думал, что я мог бы использовать n-кортежей, но это потребовало бы указать размер заранее (я мог бы включить размер вместе с F ценность возможно? Я не уверен, как это будет выглядеть в этой записи).

Что-то мне не хватает или есть другой подход, который кажется более адекватным?

Заранее спасибо!

Answer 1

Я предлагаю вам указать связанную функцию непосредственно на типе. Это, например, используется в PhD Стефании Думбравы, чтобы ограничить максимальную арность подписи и хорошо работает, если вы знаете хитрость:

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

Обычно bound := \max_S ...так что это хорошо работает с остальной частью теории.