polyrith Tactic #
In this file, the
polyrith tactic is created. This tactic, which
Fields, attempts to prove a multivariate polynomial target over said
field by using multivariable polynomial hypotheses/proof terms over the same field.
Used as is, the tactic makes use of those hypotheses in the local context that are
over the same field as the target. However, the user can also specify which hypotheses
from the local context to use, along with proof terms that might not already be in the
local context. Note: since this tactic uses SageMath via an API call done in Python,
it can only be used with a working internet connection, and with a local installation of Python.
Implementation Notes #
linear_combination is often used to prove such goals by allowing the user to
specify a coefficient for each hypothesis. If the target polynomial can be written as a
linear combination of the hypotheses with the chosen coefficients, then the
tactic succeeds. In other words,
linear_combination is a certificate checker, and it is left
to the user to find a collection of good coefficients. The
polyrith tactic automates this
process using the theory of Groebner bases.
Polyrith does this by first parsing the relevant hypotheses into a form that Python can understand.
It then calls a Python file that uses the SageMath API to compute the coefficients. These
coefficients are then sent back to Lean, which parses them into pexprs. The information is then
given to the
linear_combination tactic, which completes the process by checking the certificate.
polyrith calls an external python script
scripts/polyrith_sage.py. Because this is not a Lean
file, changes to this script may not be noticed during Lean compilation if you have already
generated olean files. If you are modifying this python script, you likely know what you're doing;
remember to force recompilation of any files that call
- Give Sage more information about the specific ring being used for the coefficients. For now,
we always use ℚ (or
- Support local Sage installations.
- See the book [Ideals, Varieties, and Algorithms][coxlittleOshea1997] by David Cox, John Little, and Donal O'Shea for the background theory on Groebner bases
- This code was heavily inspired by the code for the tactic
linarith, which was written by Robert Lewis, who advised me on this project as part of a Computer Science independent study at Brown University.
Poly Datatype #
- const: ℚ → Mathlib.Tactic.Polyrith.Poly
- var: ℕ → Mathlib.Tactic.Polyrith.Poly
- hyp: Lean.Term → Mathlib.Tactic.Polyrith.Poly
- add: Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly
- sub: Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly
- mul: Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly
- div: Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly
- pow: Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly
- neg: Mathlib.Tactic.Polyrith.Poly → Mathlib.Tactic.Polyrith.Poly
A datatype representing the semantics of multivariable polynomials.
poly can be converted into a string.
This converts a poly object into a string representing it. The string maintains the semantic structure of the poly object.
The output of this function must be valid Python syntax, and it assumes the variables
- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.Polyrith.Poly.format (Mathlib.Tactic.Polyrith.Poly.const a) = Std.Format.text (toString a)
- Mathlib.Tactic.Polyrith.Poly.format (Mathlib.Tactic.Polyrith.Poly.var a) = Std.Format.text (toString "var" ++ toString a ++ toString "")
- Mathlib.Tactic.Polyrith.Poly.format (Mathlib.Tactic.Polyrith.Poly.hyp a) = Std.Format.text (toString "hyp" ++ toString a ++ toString "")
- Mathlib.Tactic.Polyrith.Poly.format (Mathlib.Tactic.Polyrith.Poly.neg a) = Std.Format.text (toString "-" ++ toString (Mathlib.Tactic.Polyrith.Poly.format a) ++ toString "")
Poly expression into a
Syntax suitable as an input to
- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.Polyrith.Poly.toSyntax vars (Mathlib.Tactic.Polyrith.Poly.const a) = pure (Lean.quote `term a)
- Mathlib.Tactic.Polyrith.Poly.toSyntax vars (Mathlib.Tactic.Polyrith.Poly.var a) = pure vars[a]!
- Mathlib.Tactic.Polyrith.Poly.toSyntax vars (Mathlib.Tactic.Polyrith.Poly.hyp a) = pure a
- input: ℕ → Mathlib.Tactic.Polyrith.Source
- fvar: Lean.FVarId → Mathlib.Tactic.Polyrith.Source
fvar hrefers to hypothesis
hfrom the local context.
The possible hypothesis sources for a polyrith proof.
The first half of
polyrith produces a list of arguments to be sent to Sage.
Constructs the list of arguments to pass to the external sage script
Removes an initial
- sign from a polynomial with negative leading coefficient.
- Mathlib.Tactic.Polyrith.Poly.unNeg? (Mathlib.Tactic.Polyrith.Poly.mul a b) = do let __do_lift ← Mathlib.Tactic.Polyrith.Poly.unNeg? a pure (Mathlib.Tactic.Polyrith.Poly.mul __do_lift b)
- Mathlib.Tactic.Polyrith.Poly.unNeg? (Mathlib.Tactic.Polyrith.Poly.const i) = if i < 0 then some (Mathlib.Tactic.Polyrith.Poly.const (-i)) else none
- Mathlib.Tactic.Polyrith.Poly.unNeg? (Mathlib.Tactic.Polyrith.Poly.neg p) = some p
- Mathlib.Tactic.Polyrith.Poly.unNeg? x = none
Extracts the divisor
c : ℕ from a polynomial of the form
1/c * b.
The script returns a string containing python script to be sent to the remote server, when the tracing option is set.
The main result of the function call is an array of polynomials parallel to the input list of hypotheses.
The result of a sage call in the success case.
This is the main body of the
polyrith tactic. It takes in the following inputs:
only : Bool- This represents whether the user used the key word "only"
hyps : Array Expr- the hypotheses/proof terms selected by the user
traceOnly : Bool- If enabled, the returned syntax will be
First, the tactic converts the target into a
Poly, and finds out what type it
is an equality of. (It also fills up a list of
Exprs with its atoms). Then, it
collects all the relevant hypotheses/proof terms from the context, and from those
selected by the user, taking into account whether
only is true. (The list of atoms is
updated accordingly as well).
This information is used to create a list of args that get used in a call to
the appropriate python file that executes a grobner basis computation. The
output of this computation is a
String representing the certificate. This
string is parsed into a list of
Poly objects that are then converted into
Exprs (using the updated list of atoms).
the names of the hypotheses, along with the corresponding coefficients are
linear_combination. If that tactic succeeds, the user is prompted
to replace the call to
polyrith with the appropriate call to
.error g if this was a "dry run" attempt that does not actually invoke sage.
Attempts to prove polynomial equality goals through polynomial arithmetic
on the hypotheses (and additional proof terms if the user specifies them).
It proves the goal by generating an appropriate call to the tactic
linear_combination. If this call succeeds, the call to
is suggested to the user.
polyrithwill use all relevant hypotheses in the local context.
polyrith [t1, t2, t3]will add proof terms t1, t2, t3 to the local context.
polyrith only [h1, h2, h3, t1, t2, t3]will use only local hypotheses
h3, and proofs
t3. It will ignore the rest of the local context.
- This tactic only works with a working internet connection, since it calls Sage using the SageCell web API at https://sagecell.sagemath.org/. Many thanks to the Sage team and organization for allowing this use.
- This tactic assumes that the user has
python3installed and available on the path. (Test by opening a terminal and executing
python3 --version.) It also assumes that the
requestslibrary is installed:
python3 -m pip install requests.
example (x y : ℚ) (h1 : x*y + 2*x = 1) (h2 : x = y) : x*y = -2*y + 1 := by polyrith -- Try this: linear_combination h1 - 2 * h2 example (x y z w : ℚ) (hzw : z = w) : x*z + 2*y*z = x*w + 2*y*w := by polyrith -- Try this: linear_combination (2 * y + x) * hzw constant scary : ∀ a b : ℚ, a + b = 0 example (a b c d : ℚ) (h : a + b = 0) (h2: b + c = 0) : a + b + c + d = 0 := by polyrith only [scary c d, h] -- Try this: linear_combination scary c d + h