Documentation

Mathlib.Tactic.Ring.RingNF

ring_nf tactic #

A tactic which uses ring to rewrite expressions. This can be used non-terminally to normalize ring expressions in the goal such as ⊢ P (x + x + x) ~> ⊢ P (x * 3), as well as being able to prove some equations that ring cannot because they involve ring reasoning inside a subterm, such as sin (x + y) + sin (y + x) = 2 * sin (x + y).

def Mathlib.Tactic.Ring.ExBase.isAtom :
{a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase a_1Bool

True if this represents an atomic expression.

Equations
Instances For
    def Mathlib.Tactic.Ring.ExProd.isAtom :
    {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd a_1Bool

    True if this represents an atomic expression.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Mathlib.Tactic.Ring.ExSum.isAtom :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum a_1Bool

      True if this represents an atomic expression.

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

        The normalization style for ring_nf.

        Instances For

          Configuration for ring_nf.

          Instances For
            Equations

            Function elaborating RingNF.Config.

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

              The read-only state of the RingNF monad.

              Instances For
                @[reducible, inline]

                The monad for RingNF contains, in addition to the AtomM state, a simp context for the main traversal and a simp function (which has another simp context) to simplify normalized polynomials.

                Equations
                Instances For

                  A tactic in the RingNF.M monad which will simplify expression parent to a normal form.

                  • root: true if this is a direct call to the function. RingNF.M.run sets this to false in recursive mode.
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem Mathlib.Tactic.RingNF.add_assoc_rev {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) :
                    a + (b + c) = a + b + c
                    theorem Mathlib.Tactic.RingNF.mul_assoc_rev {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) :
                    a * (b * c) = a * b * c
                    theorem Mathlib.Tactic.RingNF.mul_neg {R : Type u_1} [Ring R] (a : R) (b : R) :
                    a * -b = -(a * b)
                    theorem Mathlib.Tactic.RingNF.add_neg {R : Type u_1} [Ring R] (a : R) (b : R) :
                    a + -b = a - b
                    theorem Mathlib.Tactic.RingNF.nat_rawCast_2 {R : Type u_1} [CommSemiring R] {n : } [n.AtLeastTwo] :
                    n.rawCast = OfNat.ofNat n
                    theorem Mathlib.Tactic.RingNF.int_rawCast_neg {n : } {R : Type u_1} [Ring R] :
                    (Int.negOfNat n).rawCast = -n.rawCast
                    theorem Mathlib.Tactic.RingNF.rat_rawCast_pos {n : } {d : } {R : Type u_1} [DivisionRing R] :
                    Rat.rawCast (Int.ofNat n) d = n.rawCast / d.rawCast
                    theorem Mathlib.Tactic.RingNF.rat_rawCast_neg {n : } {d : } {R : Type u_1} [DivisionRing R] :
                    Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

                    Runs a tactic in the RingNF.M monad, given initial data:

                    • s: a reference to the mutable state of ring, for persisting across calls. This ensures that atom ordering is used consistently.
                    • cfg: the configuration options
                    • x: the tactic to run
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Use ring_nf to rewrite the main goal.

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

                        Use ring_nf to rewrite hypothesis h.

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

                          Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

                          • ring_nf! will use a more aggressive reducibility setting to identify atoms.
                          • ring_nf (config := cfg) allows for additional configuration:
                            • red: the reducibility setting (overridden by !)
                            • recursive: if true, ring_nf will also recurse into atoms
                          • ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

                            • ring_nf! will use a more aggressive reducibility setting to identify atoms.
                            • ring_nf (config := cfg) allows for additional configuration:
                              • red: the reducibility setting (overridden by !)
                              • recursive: if true, ring_nf will also recurse into atoms
                            • ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

                              • ring_nf! will use a more aggressive reducibility setting to identify atoms.
                              • ring_nf (config := cfg) allows for additional configuration:
                                • red: the reducibility setting (overridden by !)
                                • recursive: if true, ring_nf will also recurse into atoms
                              • ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

                                • This version of ring1 uses ring_nf to simplify in atoms.
                                • The variant ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

                                  • This version of ring1 uses ring_nf to simplify in atoms.
                                  • The variant ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Elaborator for the ring_nf tactic.

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

                                      Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

                                      • ring_nf! will use a more aggressive reducibility setting to identify atoms.
                                      • ring_nf (config := cfg) allows for additional configuration:
                                        • red: the reducibility setting (overridden by !)
                                        • recursive: if true, ring_nf will also recurse into atoms
                                      • ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent.

                                        • ring! will use a more aggressive reducibility setting to determine equality of atoms.
                                        • ring1 fails if the target is not an equality.

                                        For example:

                                        example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
                                        example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
                                        example (x y : ℕ) : x + id y = y + id x := by ring!
                                        
                                        Equations
                                        Instances For

                                          Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent.

                                          • ring! will use a more aggressive reducibility setting to determine equality of atoms.
                                          • ring1 fails if the target is not an equality.

                                          For example:

                                          example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
                                          example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
                                          example (x y : ℕ) : x + id y = y + id x := by ring!
                                          
                                          Equations
                                          Instances For

                                            The tactic ring evaluates expressions in commutative (semi)rings. This is the conv tactic version, which rewrites a target which is a ring equality to True.

                                            See also the ring tactic.

                                            Equations
                                            Instances For

                                              The tactic ring evaluates expressions in commutative (semi)rings. This is the conv tactic version, which rewrites a target which is a ring equality to True.

                                              See also the ring tactic.

                                              Equations
                                              Instances For