[Agda] Ringsolver seems ok, but how to get NF?

[Nils Anders Danielsson]

On 2010-08-20 16:54, Christoph HERRMANN wrote:
> I want to use natural numbers expressed as arithmetic expressions
> with unknown variables as type indices.
>
> [...]
>
> What is the problem in adding a function to the RingSolver which
> delivers a normal form, i.e.,not only a polynomial but also with
> a unique ordering of the products?

The function normalise does deliver a normal form:

   normalise : ∀ {n} (p : Polynomial n) → Normal n p

The result of normalise p is a normal form /which is equivalent to p/.

I suspect that the "p" argument to Normal gets in your way, though, and
the proof components which are part of the normal form mean that normal
forms are not unique. You may be better off with an unannotated normal
form. Defining a new type and a function which deannotates the result of
normalise should be very easy. (Another option is to use such a type in
the ring solver, and use a separate correctness proof: this could lead
to a substantial speedup.)

I have made some definitions in Algebra.RingSolver public, by the way.

--
/NAD