问题标签 [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.
linux - 如何在 Linux 中安装 SSReflect 和 MathComp?
我已经在 Linux (Ubuntu 17.04) 中成功安装了 Coq 8.6 和 CoqIDE。但是,我不知道要继续将 SSReflect 和 MathComp 添加到此安装中。我检查过的所有参考资料似乎都让我感到非常困惑。有没有人有一个直接而简单的食谱?我确实安装了 opam。
coq - Coq - 在 Ssreflect 中证明涉及 bigops 的严格不等式
我正在尝试使用数学组件库来证明以下内容:
最初,我试图在orbigsum_aux
的文档中找到一些等效的引理,但我找不到;所以这就是我到目前为止所能做的:ssralg
bigop
欢迎任何有关相关引理的帮助或指示。
coq - Coq - Ssreflect 中的空范围证明
我必须以以下形式证明一个目标:
我目前处于Hm: m = 0
堆栈中的情况,因此这本质上是forall
一个空集。在这种情况下我该如何进行?使用
留给我
但是当然我不能使用rewrite Hm
它,因为它因依赖类型错误而失败。
coq - Coq - 在 Ssreflect 中证明关于序列元素的条件
我有一个看起来像这样的目标:
在上面,f
是产生不等式的解的定义,v, j
并且P v j
是一个谓词,将 j 限制为满足另一个不等式的索引。
我已经证明了这一点Goal : P v j -> (f v j > 0)
,但是我如何使用它来证明它适用x
于序列中的任何一个?我发现了一些相关的引理,比如nthP
引入序列操作,我非常不熟悉。
提前致谢!
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 一起工作?
coq - Coq/SSreflect 中的有序序列
我目前正在使用 Coq 中的红黑树,并希望为列表配备一个订单,以便可以使用该模块nat
将它们存储在红黑树中。MSetRBT
出于这个原因,我定义seq_lt
如下:
到目前为止,我已经成功展示了:
也
但是,我正在努力证明以下内容:
我什至不确定最后一个引理是否可以使用归纳法,但我已经研究了几个小时,不知道从这一点开始。定义有seq_lt
问题吗?
coq - ssreflect、Coq 的自动化,同时处理关于 nat 数的矛盾假设
ssreflect
在以下引理中使用时:
请问为什么autos
我注释掉的那些在那些证明状态下不起作用?在我看来,这些国家已经在上下文中观察到矛盾。
是否有一些自动化ssreflect
来证明这个引理?
equality - 在 Coq 中证明 Martin-Lof 等式与路径归纳之间的同构
我正在研究 Coq 并试图证明 Martin-Lof 的平等和路径归纳的平等之间的同构。
我将这两个等式定义如下。
我将同构中涉及的两个函数定义如下。
现在我正在尝试定义以下证明术语,但我无法从最初的陈述中移开,因为我实际上不知道要应用什么策略。
我通过我可以简化表达式
但我不知道该怎么做。有谁知道我如何继续这个证明?
提前致谢。
coq - 从 mathcomp 的 ssralg 中的 int_Ring 类型中提取整数
为这个问题做一点准备:符号`_i
被定义为序列的第 i 个分量,但也意味着多项式的第 i 个系数。以下代码输出Negz 2 : int_ZmodType
:
的类型my_seq
是seq int
。该类型int
具有构造函数Posz
和Negz
.
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_polynomial
是seq int_Ring
。然而,做Eval compute in (polyseq my_polynomial)`_1.
同样的事情。
在从具体类型转换int
到int_Ring
的过程中,整数的值是否丢失了?int
或者,有没有办法从a 中恢复 a 的值int_Ring
?方式int_Ring
是打包的,看起来不太可能,因为构造函数不引用元素。但是,同样可以这样说int_ZmodType
。作为参考,这些类型定义在
https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v
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
化为该类的成员?