在 coq/ssreflect 中显示多项式相等

Question

我试图通过 coq 中的显式计算来证明多项式的相等性。这是一个显示我陷入困境的示例：

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Local Open Scope ring_scope.

Variable F : fieldType.
Variable w : F.

Definition test1 (k : nat) := w%:P*w%:P*'X^k + w%:P.

Definition test2 (k : nat) := w%:P*'X^k + 1%:P.

Lemma foo: w%:P* (test2 2) = (test1 2).
Proof.
unfold test2. unfold test1.

第一步实际上必须涉及“执行乘法”，但我不太明白该怎么做。我想接下来要显示两个多项式相等需要显示它们逐项相等，但我找不到封装它的现有引理。

我也很想知道如何定义多项式 X^k + 1；写作

Definition test3 (k : nat) := 'X^k + 1%:P.

没用。

更一般地说，如果有人可以指出使用 ssreflect 进行代数的合理文档、教程等，我将不胜感激。 （不幸的是，我不确定这样的事情是否存在。）

Answer 1

这是您小问题的解决方案。

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Local Open Scope ring_scope.

Variable F : fieldType.
Variable w : F.

Definition test1 (k : nat) := w%:P*w%:P*'X^k + w%:P.

Definition test2 (k : nat) := w%:P*'X^k + 1%:P.

Lemma foo: w%:P* (test2 2) = (test1 2).
Proof.
rewrite /test1/test2.
by rewrite mulrDr mulr1 mulrA.
Qed.

这个问题的解决仅依赖于环定理：乘法相对于加法的分配性、1是乘法的中性元素以及乘法的结合性。

经验丰富的用户会知道此处使用

mulrDr

的原因如下：

• 我们想要处理的图案具有以下形状

  _ * (_ + _)

• 乘法将在定理名称中注明

  mul

  ，
• 我们知道我们只使用乘法和加法的ring属性 这带来了

  r

的第一次出现
• 该模式的第二个重要部分是加法，这带来了定理名称中的

  D

• 加法位于乘法的右侧，这带来了定理名称中的最后一个

  r

  。

同样，库中也存在一个

mulrDl

定理，从名字上就很容易猜出其表述。

同样的推理使得我知道使用

mulr1

（任意环元素r乘1——这里1后面没有添加后缀，1乘r会写成mul1r）。

这里用到的知识就多了一点。你用

1%:P

来表示值为1的常数多项式，其中我们所说的1实际上是环

F

中乘法的中性元素。您可以使用 1，这意味着环

{poly F}

中的中性元素。原来两者是可以转换的，这样

mulr1

其实是可以用的。

对于

mulrA

：环中的乘法，结合性。

定理的名称遵循文件标题注释中解释的哲学

https://github.com/coq/coq/blob/master/theories/ssr/ssrbool.v

https://math-comp.github.io/htmldoc_2_2_0/mathcomp.algebra.ssralg.html

（可以根据最新的数学成分分布将

htmldoc_2_2_0

替换为）。

阅读您在数学组件中依赖的所有文件的所有标题注释可能会很有用。你也应该看看这本书

https://math-comp.github.io/mcb/

当然，这是很多文档，可能会让人感到不知所措，但库的大小使得我们无法更详细地记录所有内容。最后，人们可能需要完整阅读一些文件才能了解其中存储的宝藏。例如，

bigop

文件包含迭代运算符的完整处理，值得大量关注。如果不知道这些定理的存在，就很难发现如何使用它们。