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

Question

基本上，我想观察一些例子(比如3 x^2+2 x +1和2x +1)的伪多项式除法的结果。多项式间的伪除法是在SsResive1.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来测试您的问题了。正如我们在注释中所讨论的那样，您应该依赖loaded的整数来获得加载的正确的规范结构实例。下面是我的代码，使用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的内部选择禁止计算。您应该在should的邮件列表中直接询问更多这方面的信息。

希望这能帮上忙。