Конечный список с неизвестным размером - PullRequest
Новая
       18

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

0 голосов
/ 24 октября 2018

Я немного запутался, пытаясь определить некоторые структуры с помощью библиотеки 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? Я не уверен, как это будет выглядеть в этой записи).

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

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

1 Ответ

0 голосов
/ 24 октября 2018

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

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

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

...