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

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/ 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.


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/

Instances For

    Converts a Poly expression into a Syntax suitable as an input to linear_combination.

    Instances For

      The possible hypothesis sources for a polyrith proof.

      Instances For

        Constructs the list of arguments to pass to the external sage script

        Instances For

          A JSON parser for specific to the return value of

          Instances For

            Adds two polynomials, performing some simple simplifications for presentation like a + -b = a - b.

            Instances For

              Multiplies two polynomials, performing some simple simplifications for presentation like 1 * a = a.

              Instances For

                Extracts the divisor c : ℕ from a polynomial of the form 1/c * b.

                Instances For

                  Constructs a power expression v_i ^ j, performing some simplifications in trivial cases.

                  Instances For

                    Constructs a sum from a monadic function supplying the monomials.

                    Instances For
                      • trace : Option String

                        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.

                      Instances For

                        The result of a sage call in the failure case.

                        Instances For

                          The result of a sage call.

                          Instances For

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

                            Instances For

                              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 .missing

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

                              Returns .error g if this was a "dry run" attempt that does not actually invoke sage.

                              Instances For

                                Try to prove the goal by ring and fail with the given message otherwise.

                                Instances For

                                  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.


                                  • This tactic only works with a working internet connection, since it calls Sage using the SageCell web API at 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.


                                  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
                                  Instances For