The Coq mailing list

[Wenda Li <wl302 AT cam.ac.uk>]

Dear Coq experts,

I am new to Coq. I want to observe the result of pseudo polynomial 
division (implemented by edivp in polydiv.v) on some instances (say 3 
x^2+2 x +1 and 2 x +1) with the following code:

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

  Open Scope int_scope.

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

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

  Eval compute in edivp x y.

However, the evaluation seems to get stuck in a loop. I can understand 
that given polynomial x and y, there are infinite tuple (k,q,r) such 
that ((lcoeff q) ^ k) * x = q * y + r and deg r < deg y, where lcoeff q 
is the leading coefficient of q and deg r is the degree of r. Does this 
indicate that pseudo division in Coq is implemented in a way that is not 
executable?

Any help is greatly appreciated.

Best regards,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge