I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over arbitrary (semi)rings. It does this by reducing the generated polynomials to a Horner normal form and comparing equality over that.

That got me wondering whether a similar approach is possible for inequalities over general "ordered semirings" (where the order fits with the semiring operations). Someone pointed me to the omega tactic in Coq, for proving arbitrary statements (including inequalities) about Presburger arithmetic (with some restricted simulated multiplication). Anyway, it's clearly possible for Presburger arithmetic because all statements are decidable, but I don't really care about all statements, and was wondering whether it was possible for a particular algebraic structure without relying on properties of particular structures like the integers or reals.

Does anyone know whether it is possible to ? I'd be happy to even get some pointers to look more deeply into the problem, as I'm not even sure what to search for at this point.

Thanks!

Edit: there's more on the question in these slides. So I can do it on integral domains and fields through a connection with the reals. I'd really like to do it for arbitrary semirings, though.

1

# Proving inequalities over algebraic structures

I've been looking at proof techniques in formal systems like Coq and Agda recently, and encountered the newring tactic described here for proving equalities over arbitrary (semi)rings. It does this by reducing the generated polynomials to a Horner normal form and comparing equality over that.

That got me wondering whether a similar approach is possible for inequalities over general "ordered semirings" (where the order fits with the semiring operations). Someone pointed me to the omega tactic in Coq, for proving arbitrary statements (including inequalities) about Presburger arithmetic (with some restricted simulated multiplication). Anyway, it's clearly possible for Presburger arithmetic because all statements are decidable, but I don't really care about all statements, and was wondering whether it was possible for a particular algebraic structure without relying on properties of particular structures like the integers or reals.

Does anyone know whether it is possible to ? I'd be happy to even get some pointers to look more deeply into the problem, as I'm not even sure what to search for at this point.

Thanks!