field_simp tactic

Tactic to clear denominators in algebraic expressions.

Lists of expressions representing exponents and atoms, and operations on such lists

@[reducible, inline]

abbrev Mathlib.Tactic.FieldSimp.qNF {v : Lean.Level} (M : Q(Type v)) : Type

Basic meta-code "normal form" object of the field_simp tactic: a type synonym for a list of ordered triples comprising an expression representing a term of a type M (where typically M is a field), together with an integer "power" and a natural number "index".

The natural number represents the index of the M term in the AtomM monad: this is not enforced, but is sometimes assumed in operations. Thus when items ((a₁, x₁), k) and ((a₂, x₂), k) appear in two different FieldSimp.qNF objects (i.e. with the same ℕ-index k), it is expected that the expressions x₁ and x₂ are the same. It is also expected that the items in a FieldSimp.qNF list are in strictly decreasing order by natural-number index.

By forgetting the natural number indices, an expression representing a Mathlib.Tactic.FieldSimp.NF object can be built from a FieldSimp.qNF object; this construction is provided as Mathlib.Tactic.FieldSimp.qNF.toNF.

Equations

• Mathlib.Tactic.FieldSimp.qNF M = List ((ℤ × Q(«$M»)) × ℕ)

def Mathlib.Tactic.FieldSimp.qNF.toNF {v : Lean.Level} {M : Q(Type v)} (l : qNF q(«$M»)) : Q(NF «$M»)

Given l of type qNF M, i.e. a list of (ℤ × Q($M)) × ℕs (two Exprs and a natural number), build an Expr representing an object of type NF M (i.e. List (ℤ × M)) in the in the obvious way: by forgetting the natural numbers and gluing together the integers and Exprs.

Equations

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

def Mathlib.Tactic.FieldSimp.qNF.onExponent {v : Lean.Level} {M : Q(Type v)} (l : qNF M) (f : ℤ → ℤ) : qNF M

Given l of type qNF M, i.e. a list of (ℤ × Q($M)) × ℕs (two Exprs and a natural number), apply an expression representing a function with domain ℤ to each of the ℤ components.

Equations

• l.onExponent f = List.map (fun (x : (ℤ × Q(«$M»)) × ℕ) => match x with | ((a, x), k) => ((f a, x), k)) l

def Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial {v : Lean.Level} {M : Q(Type v)} (iM : Q(GroupWithZero «$M»)) (r : ℤ) (x : Q(«$M»)) : Lean.MetaM ((e : Q(«$M»)) × Q(zpow' «$x» «$r» = «$e»))

Build a transparent expression for the product of powers represented by l : qNF M.

Equations

• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM 0 x = pure ⟨q(«$x» / «$x»), q(⋯)⟩
• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM 1 x = pure ⟨x, q(⋯)⟩
• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM (Int.ofNat r_2) x = do let pf ← Qq.mkDecideProofQ q(«$r_2» ≠ 0) pure ⟨q(«$x» ^ «$r_2»), q(⋯)⟩
• Mathlib.Tactic.FieldSimp.qNF.evalPrettyMonomial iM r x = do let pf ← Qq.mkDecideProofQ q(«$r» ≠ 0) pure ⟨q(«$x» ^ «$r»), q(⋯)⟩

def Mathlib.Tactic.FieldSimp.qNF.tryClearZero {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (r : ℤ) (x : Q(«$M»)) (i : ℕ) (l : qNF M) : Lean.MetaM ((l' : qNF M) × have a := l'.toNF; have a_1 := toNF (((r, x), i) :: l); Q(«$a_1».eval = «$a».eval))

Try to drop an expression zpow' x r from the beginning of a product. If r ≠ 0 this of course can't be done. If r = 0, then zpow' x r is equal to x / x, so it can be simplified to 1 (hence dropped from the beginning of the product) if we can find a proof that x ≠ 0.

Equations

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

def Mathlib.Tactic.FieldSimp.qNF.removeZeros {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (l : qNF M) : Lean.MetaM ((l' : qNF M) × have a := l'.toNF; have a_1 := l.toNF; Q(«$a_1».eval = «$a».eval))

Given l : qNF M, obtain l' : qNF M by removing all l's exponent-zero entries where the corresponding atom can be proved nonzero, and construct a proof that their associated expressions are equal.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.removeZeros disch iM [] = pure ⟨[], q(⋯)⟩

def Mathlib.Tactic.FieldSimp.qNF.split {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l : qNF M) : Lean.MetaM ((l_n : qNF M) × (l_d : qNF M) × have a := l_d.toNF; have a_1 := l_n.toNF; have a_2 := l.toNF; Q(«$a_2».eval = «$a_1».eval / «$a».eval))

Given a product of powers, split as a quotient: the positive powers divided by (the negations of) the negative powers.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.split iM [] = pure ⟨[], ⟨[], q(⋯)⟩⟩

def Mathlib.Tactic.FieldSimp.qNF.evalPretty {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l : qNF M) : Lean.MetaM ((e : Q(«$M»)) × have a := l.toNF; Q(«$a».eval = «$e»))

Build a transparent expression for the product of powers represented by l : qNF M.

Equations

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

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.mul {v : Lean.Level} {M : Q(Type v)} : qNF q(«$M») → qNF q(«$M») → qNF q(«$M»)

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), construct another such term l, which will have the property that in the field $M, the product of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by l.

The construction assumes, to be valid, that the lists l₁ and l₂ are in strictly decreasing order by ℕ-component, and that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then the expressions x₁ and x₂ are equal.

The construction is as follows: merge the two lists, except that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then contribute a term (a₁ + a₂, x₁) to the output list with ℕ-component k.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.mul [] x✝ = x✝
• x✝.mul [] = x✝

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.mkMulProof {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : qNF M) : have a := (l₁.mul l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval * «$a_1».eval = «$a».eval)

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), recursively construct a proof that in the field $M, the product of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by FieldSimp.qNF.mul l₁ l₁.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM [] l₂ = q(⋯)
• Mathlib.Tactic.FieldSimp.qNF.mkMulProof iM l₁ [] = q(⋯)

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.div {v : Lean.Level} {M : Q(Type v)} : qNF M → qNF M → qNF M

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), construct another such term l, which will have the property that in the field $M, the quotient of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by l.

The construction assumes, to be valid, that the lists l₁ and l₂ are in strictly decreasing order by ℕ-component, and that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then the expressions x₁ and x₂ are equal.

The construction is as follows: merge the first list and the negation of the second list, except that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then contribute a term (a₁ - a₂, x₁) to the output list with ℕ-component k.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.div [] x✝ = x✝.onExponent Neg.neg
• x✝.div [] = x✝

@[irreducible]

def Mathlib.Tactic.FieldSimp.qNF.mkDivProof {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : qNF M) : have a := (l₁.div l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval / «$a_1».eval = «$a».eval)

Given two terms l₁, l₂ of type qNF M, i.e. lists of (ℤ × Q($M)) × ℕs (an integer, an Expr and a natural number), recursively construct a proof that in the field $M, the quotient of the "multiplicative linear combinations" represented by l₁ and l₂ is the multiplicative linear combination represented by FieldSimp.qNF.div l₁ l₁.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM [] l₂ = q(⋯)
• Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM l₁ [] = q(⋯)

partial def Mathlib.Tactic.FieldSimp.qNF.gcd {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : qNF M) (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (nonzero : Bool) : Lean.MetaM ((L : qNF M) × (l₁' : qNF M) × (l₂' : qNF M) × (have a := l₁.toNF; have a_1 := l₁'.toNF; have a_2 := L.toNF; Q(«$a_2».eval * «$a_1».eval = «$a».eval)) × (have a := l₂.toNF; have a_1 := l₂'.toNF; have a_2 := L.toNF; Q(«$a_2».eval * «$a_1».eval = «$a».eval)) × have a := L.toNF; Q(«$a».eval ≠ 0))

Extract a common factor L of two products-of-powers l₁ and l₂ in M, in the sense that both l₁ and l₂ are quotients by L of products of positive powers.

The boolean flag nonzero specifies whether we extract a certified nonzero (and therefore potentially smaller) common factor. The metaprogram returns a "proof" that this common factor is nonzero, i.e. an expression Q(NF.eval $(L.toNF) ≠ 0), but this will be junk if the boolean flag nonzero is set to false.

Core of the field_simp tactic

partial def Mathlib.Tactic.FieldSimp.normalize {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (x : Q(«$M»)) : AtomM ((y : Q(«$M»)) × ((g : Sign M) × have a := g.expr y; Q(«$x» = «$a»)) × (l : qNF M) × have a := l.toNF; Q(«$y» = «$a».eval))

The main algorithm behind the field_simp tactic: partially-normalizing an expression in a field M into the form x1 ^ c1 * x2 ^ c2 * ... x_k ^ c_k, where x1, x2, ... are distinct atoms in M, and c1, c2, ... are integers.

def Mathlib.Tactic.FieldSimp.reduceExprQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (x : Q(«$M»)) : AtomM ((x' : Q(«$M»)) × Q(«$x» = «$x'»))

Given x in a commutative group-with-zero, construct a new expression in the standard form *** / *** (all denominators at the end) which is equal to x.

Equations

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

def Mathlib.Tactic.FieldSimp.reduceEqQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (e₁ e₂ : Q(«$M»)) : AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» = «$e₂») = («$f₁» = «$f₂»)))

Given e₁ and e₂, cancel nonzero factors to construct a new equality which is logically equivalent to e₁ = e₂.

Equations

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

def Mathlib.Tactic.FieldSimp.reduceExpr (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (x : Lean.Expr) : AtomM Lean.Meta.Simp.Result

Given x in a commutative group-with-zero, construct a new expression in the standard form *** / *** (all denominators at the end) which is equal to x.

def Mathlib.Tactic.FieldSimp.reduceEq (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (t : Lean.Expr) : AtomM Lean.Meta.Simp.Result

Given an equality a = b, cancel nonzero factors to construct a new equality which is logically equivalent to a = b.

Frontend

def Mathlib.Tactic.FieldSimp.parseDischarger (d : Option (Lean.TSyntax `Lean.Parser.Tactic.discharger)) (args : Option (Lean.TSyntax `Lean.Parser.Tactic.simpArgs)) : Lean.Elab.Tactic.TacticM ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»))

If the user provided a discharger, elaborate it. If not, we will use the field_simp default discharger, which (among other things) includes a simp-run for the specified argument list, so we elaborate those arguments.

Equations

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

def Mathlib.Tactic.FieldSimp.fieldSimp : Lean.ParserDescr

The goal of field_simp is to reduce an expression in a field to an expression of the form n / d where neither n nor d contains any division symbol.

If the goal is an equality, this tactic will also clear the denominators, so that the proof can normally be concluded by an application of ring.

For example,

example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
    a + b / x + c / x ^ 2 + d / x ^ 3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) := by
  field_simp
  ring

Cancelling and combining denominators often requires "nonzeroness" side conditions. The field_simp tactic attempts to discharge these, and will omit such steps if it cannot discharge the corresponding side conditions. The discharger will try, among other things, positivity and norm_num, and will also use any nonzeroness proofs included explicitly (e.g. field_simp [hx]). If your expression is not completely reduced by field_simp, check the denominators of the resulting expression and provide proofs that they are nonzero to enable further progress.

Equations

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

def Mathlib.Tactic.FieldSimp.convField_simp__ : Lean.ParserDescr

The goal of field_simp is to reduce an expression in a field to an expression of the form n / d where neither n nor d contains any division symbol.

If the goal is an equality, this tactic will also clear the denominators, so that the proof can normally be concluded by an application of ring.

For example,

example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
    a + b / x + c / x ^ 2 + d / x ^ 3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) := by
  field_simp
  ring

Cancelling and combining denominators often requires "nonzeroness" side conditions. The field_simp tactic attempts to discharge these, and will omit such steps if it cannot discharge the corresponding side conditions. The discharger will try, among other things, positivity and norm_num, and will also use any nonzeroness proofs included explicitly (e.g. field_simp [hx]). If your expression is not completely reduced by field_simp, check the denominators of the resulting expression and provide proofs that they are nonzero to enable further progress.

Equations

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

def field : Lean.Meta.Simp.Simproc

The goal of field_simp is to reduce an expression in a field to an expression of the form n / d where neither n nor d contains any division symbol.

If the goal is an equality, this tactic will also clear the denominators, so that the proof can normally be concluded by an application of ring.

For example,

example (a b c d x y : ℂ) (hx : x ≠ 0) (hy : y ≠ 0) :
    a + b / x + c / x ^ 2 + d / x ^ 3 = a + x⁻¹ * (y * b / y + (d / x + c) / x) := by
  field_simp
  ring

Cancelling and combining denominators often requires "nonzeroness" side conditions. The field_simp tactic attempts to discharge these, and will omit such steps if it cannot discharge the corresponding side conditions. The discharger will try, among other things, positivity and norm_num, and will also use any nonzeroness proofs included explicitly (e.g. field_simp [hx]). If your expression is not completely reduced by field_simp, check the denominators of the resulting expression and provide proofs that they are nonzero to enable further progress.

Equations

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

We register field_simp with the hint tactic.