mathlib3 documentation

tactic.polyrith

polyrith Tactic #

In this file, the polyrith tactic is created. This tactic, which works over 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 specifiy 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 #

The tactic 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 linear_combination 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 polyrith.

TODO #

References #

Poly Datatype #

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 varN from scripts/polyrith.py.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

Parsing algorithms #

The following section contains code that can convert an expr of type Prop into a poly object (provided that it is an equality)

(vars, p) ← poly_form_of_atom red vars e is the atomic case for poly_form_of_expr. If e appears with index k in vars, it returns the singleton sum p = poly.var k. Otherwise it updates vars, adding e with index n, and returns the singleton p = poly.var n.

poly_form_of_expr red map e computes the polynomial form of e.

map is a lookup map from atomic expressions to variable numbers. If a new atomic expression is encountered, it is added to the map with a new number. It matches atomic expressions up to reducibility given by red.

Because it matches up to definitional equality, this function must be in the tactic monad, and forces some functions that call it into tactic as well.

Un-Parsing algorithms #

The following section contains code that can convert an a poly object into a pexpr.

This can convert a poly into a pexpr that would evaluate to a polynomial. To do so, it uses a list m of expressions, the atomic expressions that appear in the poly. The index of an expression in this list corresponds to its poly.var argument: that is, if e is the kth element of m, then it is represented as poly.var k.

poly objects only contain coefficients from . However, the poly object might be referring to a polynomial over some other field. As such, the resulting pexpr contains no typing information.

Parsing SageMath output into a poly #

The following section contains code that can convert a string of appropriate format into a poly object. This is used later on to convert the coefficients given by Sage into poly objects.

A parser object that parses strings of the form "poly.var n" to the appropriate poly object representing a variable. Here, n is a natural number

A parser object that parses strings of the form "poly.const r" to the appropriate poly object representing a rational coefficient. Here, r is a rational number

A parser object that parses strings of the form "poly.add p q" to the appropriate poly object representing the sum of two polys. Here, p and q are themselves string forms of polys.

A parser object that parses strings of the form "poly.sub p q" to the appropriate poly object representing the subtraction of two polys. Here, p and q are themselves string forms of polys.

A parser object that parses strings of the form "poly.mul p q" to the appropriate poly object representing the product of two polys. Here, p and q are themselves string forms of polys.

A parser object that parses strings of the form "poly.pow p n" to the appropriate poly object representing a poly raised to the power of a natural number. Here, p is the string form of a poly and n is a natural number.

A parser object that parses strings of the form "poly.neg p" to the appropriate poly object representing the negation of a poly. Here, p is the string form of a poly.

A parser for poly that uses an s-essresion style formats such as (poly.add (poly.var 0) (poly.const 1).

A schema for success messages from the python script

Instances for polyrith.sage_json_success

A schema for failure messages from the python script

Instances for polyrith.sage_json_failure

Parse the json output from scripts/polyrith.py into either an error message, a list of poly objects, or none if only trace output was requested.

Parsing context into poly #

The following section contains code that collects hypotheses of the appropriate type from the context (and from the list of hypotheses and proof terms specified by the user) and converts them into poly objects.

Convert an expression of the form lhs = rhs into the form lhs - rhs

(vars, poly, typ) ← parse_target_to_poly interprets the current target (an equality over some field) into a poly. The result is a list of the atomic expressions in the target, the poly itself, and an expr representing the type of the field.

Filter l to the elements which are equalities of type expt.

meta def polyrith.parse_ctx_to_polys (expt : expr) (m : list expr) (only_on : bool) (hyps : list pexpr) :

The purpose of this tactic is to collect all the hypotheses and proof terms (specified by the user) that are equalities of the same type as the target. It takes in an expr representing the type, a list of expressions representing the atoms (typically this starts as only containing information about the target), a bool representing whether the user used the key word "only", and a list pexpr of all the hypotheses and proof terms selected by the user.

If the key word "only" is used, it collects together only those hypotheses/proof terms selected by the user. If not, they are combined with hypotheses from the local context. We throw out those hypotheses that are not equalities of the given type, and then modify each equality such that everything has been moved to the left of the "=" sign.

The tactic returns the names of these hypotheses (as exprs), a list of atoms updated with information from all these hypotheses, and a list of these hypotheses converted into poly objects.

Connecting with Python #

The following section contains code that allows lean to communicate with a python script.

This tactic calls python from the command line with the args in arg_list. The output printed to the console is returned as a string. It assumes that python3 is available on the path.

Adds parentheses around additions and subtractions, for printing at precedence 65.

Given a pair of exprs, where one represents the hypothesis/proof term, and the other representes the coefficient attached to it, this tactic creates a string combining the two in the appropriate format for linear_combination.

The boolean value returned is tt if the format needs to be negated to accurately reflect the input expressions. The negation is not applied in the format output by this function, because it may appear as a negation (if this is the first component) or a subtraction.

Given a list (bool × format), this function uses + and - to conjoin the formats in the list. A format is negated if its corresponding bool is tt.

This tactic repeats the process above for a list of pairs of exprs.

Connecting with Python #

The following section contains code that allows lean to communicate with a python script.

meta def polyrith.create_args (only_on : bool) (hyps : list pexpr) :

The first half of tactic.polyrith produces a list of arguments to be sent to Sage.

meta def polyrith.process_output (eq_names m : list expr) (R : expr) (sage_out : json) :

The second half of tactic.polyrith processes the output from Sage into a call to linear_combination.

Tactic for the special case when no hypotheses are available.

Tactic for the special case when there are no variables.

meta def tactic.polyrith (only_on : bool) (hyps : list pexpr) :

This is the main body of the polyrith tactic. It takes in the following inputs:

  • (only_on : bool) - This represents whether the user used the key word "only"
  • (hyps : list pexpr) - the hypotheses/proof terms selecteed by the user

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_on 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 pexprs (using the updated list of atoms).

the names of the hypotheses, along with the corresponding coefficients are given to linear_combination. If that tactic succeeds, the user is prompted to replace the call to polyrith with the appropriate call to linear_combination.

This returns none if this was a "dry run" attempt that does not actually invoke sage.

Interactivity #

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 linear_combination is suggested to the user.

  • polyrith will 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 h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

Notes:

  • 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 python3 installed and available on the path. (Test by opening a terminal and executing python3 --version.) It also assumes that the requests library is installed: python3 -m pip install requests.

Examples:

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
```

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 linear_combination is suggested to the user.

  • polyrith will 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 h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

Notes:

  • 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 python3 installed and available on the path. (Test by opening a terminal and executing python3 --version.) It also assumes that the requests library is installed: python3 -m pip install requests.

Examples:

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
```