field_simp
tactic #
Tactic to clear denominators in algebraic expressions.
Lists of expressions representing exponents and atoms, and operations on such lists #
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
.
Instances For
Given l
of type qNF M
, i.e. a list of (ℤ × Q($M)) × ℕ
s (two Expr
s 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 Expr
s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given l
of type qNF M
, i.e. a list of (ℤ × Q($M)) × ℕ
s (two Expr
s and a natural
number), apply an expression representing a function with domain ℤ
to each of the ℤ
components.
Equations
Instances For
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(⋯)⟩
Instances For
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.
Instances For
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
Instances For
Given a product of powers, split as a quotient: the positive powers divided by (the negations of) the negative powers.
Equations
Instances For
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.
Instances For
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
Instances For
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(⋯)
Instances For
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✝
Instances For
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(⋯)
Instances For
Constraints on denominators which may need to be considered in field_simp
: no condition,
nonzeroness, or strict positivity.
- none {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} : DenomCondition iM
- nonzero {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} : DenomCondition iM
- positive {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} (iM' : Q(PartialOrder «$M»)) (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLT «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)) : DenomCondition iM
Instances For
Given a field-simp-normal-form expression L
(a product of powers of atoms), a proof (according
to the value of DenomCondition
) of that expression's nonzeroness, strict positivity, etc.
Equations
- Mathlib.Tactic.FieldSimp.DenomCondition.proof L Mathlib.Tactic.FieldSimp.DenomCondition.none = Unit
- Mathlib.Tactic.FieldSimp.DenomCondition.proof L Mathlib.Tactic.FieldSimp.DenomCondition.nonzero = Q(Mathlib.Tactic.FieldSimp.NF.eval unknown_1 ≠ 0)
- Mathlib.Tactic.FieldSimp.DenomCondition.proof L (Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''') = Q(0 < Mathlib.Tactic.FieldSimp.NF.eval unknown_1)
Instances For
The empty field-simp-normal-form expression []
(representing 1
as an empty product of powers
of atoms) can be proved to be nonzero, strict positivity, etc., as needed, as specified by the
value of DenomCondition
.
Equations
Instances For
Given a proof of the nonzeroness, strict positivity, etc. (as specified by the value of
DenomCondition
) of a field-simp-normal-form expression L
(a product of powers of atoms),
construct a corresponding proof for ((r, e), i) :: L
.
In this version we also expose the proof of nonzeroness of e
.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc disch hL_2 e r i = do let __do_lift ← disch q(«$e» ≠ 0) pure (__do_lift, ())
- Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc disch hL_2 e r i = do let pf ← disch q(«$e» ≠ 0) have pf₀ : have a := L.toNF; Q(«$a».eval ≠ 0) := hL_2 pure (pf, q(⋯))
Instances For
Given a proof of the nonzeroness, strict positivity, etc. (as specified by the value of
DenomCondition
) of a field-simp-normal-form expression L
(a product of powers of atoms),
construct a corresponding proof for ((r, e), i) :: L
.
Equations
- Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' disch hL_2 e r i = pure ()
- Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' disch hL_2 e r i = do let pf ← disch q(«$e» ≠ 0) have pf₀ : have a := L.toNF; Q(«$a».eval ≠ 0) := hL_2 pure q(⋯)
- Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' disch hL_2 e r i = do let pf ← disch q(0 < «$e») have pf₀ : have a := L.toNF; Q(0 < «$a».eval) := hL_2 pure q(⋯)
Instances For
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 variable cond
specifies whether we extract a certified nonzero[/positive] (and therefore
potentially smaller) common factor. If so, the metaprogram returns a "proof" that this common factor
is nonzero/positive, i.e. an expression Q(NF.eval $(L.toNF) ≠ 0)
/ Q(0 < NF.eval $(L.toNF))
.
Core of the field_simp
tactic #
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.
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.
Instances For
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.
Instances For
Given e₁
and e₂
, cancel positive factors to construct a new inequality which is logically
equivalent to e₁ ≤ e₂
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given e₁
and e₂
, cancel positive factors to construct a new inequality which is logically
equivalent to e₁ < e₂
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
.
Instances For
Given an (in)equality a = b
(respectively, a ≤ b
, a < b
), cancel nonzero (resp. positive)
factors to construct a new (in)equality which is logically equivalent to a = b
(respectively,
a ≤ b
, a < b
).
Instances For
Frontend #
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.
Instances For
The goal of field_simp
is to bring expressions in (semi-)fields over a common denominator, i.e. to
reduce them to expressions of the form n / d
where neither n
nor d
contains any division
symbol. For example, x / (1 - y) / (1 + y / (1 - y))
is reduced to x / (1 - y + y)
:
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
field_simp
-- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
The field_simp
tactic will also clear denominators in field (in)equalities, by
cross-multiplying. For example, field_simp
will clear the x
denominators in the following
equation:
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
field_simp
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
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/positivity 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/positive to enable
further progress.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The goal of the field_simp
conv tactic is to bring an expression in a (semi-)field over a common
denominator, i.e. to reduce it to an expression of the form n / d
where neither n
nor d
contains any division symbol. For example, x / (1 - y) / (1 + y / (1 - y))
is reduced to
x / (1 - y + y)
:
example (x y z : ℚ) (hy : 1 - y ≠ 0) :
⌊x / (1 - y) / (1 + y / (1 - y))⌋ < 3 := by
conv => enter [1, 1]; field_simp
-- new goal: `⊢ ⌊x / (1 - y + y)⌋ < 3`
As in this example, cancelling and combining denominators will generally require checking
"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.
The field_simp
conv tactic is a variant of the main (i.e., not conv) field_simp
tactic. The
latter operates recursively on subexpressions, bringing every field-expression encountered to the
form n / d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The goal of the simprocs grouped under the field
attribute is to clear denominators in
(semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then
cross-multiplying. For example, the field
simproc will clear the x
denominators in the following
equation:
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
simp only [field]
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
The field
simproc-set's functionality is a variant of the more general field_simp
tactic, which
not only clears denominators in field (in)equalities but also brings isolated field expressions into
the normal form n / d
(where neither n
nor d
contains any division symbol). (For confluence
reasons, the field
simprocs also have a slightly different normal form from field_simp
's.)
Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
side conditions. The field
simproc-set 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/positivity proofs included explicitly
in the simp call (e.g. simp [field, hx]
). If your (in)equality is not completely reduced by the
field
simproc-set, check the denominators of the resulting (in)equality and provide proofs that
they are nonzero/positive to enable further progress.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The goal of the simprocs grouped under the field
attribute is to clear denominators in
(semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then
cross-multiplying. For example, the field
simproc will clear the x
denominators in the following
equation:
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
simp only [field]
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
The field
simproc-set's functionality is a variant of the more general field_simp
tactic, which
not only clears denominators in field (in)equalities but also brings isolated field expressions into
the normal form n / d
(where neither n
nor d
contains any division symbol). (For confluence
reasons, the field
simprocs also have a slightly different normal form from field_simp
's.)
Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
side conditions. The field
simproc-set 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/positivity proofs included explicitly
in the simp call (e.g. simp [field, hx]
). If your (in)equality is not completely reduced by the
field
simproc-set, check the denominators of the resulting (in)equality and provide proofs that
they are nonzero/positive to enable further progress.
Equations
Instances For
The goal of the simprocs grouped under the field
attribute is to clear denominators in
(semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then
cross-multiplying. For example, the field
simproc will clear the x
denominators in the following
equation:
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
simp only [field]
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
The field
simproc-set's functionality is a variant of the more general field_simp
tactic, which
not only clears denominators in field (in)equalities but also brings isolated field expressions into
the normal form n / d
(where neither n
nor d
contains any division symbol). (For confluence
reasons, the field
simprocs also have a slightly different normal form from field_simp
's.)
Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
side conditions. The field
simproc-set 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/positivity proofs included explicitly
in the simp call (e.g. simp [field, hx]
). If your (in)equality is not completely reduced by the
field
simproc-set, check the denominators of the resulting (in)equality and provide proofs that
they are nonzero/positive to enable further progress.
Equations
Instances For
The goal of the simprocs grouped under the field
attribute is to clear denominators in
(semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then
cross-multiplying. For example, the field
simproc will clear the x
denominators in the following
equation:
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
simp only [field]
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
The field
simproc-set's functionality is a variant of the more general field_simp
tactic, which
not only clears denominators in field (in)equalities but also brings isolated field expressions into
the normal form n / d
(where neither n
nor d
contains any division symbol). (For confluence
reasons, the field
simprocs also have a slightly different normal form from field_simp
's.)
Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
side conditions. The field
simproc-set 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/positivity proofs included explicitly
in the simp call (e.g. simp [field, hx]
). If your (in)equality is not completely reduced by the
field
simproc-set, check the denominators of the resulting (in)equality and provide proofs that
they are nonzero/positive to enable further progress.
Equations
Instances For
We register field_simp
with the hint
tactic.