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, it can only be used with a working internet connection.

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 SageMath can understand. It then calls 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.

In fact, polyrith uses Sage to test for membership in the radical of the ideal. This means it searches for a linear combination of hypotheses that add up to a power of the goal. When this power is not 1, it uses the (exp := n) feature of linear_combination to report the certificate.

TODO

• Give Sage more information about the specific ring being used for the coefficients. For now, we always use ℚ (or QQ in Sage).
• Handle • terms.
• Support local Sage installations.

References

• 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 Y. Lewis, who advised me on this project as part of a Computer Science independent study at Brown University.

Poly Datatype

inductive Mathlib.Tactic.Polyrith.Poly : Type

A datatype representing the semantics of multivariable polynomials. Each Poly can be converted into a string.

• const : ℚ → Poly
• var : ℕ → Poly
• hyp : Lean.Term → Poly
• add : Poly → Poly → Poly
• sub : Poly → Poly → Poly
• mul : Poly → Poly → Poly
• div : Poly → Poly → Poly
• pow : Poly → Poly → Poly
• neg : Poly → Poly

instance Mathlib.Tactic.Polyrith.instBEqPoly : BEq Poly

Equations

• Mathlib.Tactic.Polyrith.instBEqPoly = { beq := Mathlib.Tactic.Polyrith.beqPoly✝ }

instance Mathlib.Tactic.Polyrith.instReprPoly : Repr Poly

Equations

• Mathlib.Tactic.Polyrith.instReprPoly = { reprPrec := Mathlib.Tactic.Polyrith.reprPoly✝ }

def Mathlib.Tactic.Polyrith.Poly.format : Poly → Std.Format

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 vars (see sageCreateQuery).

Equations

• (Mathlib.Tactic.Polyrith.Poly.const a).format = Std.Format.text (toString a)
• (Mathlib.Tactic.Polyrith.Poly.var a).format = Std.Format.text (toString "vars[" ++ toString a ++ toString "]")
• (Mathlib.Tactic.Polyrith.Poly.hyp a).format = Std.Format.text (toString "hyp" ++ toString a ++ toString "")
• (a.add a_1).format = Std.Format.text (toString "(" ++ toString a.format ++ toString " + " ++ toString a_1.format ++ toString ")")
• (a.sub a_1).format = Std.Format.text (toString "(" ++ toString a.format ++ toString " - " ++ toString a_1.format ++ toString ")")
• (a.mul a_1).format = Std.Format.text (toString "(" ++ toString a.format ++ toString " * " ++ toString a_1.format ++ toString ")")
• (a.div a_1).format = Std.Format.text (toString "(" ++ toString a.format ++ toString " / " ++ toString a_1.format ++ toString ")")
• (a.pow a_1).format = Std.Format.text (toString "(" ++ toString a.format ++ toString " ^ " ++ toString a_1.format ++ toString ")")
• a.neg.format = Std.Format.text (toString "-" ++ toString a.format ++ toString "")

instance Mathlib.Tactic.Polyrith.instToFormatPoly : Std.ToFormat Poly

Equations

• Mathlib.Tactic.Polyrith.instToFormatPoly = { format := Mathlib.Tactic.Polyrith.Poly.format }

instance Mathlib.Tactic.Polyrith.instToStringPoly : ToString Poly

Equations

• Mathlib.Tactic.Polyrith.instToStringPoly = { toString := fun (x : Mathlib.Tactic.Polyrith.Poly) => toString x.format }

instance Mathlib.Tactic.Polyrith.instReprPoly_1 : Repr Poly

Equations

• Mathlib.Tactic.Polyrith.instReprPoly_1 = { reprPrec := fun (p : Mathlib.Tactic.Polyrith.Poly) (x : ℕ) => p.format }

instance Mathlib.Tactic.Polyrith.instInhabitedPoly : Inhabited Poly

Equations

• Mathlib.Tactic.Polyrith.instInhabitedPoly = { default := Mathlib.Tactic.Polyrith.Poly.const 0 }

instance Mathlib.Tactic.Polyrith.instQuoteIntMkStr1_mathlib : Lean.Quote ℤ

Equations

• One or more equations did not get rendered due to their size.

instance Mathlib.Tactic.Polyrith.instQuoteRatMkStr1_mathlib : Lean.Quote ℚ

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.Poly.toSyntax (vars : Array Lean.Term) : Poly → Lean.Unhygienic Lean.Term

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

Equations

• 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

partial def Mathlib.Tactic.Polyrith.parse {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (c : Ring.Cache sα) (e : Q(«$α»)) : AtomM Poly

Reifies a ring expression of type α as a Poly.

inductive Mathlib.Tactic.Polyrith.Source : Type

The possible hypothesis sources for a polyrith proof.

• input : ℕ → Source

  input n refers to the n'th input ai in polyrith [a1, ..., an].

• fvar : Lean.FVarId → Source

  fvar h refers to hypothesis h from the local context.

def Mathlib.Tactic.Polyrith.parseContext (only : Bool) (hyps : Array Lean.Expr) (target : Lean.Expr) : AtomM (Lean.Expr × Array (Source × Poly) × Poly)

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.parseContext.processHyp (v : Lean.Level) (α : Q(Type v)) (sα : Q(CommSemiring «$α»)) (c : Ring.Cache sα) (src : Source) (ty : Lean.Expr) (out : Array (Source × Poly)) : AtomM (Array (Source × Poly))

Parses a hypothesis and adds it to the out list.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.instFromJsonRat_mathlib : Lean.FromJson ℚ

A JSON parser for ℚ specific to the return value of Sage.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.Poly.unNeg? : Poly → Option Poly

Removes an initial - sign from a polynomial with negative leading coefficient.

Equations

• (a.mul b).unNeg? = do let __do_lift ← a.unNeg? pure (__do_lift.mul b)
• (Mathlib.Tactic.Polyrith.Poly.const i).unNeg? = if i < 0 then some (Mathlib.Tactic.Polyrith.Poly.const (-i)) else none
• p.neg.unNeg? = some p
• x✝.unNeg? = none

def Mathlib.Tactic.Polyrith.Poly.add' : Poly → Poly → Poly

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

Equations

• (Mathlib.Tactic.Polyrith.Poly.const { num := Int.ofNat 0, den_nz := ⋯, reduced := ⋯ }).add' x✝ = match x✝.unNeg? with | some np => np.neg | none => x✝
• x✝.add' (Mathlib.Tactic.Polyrith.Poly.const { num := Int.ofNat 0, den_nz := ⋯, reduced := ⋯ }) = x✝
• x✝¹.add' x✝ = match x✝.unNeg? with | some nb => x✝¹.sub nb | none => x✝¹.add x✝

def Mathlib.Tactic.Polyrith.Poly.mul' : Poly → Poly → Poly

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

Equations

• (Mathlib.Tactic.Polyrith.Poly.const { num := Int.ofNat 0, den_nz := ⋯, reduced := ⋯ }).mul' x✝ = Mathlib.Tactic.Polyrith.Poly.const 0
• (Mathlib.Tactic.Polyrith.Poly.const { num := Int.ofNat 1, den_nz := ⋯, reduced := ⋯ }).mul' x✝ = x✝
• x✝.mul' (Mathlib.Tactic.Polyrith.Poly.const { num := Int.ofNat 1, den_nz := ⋯, reduced := ⋯ }) = x✝
• x✝¹.mul' x✝ = x✝¹.mul x✝

def Mathlib.Tactic.Polyrith.Poly.unDiv? : Poly → Option (Poly × ℕ)

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

Equations

• (a.mul b).unDiv? = do let __discr ← a.unDiv? match __discr with | (a, r) => pure (a.mul' b, r)
• (Mathlib.Tactic.Polyrith.Poly.const i).unDiv? = if i.num = 1 ∧ i.den ≠ 1 then some (Mathlib.Tactic.Polyrith.Poly.const ↑i.num, i.den) else none
• p.neg.unDiv? = do let __discr ← p.unDiv? match __discr with | (p, r) => pure (p.neg, r)
• x✝.unDiv? = none

def Mathlib.Tactic.Polyrith.Poly.pow' : ℕ → ℕ → Poly

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

Equations

• Mathlib.Tactic.Polyrith.Poly.pow' x✝ 0 = Mathlib.Tactic.Polyrith.Poly.const 1
• Mathlib.Tactic.Polyrith.Poly.pow' x✝ 1 = Mathlib.Tactic.Polyrith.Poly.var x✝
• Mathlib.Tactic.Polyrith.Poly.pow' x✝¹ x✝ = (Mathlib.Tactic.Polyrith.Poly.var x✝¹).pow (Mathlib.Tactic.Polyrith.Poly.const ↑x✝)

def Mathlib.Tactic.Polyrith.Poly.sumM {m : Type → Type u_1} {α : Type u_2} [Monad m] (a : Array α) (f : α → m Poly) : m Poly

Constructs a sum from a monadic function supplying the monomials.

Equations

• One or more equations did not get rendered due to their size.

instance Mathlib.Tactic.Polyrith.instFromJsonPoly : Lean.FromJson Poly

Equations

• One or more equations did not get rendered due to their size.

structure Mathlib.Tactic.Polyrith.SageCoeffAndPower : Type

A schema for the data reported by the Sage calculation

• coeffs : Array Poly

  The function call produces an array of polynomials parallel to the input list of hypotheses.

• power : ℕ

  Sage produces an exponent (default 1) in the case where the hypothesess sum to a power of the goal.

instance Mathlib.Tactic.Polyrith.instFromJsonSageCoeffAndPower : Lean.FromJson SageCoeffAndPower

Equations

• Mathlib.Tactic.Polyrith.instFromJsonSageCoeffAndPower = { fromJson? := Mathlib.Tactic.Polyrith.fromJsonSageCoeffAndPower✝ }

instance Mathlib.Tactic.Polyrith.instReprSageCoeffAndPower : Repr SageCoeffAndPower

Equations

• Mathlib.Tactic.Polyrith.instReprSageCoeffAndPower = { reprPrec := Mathlib.Tactic.Polyrith.reprSageCoeffAndPower✝ }

structure Mathlib.Tactic.Polyrith.SageSuccess : Type

The result of a sage call in the success case.

• trace : Option String

  The script returns a string containing python script to be sent to the remote server, when the tracing option is set.

• data : Option SageCoeffAndPower

  The main result of the function call is an array of polynomials parallel to the input list of hypotheses and an exponent for the goal.

instance Mathlib.Tactic.Polyrith.instFromJsonSageSuccess : Lean.FromJson SageSuccess

Equations

• Mathlib.Tactic.Polyrith.instFromJsonSageSuccess = { fromJson? := Mathlib.Tactic.Polyrith.fromJsonSageSuccess✝ }

instance Mathlib.Tactic.Polyrith.instReprSageSuccess : Repr SageSuccess

Equations

• Mathlib.Tactic.Polyrith.instReprSageSuccess = { reprPrec := Mathlib.Tactic.Polyrith.reprSageSuccess✝ }

structure Mathlib.Tactic.Polyrith.SageError : Type

The result of a sage call in the failure case.

• name : String

  The error kind

• value : String

  The error message

instance Mathlib.Tactic.Polyrith.instFromJsonSageError : Lean.FromJson SageError

Equations

• Mathlib.Tactic.Polyrith.instFromJsonSageError = { fromJson? := Mathlib.Tactic.Polyrith.fromJsonSageError✝ }

def Mathlib.Tactic.Polyrith.SageResult : Type

The result of a sage call.

Equations

• Mathlib.Tactic.Polyrith.SageResult = Except Mathlib.Tactic.Polyrith.SageError Mathlib.Tactic.Polyrith.SageSuccess

Interaction with SageMath

def Mathlib.Tactic.Polyrith.sageHelperFunctions : String

These are Sage functions that test membership in the radical and format the output. See https://github.com/sagemath/sage/blob/f8df80820dc7321dc9b18c9644c3b8315999670b/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx#L4472-L4518 for a description of MPolynomial_libsingular.lift.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.sageTypeStr : Lean.Expr → String

The Sage type to use, given a base type of the target. Currently always rational numbers (QQ). Future extensions may change behavior depending on the base type.

Equations

• Mathlib.Tactic.Polyrith.sageTypeStr x✝ = "QQ"

def Mathlib.Tactic.Polyrith.sageCreateQuery (α : Lean.Expr) (atoms : ℕ) (hyps : Array (Source × Poly)) (target : Poly) : IO String

Create a Sage script to send to SageMath API.

Equations

• One or more equations did not get rendered due to their size.

instance Mathlib.Tactic.Polyrith.instFromJsonSageResult : Lean.FromJson SageResult

Parse a SageResult from the raw SageMath API output.

Equations

• One or more equations did not get rendered due to their size.

opaque Mathlib.Tactic.Polyrith.polyrith.sageUserAgent : Lean.Option String

The User-Agent header value for HTTP calls to SageMath API

def Mathlib.Tactic.Polyrith.runSage (trace : Bool) (α : Lean.Expr) (atoms : ℕ) (hyps : Array (Source × Poly)) (target : Poly) : Lean.CoreM SageResult

This function calls the Sage API at https://sagecell.sagemath.org/service. The output is parsed as SageResult.

Equations

• One or more equations did not get rendered due to their size.

Main function

def Mathlib.Tactic.Polyrith.polyrith (g : Lean.MVarId) (only : Bool) (hyps : Array Lean.Expr) (traceOnly : Bool := false) : Lean.MetaM (Except Lean.MVarId (Lean.TSyntax `tactic))

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 an appropriate SageMath script that executes a Groebner basis computation, which is sent to SageMath's API server. The output of this computation is a JSON representing the certificate. This JSON is parsed into the power of the goal and 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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.polyrith.byRing (g : Lean.MVarId) (msg : String) : AtomM (Except Lean.MVarId (Lean.TSyntax `tactic))

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Polyrith.«tacticPolyrithOnly[_]» : Lean.ParserDescr

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 curl available on path.

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

axiom 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

Equations

• One or more equations did not get rendered due to their size.