Documentation

Mathlib.Tactic.Abel

The abel tactic #

Evaluate expressions in the language of additive, commutative monoids and groups.

The Context for a call to abel.

Stores a few options for this call, and caches some common subexpressions such as typeclass instances and 0 : α.

Instances For

    Populate a context object for evaluating e.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline, reducible]

      The monad for Abel contains, in addition to the AtomM state, some information about the current type we are working over, so that we can consistently use group lemmas or monoid lemmas as appropriate.

      Equations
      Instances For

        Apply the function n : ∀ {α} [inst : AddWhatever α], _ to the implicit parameters in the context, and the given list of arguments.

        Equations
        Instances For

          Apply the function n : ∀ {α} [inst α], _ to the implicit parameters in the context, and the given list of arguments.

          Compared to context.app, this takes the name of the typeclass, rather than an inferred typeclass instance.

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

            Add the letter "g" to the end of the name, e.g. turning term into termg.

            This is used to choose between declarations taking AddCommMonoid and those taking AddCommGroup instances.

            Equations
            Instances For

              Apply the function n : ∀ {α} [AddComm{Monoid,Group} α] to the given list of arguments.

              Will use the AddComm{Monoid,Group} instance that has been cached in the context.

              Equations
              Instances For
                def Mathlib.Tactic.Abel.term {α : Type u_1} [AddCommMonoid α] (n : ) (x : α) (a : α) :
                α

                A type synonym used by abel to represent n • x + a in an additive commutative monoid.

                Equations
                Instances For
                  def Mathlib.Tactic.Abel.termg {α : Type u_1} [AddCommGroup α] (n : ) (x : α) (a : α) :
                  α

                  A type synonym used by abel to represent n • x + a in an additive commutative group.

                  Equations
                  Instances For

                    Evaluate a term with coefficient n, atom x and successor terms a.

                    Equations
                    Instances For

                      Interpret an integer as a coefficient to a term.

                      Equations
                      Instances For

                        A normal form for abel. Expressions are represented as a list of terms of the form e = n • x, where n : ℤ and x is an arbitrary element of the additive commutative monoid or group. We explicitly track the Expr forms of e and n, even though they could be reconstructed, for efficiency.

                        Instances For

                          Construct the normal form representing a single term.

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

                            Construct the normal form representing zero.

                            Equations
                            Instances For
                              theorem Mathlib.Tactic.Abel.const_add_term {α : Type u_1} [AddCommMonoid α] (k : α) (n : ) (x : α) (a : α) (a' : α) (h : k + a = a') :
                              theorem Mathlib.Tactic.Abel.const_add_termg {α : Type u_1} [AddCommGroup α] (k : α) (n : ) (x : α) (a : α) (a' : α) (h : k + a = a') :
                              theorem Mathlib.Tactic.Abel.term_add_const {α : Type u_1} [AddCommMonoid α] (n : ) (x : α) (a : α) (k : α) (a' : α) (h : a + k = a') :
                              theorem Mathlib.Tactic.Abel.term_add_constg {α : Type u_1} [AddCommGroup α] (n : ) (x : α) (a : α) (k : α) (a' : α) (h : a + k = a') :
                              theorem Mathlib.Tactic.Abel.term_add_term {α : Type u_1} [AddCommMonoid α] (n₁ : ) (x : α) (a₁ : α) (n₂ : ) (a₂ : α) (n' : ) (a' : α) (h₁ : n₁ + n₂ = n') (h₂ : a₁ + a₂ = a') :
                              theorem Mathlib.Tactic.Abel.term_add_termg {α : Type u_1} [AddCommGroup α] (n₁ : ) (x : α) (a₁ : α) (n₂ : ) (a₂ : α) (n' : ) (a' : α) (h₁ : n₁ + n₂ = n') (h₂ : a₁ + a₂ = a') :
                              theorem Mathlib.Tactic.Abel.zero_term {α : Type u_1} [AddCommMonoid α] (x : α) (a : α) :
                              theorem Mathlib.Tactic.Abel.zero_termg {α : Type u_1} [AddCommGroup α] (x : α) (a : α) :
                              theorem Mathlib.Tactic.Abel.term_neg {α : Type u_1} [AddCommGroup α] (n : ) (x : α) (a : α) (n' : ) (a' : α) (h₁ : -n = n') (h₂ : -a = a') :

                              Interpret a negated expression in abel's normal form.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Mathlib.Tactic.Abel.smul {α : Type u_1} [AddCommMonoid α] (n : ) (x : α) :
                                α

                                A synonym for , used internally in abel.

                                Equations
                                Instances For
                                  def Mathlib.Tactic.Abel.smulg {α : Type u_1} [AddCommGroup α] (n : ) (x : α) :
                                  α

                                  A synonym for , used internally in abel.

                                  Equations
                                  Instances For
                                    theorem Mathlib.Tactic.Abel.term_smul {α : Type u_1} [AddCommMonoid α] (c : ) (n : ) (x : α) (a : α) (n' : ) (a' : α) (h₁ : c * n = n') (h₂ : Mathlib.Tactic.Abel.smul c a = a') :
                                    theorem Mathlib.Tactic.Abel.term_smulg {α : Type u_1} [AddCommGroup α] (c : ) (n : ) (x : α) (a : α) (n' : ) (a' : α) (h₁ : c * n = n') (h₂ : Mathlib.Tactic.Abel.smulg c a = a') :

                                    Auxiliary function for evalSMul'.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Mathlib.Tactic.Abel.term_atom_pf {α : Type u_1} [AddCommMonoid α] (x : α) (x' : α) (h : x = x') :
                                      theorem Mathlib.Tactic.Abel.term_atom_pfg {α : Type u_1} [AddCommGroup α] (x : α) (x' : α) (h : x = x') :

                                      Interpret an expression as an atom for abel's normal form.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem Mathlib.Tactic.Abel.unfold_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (b : α) (c : α) (h : a + -b = c) :
                                        a - b = c
                                        theorem Mathlib.Tactic.Abel.unfold_smul {α : Type u_1} [AddCommMonoid α] (n : ) (x : α) (y : α) (h : Mathlib.Tactic.Abel.smul n x = y) :
                                        n x = y
                                        theorem Mathlib.Tactic.Abel.unfold_smulg {α : Type u_1} [AddCommGroup α] (n : ) (x : α) (y : α) (h : Mathlib.Tactic.Abel.smulg (Int.ofNat n) x = y) :
                                        n x = y
                                        theorem Mathlib.Tactic.Abel.unfold_zsmul {α : Type u_1} [AddCommGroup α] (n : ) (x : α) (y : α) (h : Mathlib.Tactic.Abel.smulg n x = y) :
                                        n x = y
                                        theorem Mathlib.Tactic.Abel.subst_into_smul {α : Type u_1} [AddCommMonoid α] (l : ) (r : α) (tl : ) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : Mathlib.Tactic.Abel.smul tl tr = t) :
                                        theorem Mathlib.Tactic.Abel.subst_into_smulg {α : Type u_1} [AddCommGroup α] (l : ) (r : α) (tl : ) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : Mathlib.Tactic.Abel.smulg tl tr = t) :
                                        theorem Mathlib.Tactic.Abel.subst_into_smul_upcast {α : Type u_1} [AddCommGroup α] (l : ) (r : α) (tl : ) (zl : ) (tr : α) (t : α) (prl₁ : l = tl) (prl₂ : tl = zl) (prr : r = tr) (prt : Mathlib.Tactic.Abel.smulg zl tr = t) :
                                        theorem Mathlib.Tactic.Abel.subst_into_add {α : Type u_1} [AddCommMonoid α] (l : α) (r : α) (tl : α) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) :
                                        l + r = t
                                        theorem Mathlib.Tactic.Abel.subst_into_addg {α : Type u_1} [AddCommGroup α] (l : α) (r : α) (tl : α) (tr : α) (t : α) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) :
                                        l + r = t
                                        theorem Mathlib.Tactic.Abel.subst_into_negg {α : Type u_1} [AddCommGroup α] (a : α) (ta : α) (t : α) (pra : a = ta) (prt : -ta = t) :
                                        -a = t

                                        Normalize a term orig of the form smul e₁ e₂ or smulg e₁ e₂. Normalized terms use smul for monoids and smulg for groups, so there are actually four cases to handle:

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

                                          Evaluate an expression into its abel normal form, by recursing into subexpressions.

                                          Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

                                          abel1! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

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

                                            Tactic for solving equations in the language of additive, commutative monoids and groups. This version of abel fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.

                                            abel1! will use a more aggressive reducibility setting to identify atoms. This can prove goals that abel cannot, but is more expensive.

                                            Equations
                                            Instances For
                                              theorem Mathlib.Tactic.Abel.term_eq {α : Type u_1} [AddCommMonoid α] (n : ) (x : α) (a : α) :
                                              theorem Mathlib.Tactic.Abel.termg_eq {α : Type u_1} [AddCommGroup α] (n : ) (x : α) (a : α) :

                                              A type synonym used by abel to represent n • x + a in an additive commutative group.

                                              True if this represents an atomic expression.

                                              Equations
                                              Instances For

                                                The normalization style for abel_nf.

                                                Instances For

                                                  Configuration for abel_nf.

                                                  Instances For

                                                    Function elaborating AbelNF.Config.

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

                                                      The core of abel_nf, which rewrites the expression e into abel normal form.

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

                                                        The recursive case of abelNF.

                                                        • root: true when the function is called directly from abelNFCore and false when called by evalAtom in recursive mode.
                                                        • parent: The input expression to simplify. In pre we make use of both parent and e to determine if we are at the top level in order to prevent a loop go -> eval -> evalAtom -> go which makes no progress.

                                                        Use abel_nf to rewrite the main goal.

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

                                                          Use abel_nf to rewrite hypothesis h.

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

                                                            Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel.

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

                                                              Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel!.

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

                                                                Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.

                                                                • abel_nf! will use a more aggressive reducibility setting to identify atoms.
                                                                • abel_nf (config := cfg) allows for additional configuration:
                                                                  • red: the reducibility setting (overridden by !)
                                                                  • recursive: if true, abel_nf will also recurse into atoms
                                                                • abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_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 abelian groups, which rewrites all group expressions into a normal form.

                                                                  • abel_nf! will use a more aggressive reducibility setting to identify atoms.
                                                                  • abel_nf (config := cfg) allows for additional configuration:
                                                                    • red: the reducibility setting (overridden by !)
                                                                    • recursive: if true, abel_nf will also recurse into atoms
                                                                  • abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_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 abelian groups, which rewrites all group expressions into a normal form.

                                                                    • abel_nf! will use a more aggressive reducibility setting to identify atoms.
                                                                    • abel_nf (config := cfg) allows for additional configuration:
                                                                      • red: the reducibility setting (overridden by !)
                                                                      • recursive: if true, abel_nf will also recurse into atoms
                                                                    • abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_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

                                                                      Elaborator for the abel_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 abelian groups, which rewrites all group expressions into a normal form.

                                                                        • abel_nf! will use a more aggressive reducibility setting to identify atoms.
                                                                        • abel_nf (config := cfg) allows for additional configuration:
                                                                          • red: the reducibility setting (overridden by !)
                                                                          • recursive: if true, abel_nf will also recurse into atoms
                                                                        • abel_nf works as both a tactic and a conv tactic. In tactic mode, abel_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 abelian groups.

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

                                                                          For example:

                                                                          example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
                                                                          example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
                                                                          
                                                                          Equations
                                                                          Instances For

                                                                            Tactic for evaluating expressions in abelian groups.

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

                                                                            For example:

                                                                            example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
                                                                            example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
                                                                            
                                                                            Equations
                                                                            Instances For

                                                                              The tactic abel evaluates expressions in abelian groups. This is the conv tactic version, which rewrites a target which is an abel equality to True.

                                                                              See also the abel tactic.

                                                                              Equations
                                                                              Instances For

                                                                                The tactic abel evaluates expressions in abelian groups. This is the conv tactic version, which rewrites a target which is an abel equality to True.

                                                                                See also the abel tactic.

                                                                                Equations
                                                                                Instances For