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 {u : Lean.Level} {arg : Q(Type u)} {sα : Q(CommSemiring «$arg»)} {a : Q(«$arg»)} :

True if this represents an atomic expression.

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

    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 {u : Lean.Level} {arg : Q(Type u)} {sα : Q(CommSemiring «$arg»)} {a : Q(«$arg»)} :

      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_2} [Ring R] (a : R) (b : R) :
                    a * -b = -(a * b)
                    theorem Mathlib.Tactic.RingNF.add_neg {R : Type u_2} [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_2} [Ring R] :
                    (Int.negOfNat n).rawCast = -n.rawCast
                    theorem Mathlib.Tactic.RingNF.rat_rawCast_pos {n : } {d : } {R : Type u_2} [DivisionRing R] :
                    Rat.rawCast (Int.ofNat n) d = n.rawCast / d.rawCast
                    theorem Mathlib.Tactic.RingNF.rat_rawCast_neg {n : } {d : } {R : Type u_2} [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.

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

                          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.

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

                            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.

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

                              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.

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

                                      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. If the goal is not appropriate for ring (e.g. not an equality) ring_nf will be suggested.

                                        • 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!
                                        example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf
                                        
                                        Equations
                                        Instances For

                                          Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent. If the goal is not appropriate for ring (e.g. not an equality) ring_nf will be suggested.

                                          • 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!
                                          example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf
                                          
                                          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