The Coq mailing list

[Laurent Théry <Laurent.Thery AT inria.fr>]

On 12/20/2014 06:53 PM, Wenda Li wrote:
> 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.

Unfortunately most of the functions in ssreflect are locked and do not
actually compute.
Coqeal
(http://www.maximedenes.fr/content/coqeal-coq-effective-algebra-library)
is an attempt to give an effective way of computing with algebra in
ssreflect. It should give you a way to divide polynomials inside Coq.

--
Laurent

Ps: If you are using SSreflect, you should consider sending email to the
dedicated mailing list: 
ssreflect AT msr-inria.inria.fr