Documentation

Mathlib.Tactic.FieldSimp

field_simp tactic #

Tactic to clear denominators in algebraic expressions.

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

@[reducible, inline]

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
Instances For
    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.
    Instances For
      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
      Instances For
        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
        Instances For
          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.
          Instances For
            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
            Instances For
              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
              Instances For
                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.
                Instances For
                  @[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
                  Instances For
                    @[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
                    Instances For
                      @[irreducible]
                      def Mathlib.Tactic.FieldSimp.qNF.div {v : Lean.Level} {M : Q(Type v)} :
                      qNF MqNF MqNF 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
                      Instances For
                        @[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
                        Instances For
                          inductive Mathlib.Tactic.FieldSimp.DenomCondition {v : Lean.Level} {M : Q(Type v)} (iM : Q(GroupWithZero «$M»)) :

                          Constraints on denominators which may need to be considered in field_simp: no condition, nonzeroness, or strict positivity.

                          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
                            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
                                def Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc {v : Lean.Level} {M : Q(Type v)} {iM : Q(CommGroupWithZero «$M»)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) {cond : DenomCondition q(inferInstance)} {L : qNF M} (hL : DenomCondition.proof L cond) (e : Q(«$M»)) (r : ) (i : ) :
                                Lean.MetaM (Q(«$e» 0) × DenomCondition.proof (((r, e), i) :: L) cond)

                                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
                                Instances For
                                  def Mathlib.Tactic.FieldSimp.mkDenomConditionProofSucc' {v : Lean.Level} {M : Q(Type v)} {iM : Q(CommGroupWithZero «$M»)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) {cond : DenomCondition q(inferInstance)} {L : qNF M} (hL : DenomCondition.proof L cond) (e : Q(«$M»)) (r : ) (i : ) :

                                  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
                                  Instances For
                                    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»)) (cond : DenomCondition q(inferInstance)) :
                                    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)) × DenomCondition.proof L cond)

                                    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 #

                                    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.
                                    Instances For
                                      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.
                                      Instances For
                                        def Mathlib.Tactic.FieldSimp.reduceLeQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (iM' : Q(PartialOrder «$M»)) (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLE «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)) (e₁ e₂ : Q(«$M»)) :
                                        AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» «$e₂») = («$f₁» «$f₂»)))

                                        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
                                          def Mathlib.Tactic.FieldSimp.reduceLtQ {v : Lean.Level} {M : Q(Type v)} (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (iM : Q(CommGroupWithZero «$M»)) (iM' : Q(PartialOrder «$M»)) (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLT «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»)) (e₁ e₂ : Q(«$M»)) :
                                          AtomM ((f₁ : Q(«$M»)) × (f₂ : Q(«$M»)) × Q((«$e₁» < «$e₂») = («$f₁» < «$f₂»)))

                                          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
                                            def Mathlib.Tactic.FieldSimp.reduceExpr (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (x : Lean.Expr) :

                                            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
                                              def Mathlib.Tactic.FieldSimp.reduceProp (disch : {u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) (t : Lean.Expr) :

                                              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 #

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