coq - 如何在 Coq/Ssreflect 中进行伪多项式除法

Question

基本上，我想在某些情况下观察伪多项式除法的结果（比如 3 x^2+2 x +1 和 2 x +1）。多项式之间的伪除法在 Ssreflect 1.4 的 polydiv.v 中的 edivp 中实现。我希望代码应该如下所示：

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import ssralg poly ssrnum zmodp polydiv interval.

Open Scope Z_scope.

Definition p := Poly [::1;2;3].

Definition q := Poly [:1;2:].

Eval compute in edivp p q.

但是，由于类型统一失败，代码停留在定义 p 上。任何帮助是极大的赞赏。

Answer 1

我终于有时间安装 ssreflect 来测试您的问题。正如我们在评论中讨论的那样，您应该依靠 ssreflect 的整数来加载正确的规范结构实例。这是我的代码，使用 ssr1.4 和 coq8.4pl5：

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import ssralg poly ssrnum zmodp polydiv ssrint.

Open Scope int_scope.

Definition p := Poly [:: 1%:Z;2%:Z;3%:Z].

Definition q := Poly [:: 1%:Z;2%:Z].

现在Eval compute输入正确，但它的计算似乎没有终止。我认为这是由于 ssr 的内部选择禁止计算。您应该直接在 ssreflect 的邮件列表中询问更多相关信息。

希望这会有所帮助，V。