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)} { : Q(CommSemiring «$arg»)} {a : Q(«$arg»)} :
ExBase aBool

True if this represents an atomic expression.

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

      True if this represents an atomic expression.

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

          True if this represents an atomic expression.

          Equations
            Instances For

              The normalization style for ring_nf.

              • SOP : RingMode

                Sum-of-products form, like x + x * y * 2 + z ^ 2.

              • raw : RingMode

                Raw form: the representation ring uses internally.

              Instances For

                Configuration for ring_nf.

                • the reducibility setting to use when comparing atoms for defeq

                • zetaDelta : Bool

                  if true, local let variables can be unfolded

                • recursive : Bool

                  if true, atoms inside ring expressions will be reduced recursively

                • failIfUnchanged : Bool

                  if true, then fail if no progress is made

                • mode : RingMode

                  The normalization style.

                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
                          Instances For
                            theorem Mathlib.Tactic.RingNF.add_assoc_rev {R : Type u_1} [CommSemiring R] (a b c : R) :
                            a + (b + c) = a + b + c
                            theorem Mathlib.Tactic.RingNF.mul_assoc_rev {R : Type u_1} [CommSemiring R] (a b c : R) :
                            a * (b * c) = a * b * c
                            theorem Mathlib.Tactic.RingNF.mul_neg {R : Type u_2} [Ring R] (a b : R) :
                            a * -b = -(a * b)
                            theorem Mathlib.Tactic.RingNF.add_neg {R : Type u_2} [Ring R] (a b : R) :
                            a + -b = a - b
                            def Mathlib.Tactic.RingNF.M.run {α : Type} (s : IO.Ref AtomM.State) (cfg : Config) (x : M α) :

                            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
                              Instances For

                                The recursive context.

                                The atom evaluator calls either RingNF.rewrite recursively, or nothing depending on cfg.recursive.

                                Use ring_nf to rewrite the main goal.

                                Equations
                                  Instances For

                                    Use ring_nf to rewrite hypothesis h.

                                    Equations
                                      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 !)
                                          • zetaDelta: if true, local let variables can be unfolded (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
                                          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 !)
                                              • zetaDelta: if true, local let variables can be unfolded (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
                                              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 !)
                                                  • zetaDelta: if true, local let variables can be unfolded (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
                                                  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
                                                      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
                                                          Instances For

                                                            Elaborator for the ring_nf tactic.

                                                            Equations
                                                              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 !)
                                                                  • zetaDelta: if true, local let variables can be unfolded (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
                                                                  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