Documentation for the omega backend

Stream: general

[Frederick Pu]

Is there any easy way to use the omega tactic backend within my own metaprogram to find a solution to a set of linear inequalities?

[Eric Rodriguez]

Scott Morrison

[Kim Morrison]

Right now omega only proves contradiction, it does not provide a witness that a system of contraints is satisfiable. This is coming.

If proving a contradiction is useful in the meantime, I can explain how to use the backend, either from Expr containing your constraints or an some pre-existing internal representation you have.

[Frederick Pu]

Scott Morrison said:

Right now omega only proves contradiction, it does not provide a witness that a system of contraints is satisfiable. This is coming.

If proving a contradiction is useful in the meantime, I can explain how to use the backend, either from Expr containing your constraints or an some pre-existing internal representation you have.

I'm trying to assign a numerical value to each meta variable in the tactic state that satisfies the all the linear constraints in the tactic state. I'm doing this to visualize the graphs of arcs and lines who's coordinates are metavariables.

[Kim Morrison]

I don't precisely see what you're doing, but it does sound like omega won't be useful to you until omega is producing witnesses.

[Kim Morrison]

Note also that omega only works over Int and Nat: it is not a linear arithmetic procedure over Rat (or more general things).

[Mario Carneiro]

sounds like you might want a linear programming solver

[Frederick Pu]

Does lean have any linear programming solvers or will I just have to implement it myself.

[Henrik Böving]

Lean doesnt have an LP solver but there isn't really a reason to implement one yourself. Since you dont seem to have an optimality constraint you can just run an external LP solver, plug the numbers it spits out into Lean and (if you need it) run a proof by decide hat your variable assignment is valid.

[Frederick Pu]

Henrik Böving said:

Lean doesnt have an LP solver but there isn't really a reason to implement one yourself. Since you dont seem to have an optimality constraint you can just run an external LP solver, plug the numbers it spits out into Lean and (if you need it) run a proof by decide hat your variable assignment is valid.

I think using a foreign function interface would add too much overhead. Since my tactic is supposed visualize the proof state and not perform proof search like omega. Also think a native and certified linear proggraming algorithm would be pretty interesting thing to add to mathlib

[Henrik Böving]

Frederick Pu said:

Henrik Böving said:

Lean doesnt have an LP solver but there isn't really a reason to implement one yourself. Since you dont seem to have an optimality constraint you can just run an external LP solver, plug the numbers it spits out into Lean and (if you need it) run a proof by decide hat your variable assignment is valid.

I think using a foreign function interface would add too much overhead. Since my tactic is supposed visualize the proof state and not perform proof search like omega. Also think a native and certified linear proggraming algorithm would be pretty interesting thing to add to mathlib

Multiple things:

1. What do you mean by overhead? FFI would be simpler than writing your own, it is extremly unlikely that we'll be able to come up with a Lean solver that outruns external ones in terms of speed as well.
2. There is no need for FFI, you can simply call the solver as an external process and parse its output
3. I do agree on the native and certified LP algorithm but that seems like a ton of overhead :D

[Jannis Limperg]

FFI requires that users install the external solver. This would create a major barrier to the adoption of whatever Frederick is working on, assuming that this is a user-facing thing.

[Joachim Breitner]

Maybe lean needs to come with a bundled Wasm runtime and FFI, then all the projects that need to ship existing solvers (which almost always have a very simple system api demands for input/output) can do so as an embedded blob, and works on all platforms.

[Kevin Buzzard]

polyrith uses an external solver and we don't have to install sagemath to use it (but we do have to be connected to the internet)

[Joachim Breitner]

Brave new world…

[Henrik Böving]

Joachim Breitner said:

Brave new world…

Not that brave, Isabelle's sledgehammer can also call external solvers via the internet^^

[Rob Lewis]

The builtin solver for linarith probably isn't suitable for your needs, but if anyone did implement a generic lp solver in Lean or hook up an external one, it would be straightforward to plug it into linarith

[Joachim Breitner]

Maybe still brave, but therefore not so new :-). Does it do it by default?

I’m oldscool and don’t like if my tools use some random internet service behind my back, if only because I might be looking forward to a long productive train ride and suddenly things don’t work any more. But since we are soon all just going to be conversing with some cloud-based programming assisting AI anyways (I finally installed github copilot and it definitely has a appeal) it’s probably just fine.

[Henrik Böving]

It doesn't, iirc its the vampire prover and if you want to use the online version you have to pinky promise that its only for research or personal use, not commercial or something like that. (this pinky promise works by flipping a switch in your local isabelle install)