Stream: Miscellaneous

Topic: lra, but on arbitrary ordered field

view this post on Zulip 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?

view this post on Zulip Pierre Roux (May 31 2023 at 10:56):

In you have the lra tactic for any realDomainType or realFieldType (hence `rat), don't know if that's what you are looking for.

view this post on Zulip Lessness (May 31 2023 at 14:46):

Will take a look, thank you!

Last updated: Jun 17 2024 at 22:01 UTC