2

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

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
Open Scope ring_scope.
Definition my_seq := [:: Posz 4; Negz 2].
Eval compute in my_seq`_1.

的类型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：

Definition my_polynomial := Poly my_seq.
Eval compute in my_polynomial`_1.

结果项不是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

4

2 回答 2

3

这并没有完全回答这个问题，但我设法证明系数确实是Negz 2。我在此提供证据以作记录。请注意，我对 ssreflect 一点也不熟悉，因此可能有更好、更自然的方法来做到这一点。

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
Open Scope ring_scope.
Definition my_seq := [:: Posz 4; Negz 2].
Eval compute in my_seq`_1.

Definition my_polynomial := Poly my_seq.

Example test : my_polynomial `_1 = Negz 2.
Proof.
  cbn.
  rewrite 2!polyseq_cons. cbn.
  rewrite 2!size_polyC. cbn.
  rewrite polyseqC. cbn. reflexivity.
Qed.

编辑：正如下面的评论中所解释的，这个事实存在更简单的证据。

于 2017-08-11T08:42:57.040 回答
2

这是您的代码的一个有效版本：

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_algebra.
Open Scope ring_scope.
Definition my_seq := [:: Posz 4; Negz 2].
Definition my_poly := @Polynomial _ my_seq erefl.
Compute my_poly`_1.

Poly这个版本没有使用库中定义的更简单的包装函数，而是直接调用polynomial. 如果您查看此类型的定义，您会发现多项式只是包含多项式系数序列的记录，以及断言该序列的最后一个元素（前导系数）的布尔等式证明不为零。（上面表达式中的第二个参数是 的证明，true = trueCoq 将其理解为与 的证明相同的东西(last 1 polyseq != 0) = true，根据计算规则。）您可以手动检查没有什么阻止我们计算的表达式减少，所以 Coq 能够找出答案。

要了解您最初的尝试有什么问题，我们必须稍微展开它。我在这里按顺序包含了相关定义，扩展了一些符号：

Poly s := foldr cons_poly (polyC 0)

polyC c := insubd poly_nil [:: c]

(* from eqtype.v *)
insubd {T : Type} {P : pred T} {sT : subType T P} u0 (x : T) : sT := 
  odflt u0 (insub x)

insub {T : Type} {P : pred T} {sT : subType T P} (x : T) : option sT 
  := if @idP (P x) is ReflectT Px then @Some sT (Sub x Px) else None

在这里我们找到了罪魁祸首：Poly是根据 定义的insub，而后者又是由对 的案例分析定义的idP，这是一个不透明的引理！当一个不透明的术语妨碍时，Coq 的缩减就会卡住。（如果您好奇，这里发生的事情insub是测试，使用idP，多项式的前导系数是否确实不同于零，如果是，则使用该事实来构建多项式。）

问题是 ssreflect 中的许多定义并未完全在逻辑内部进行计算。这是由于两个原因。一是性能：通过让一切都完全减少，我们可以让类型检查变得更慢。另一个是ssreflect是为了推理方便而量身定制的，所以很多定义并不是最有效的。CoqEAL库的开发是为了将具有更好计算行为的定义与更容易推理的定义联系起来，例如在 ssreflect 中；不幸的是，我不知道该项目是否仍在维护。

于 2017-08-10T14:33:28.930 回答