问题标签 [ssreflect]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
2 回答
1867 浏览

linux - 如何在 Linux 中安装 SSReflect 和 MathComp?

我已经在 Linux (Ubuntu 17.04) 中成功安装了 Coq 8.6 和 CoqIDE。但是,我不知道要继续将 SSReflect 和 MathComp 添加到此安装中。我检查过的所有参考资料似乎都让我感到非常困惑。有没有人有一个直接而简单的食谱?我确实安装了 opam。

0 投票
1 回答
77 浏览

coq - Coq - 在 Ssreflect 中证明涉及 bigops 的严格不等式

我正在尝试使用数学组件库来证明以下内容:

最初,我试图在orbigsum_aux的文档中找到一些等效的引理,但我找不到;所以这就是我到目前为止所能做的:ssralgbigop

欢迎任何有关相关引理的帮助或指示。

0 投票
1 回答
72 浏览

coq - Coq - Ssreflect 中的空范围证明

我必须以以下形式证明一个目标:

我目前处于Hm: m = 0堆栈中的情况,因此这本质上是forall一个空集。在这种情况下我该如何进行?使用

留给我

但是当然我不能使用rewrite Hm它,因为它因依赖类型错误而失败。

0 投票
1 回答
80 浏览

coq - Coq - 在 Ssreflect 中证明关于序列元素的条件

我有一个看起来像这样的目标:

在上面,f是产生不等式的解的定义,v, j并且P v j是一个谓词,将 j 限制为满足另一个不等式的索引。

我已经证明了这一点Goal : P v j -> (f v j > 0),但是我如何使用它来证明它适用x于序列中的任何一个?我发现了一些相关的引理,比如nthP引入序列操作,我非常不熟悉。

提前致谢!

0 投票
1 回答
273 浏览

installation - Nix:安装 ssreflect

我正在使用 Coq(版本 8.5-6),安装有 Nix。我想安装 ssreflect,最好还带有 Nix。我发现的唯一信息是here。但是,这与安装 ssreflect 无关,只是尝试一下。尽管如此,我还是尝试尝试一下,但最终收到了数百条警告(关于各种.v.ml4文件的内容),并且迫不及待地等待该过程结束。一个相当典型的警告如下所示:

文件“./algebra/ssralg.v”,第 856 行,字符 0-39:警告:不推荐使用隐式参数;改用参数

所以问题是:我到底如何安装带有 Nix 的 ssreflect?

编辑:阅读 ejgallego 的评论后,似乎不可能安装带有 Nix 的 ssreflect - 尤其是。如果只想安装 ssreflect 而不安装其他模块(fingroup、代数等)。所以我也有以下问题:

标准的 Opam或ssreflectmake install的安装是否可以与 Nix 安装的 Coq 一起工作?

0 投票
1 回答
165 浏览

coq - Coq/SSreflect 中的有序序列

我目前正在使用 Coq 中的红黑树,并希望为列表配备一个订单,以便可以使用该模块nat将它们存储在红黑树中。MSetRBT

出于这个原因,我定义seq_lt如下:

到目前为止,我已经成功展示了:

但是,我正在努力证明以下内容:

我什至不确定最后一个引理是否可以使用归纳法,但我已经研究了几个小时,不知道从这一点开始。定义有seq_lt问题吗?

0 投票
1 回答
159 浏览

coq - ssreflect、Coq 的自动化,同时处理关于 nat 数的矛盾假设

ssreflect在以下引理中使用时:

请问为什么autos我注释掉的那些在那些证明状态下不起作用?在我看来,这些国家已经在上下文中观察到矛盾。

是否有一些自动化ssreflect来证明这个引理?

0 投票
1 回答
138 浏览

equality - 在 Coq 中证明 Martin-Lof 等式与路径归纳之间的同构

我正在研究 Coq 并试图证明 Martin-Lof 的平等和路径归纳的平等之间的同构。

我将这两个等式定义如下。

我将同构中涉及的两个函数定义如下。

现在我正在尝试定义以下证明术语,但我无法从最初的陈述中移开,因为我实际上不知道要应用什么策略。

我通过我可以简化表达式

但我不知道该怎么做。有谁知道我如何继续这个证明?

提前致谢。

0 投票
2 回答
158 浏览

coq - 从 mathcomp 的 ssralg 中的 int_Ring 类型中提取整数

为这个问题做一点准备:符号`_i被定义为序列的第 i 个分量,但也意味着多项式的第 i 个系数。以下代码输出Negz 2 : int_ZmodType

的类型my_seqseq int。该类型int具有构造函数PoszNegz.

https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/poly.v的标题 告诉我们这Poly s是一个带有来自序列的系数的多项式s。它还说这p`_i是多项式的第 i 个系数p。我希望输出以下代码Negz 2

结果项不是Negz 2,尽管它确实有类型int_Ring。多项式有一个序列构造函数polyseq。确实, 的类型polyseq my_polynomialseq int_Ring。然而,做Eval compute in (polyseq my_polynomial)`_1.同样的事情。

在从具体类型转换intint_Ring的过程中,整数的值是否丢失了?int或者,有没有办法从a 中恢复 a 的值int_Ring?方式int_Ring是打包的,看起来不太可能,因为构造函数不引用元素。但是,同样可以这样说int_ZmodType。作为参考,这些类型定义在

https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v

0 投票
0 回答
132 浏览

coq - 如何实现 GRing.Ring.sort

我正在尝试将 SSReflect 的矩阵库与 Coquelicot ( http://coquelicot.saclay.inria.fr/html/Coquelicot.Complex.html )中的复数一起使用。

但是,我收到错误:

The term "ket0" has type "matrix C (S (S O)) (S O)" while it is expected to have type "matrix (GRing.Ring.sort ?R) ?m ?n"

我假设这GRing.Ring.sort是某种类型类或规范结构,但我如何实例C化为该类的成员?