Lessness (May 31 2023 at 10:35): Lessness (May 31 2023 at 10:35):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?
Pierre Roux (May 31 2023 at 10:56):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.
Lessness (May 31 2023 at 14:46):Will take a look, thank you!
Last updated: Nov 29 2023 at 21:01 UTC