问题标签 [ssreflect]

I'm trying to deal with canonical structures in ssreflect. There are 2 pieces of code that I took from here.

I will bring pieces for the bool and the option types.

Now, suppose I have a function f from finType to Prop.

In the last two cases I get the following error:

The term "bool/option T" has type "Set/Type" while it is expected to have type "finType".

What am I doing wrong?

Coq 8.7 集成了流行的 Ssreflect 库。因此可以通过以下方式导入其库：

但是，当我尝试导入ssrnat它时，它会抱怨它是Unable to locate library ssrnat with prefix Coqssrnat，而且我也无法在磁盘上的 Coq 发行版中找到 ssrnat。出于ssrnat某种原因故意不包含，或者文件夹到另一个模块中，或者我的安装有问题？

我想在定义的 Reals 上使用 ssreflect 的引理Coq.Reals.Raxioms。我怎么做？

例如，我希望能够直接在类型变量上使用定义的add、mul等操作，并直接在 Coq 实数上应用。ssralg.GRing.RingRdefintions.RNum.real_closed_axiom

是否有必要证明从 eqType、choice、zmodule 等到 ClosedReals 的所有结构？如果是这样，之前一定有人这样做过，但我一直无法找到它。我可以使用其他一些开发吗？

如果不是这样，那么通过公理来做到这一点的正确方法是什么？是否必须添加额外的强制和Canonical结构语句。

我有两个finTypes，它们之间有一个双射。目前，我需要它们具有相同的基数这一事实。但是，我找不到这个引理，也找不到可以轻松证明该陈述的其他引理。在我看来，证明应该不难。

声明是：

任何帮助表示赞赏！

我试图证明欧拉标准的一种非常有限的形式：

我已经完成了大部分证明，但我只剩下odd (#|F|.-1) = 0，也就是说，#|F|.-1是偶数。（我对特征 2 不感兴趣）。我似乎无法在数学计算库中找到关于finFieldTypes 的基数的有用事实。例如，我希望有一个引理说存在一个p这样的prime p和#|F| = p。我在这里错过了什么吗？

顺便说一句，我也可能完全错过了数学计算库本身中已经存在的欧拉准则证明。

鉴于以下假设：

以及定义为的记录：

直觉上，这个例子似乎也必须是 of finType。

查看其他代码库，我看到人们finType使用表单的构造仅使用一个非证明项导出记录

但在这种情况下，记录有多个字段。

是否有一种自动方法可以为记录派生 fintype，如果没有，如何为记录派生 fintype？

我一直在尝试学习如何使用 ssreflect 进行子类型化，http ://ssr.msr-inria.inria.fr/~jenkins/current/mathcomp.ssreflect.eqtype.html作为我的主要参考，但一直遇到问题. 我想要做的是从T具有三个术语的类型，创建一个T'具有两个术语的子类型a,b。{x:T | P x}(1)和有什么区别subType P？(2) 从我下面的代码中，我必须Sub a Pa是 的一个术语T'，是否有可能有一个适用于两者的通用证明a, b？我在这里感到困惑，因为eqType.v它感觉好像insub是用来从一种类型投影到其子类型的那种。

尝试使用 math-comp 库定义一些结构时，我有点困惑。我想定义一个结构，它的功能范围从一组值到返回其他值的列表。我试图将此结构定义为，finType但它失败了（我认为这是因为我正在返回一个未知大小的列表）。

例如：

这会引发错误Unable to unify。

我认为问题在于我正在使用seq，这不是有限的。我不确定如何描述它只会返回有限列表。我想我可能会使用 n 元组，但这需要事先指定一个大小（我可能可以将大小和F值一起包括在内？我不确定在这个符号中会是什么样子）。

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

提前致谢！

我正在学习 Ssreflect，我想知道如何解决这种情况。我的想法是定义一个图（作为一个记录），然后生成另一个图。下面，我展示了一段不言自明的代码（我从一个较大的代码中提取的）：

请注意，我目前使用finType T，然后，顶点集在某种程度上是 T 的子集。但是，我觉得我可以通过将顶点集视为 finType 本身来利用，并避免“edges_have_vertices”的证明“， 如下：

但是，我得到一个关于 V_Gp（新图的顶点集）应该有一个类型 finType 而不是 {set _} 的错误。有没有办法在 finType 中“转换” V_Gp？

我有一个由有限类型上的序列和该序列的 uniq 证明组成的结构。这应该描述一个显然是有限的类型，但我不知道如何证明这一点。

我以为我可以使用 UniqFinMixin，但是它需要 - 如果我理解正确的话 - 提供该类型的所有元素的显式序列，我不知道如何计算。我尝试在有限类型上使用 Finite.enum，但它只生成一个包含有限类型的所有元素的序列，而且我没有找到一种计算所有子序列/排列的优雅方法。

对我来说似乎很奇怪，这里没有一种简单的方法来派生 finType，但我在 finset.v 文件中找不到它。预先感谢您的帮助。