2

尝试使用 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值一起包括在内？我不确定在这个符号中会是什么样子）。

是否有我遗漏的东西，或者是否有另一种似乎更合适的方法？

提前致谢！

4

1 回答 1

2

我建议您直接在类型上指定绑定函数。例如，这在 Stefania Dumbrava 的博士中用于限制签名的最大数量，如果你知道诀窍，效果很好：

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

通常bound := \max_S ...，因此它适用于理论的其余部分。

于 2018-10-24T14:22:07.360 回答