Is it possible? I believe that Linear Programming (for example, simplex algorithm) should work on any ordered field (If I'm wrong, my apologies).

1) Could the "lra" tactic made to work with any given ordered field? (Don't know, having coefficients with decidable strict inequality, for example, rational numbers.)

2) Also, if it is not possible currently in the Coq - is this something that is really necessary?

In https://github.com/math-comp/algebra-tactics/ you have the lra tactic for any `realDomainType`

or `realFieldType`

(hence ``rat`

), don't know if that's what you are looking for.

Will take a look, thank you!

Last updated: Nov 29 2023 at 21:01 UTC