The abel tactic

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

Future work

• In mathlib 3, abel accepted additional optional arguments:

  syntax "abel" (&" raw" <|> &" term")? (location)? : tactic
  

  It is undecided whether these features should be restored eventually.

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.

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.

def Mathlib.Tactic.Abel.smul {α : Type u_1} [AddCommMonoid α] (n : ℕ) (x : α) : α

A synonym for •, used internally in abel.

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

A synonym for •, used internally in abel.

def Mathlib.Tactic.Abel.abel : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

structure Mathlib.Tactic.Abel.Context : Type

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

• α : Lean.Expr

  The type of the ambient additive commutative group or monoid.

• univ : Lean.Level

  The universe level for α.

• α0 : Lean.Expr

  The expression representing 0 : α.

• isGroup : Bool

  Specify whether we are in an additive commutative group or an additive commutative monoid.

• inst : Lean.Expr

  The AddCommGroup α or AddCommMonoid α expression.

def Mathlib.Tactic.Abel.mkContext (e : Lean.Expr) : Lean.MetaM Context

Populate a context object for evaluating e.

@[reducible, inline]

abbrev Mathlib.Tactic.Abel.M (α : Type) : Type

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.

def Mathlib.Tactic.Abel.Context.app (c : Context) (n : Lean.Name) (inst : Lean.Expr) : Array Lean.Expr → Lean.Expr

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

def Mathlib.Tactic.Abel.Context.mkApp (c : Context) (n inst : Lean.Name) (l : Array Lean.Expr) : Lean.MetaM Lean.Expr

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.

def Mathlib.Tactic.Abel.addG : Lean.Name → Lean.Name

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.

def Mathlib.Tactic.Abel.iapp (n : Lean.Name) (xs : Array Lean.Expr) : M Lean.Expr

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.

def Mathlib.Tactic.Abel.mkTerm (n x a : Lean.Expr) : M Lean.Expr

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

def Mathlib.Tactic.Abel.intToExpr (n : ℤ) : M Lean.Expr

Interpret an integer as a coefficient to a term.

inductive Mathlib.Tactic.Abel.NormalExpr : Type

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.

• zero (e : Lean.Expr) : NormalExpr
• nterm (e : Lean.Expr) (n : Lean.Expr × ℤ) (x : ℕ × Lean.Expr) (a : NormalExpr) : NormalExpr

@[implicit_reducible]

instance Mathlib.Tactic.Abel.instInhabitedNormalExpr : Inhabited NormalExpr

def Mathlib.Tactic.Abel.instInhabitedNormalExpr.default : NormalExpr

def Mathlib.Tactic.Abel.NormalExpr.e : NormalExpr → Lean.Expr

Extract the expression from a normal form.

@[implicit_reducible]

instance Mathlib.Tactic.Abel.instCoeNormalExprExpr : Coe NormalExpr Lean.Expr

def Mathlib.Tactic.Abel.NormalExpr.term' (n : Lean.Expr × ℤ) (x : ℕ × Lean.Expr) (a : NormalExpr) : M NormalExpr

Construct the normal form representing a single term.

def Mathlib.Tactic.Abel.NormalExpr.zero' : M NormalExpr

Construct the normal form representing zero.

theorem Mathlib.Tactic.Abel.const_add_term {α : Type u_1} [AddCommMonoid α] (k : α) (n : ℕ) (x a a' : α) (h : k + a = a') : k + term n x a = term n x a'

theorem Mathlib.Tactic.Abel.const_add_termg {α : Type u_1} [AddCommGroup α] (k : α) (n : ℤ) (x a a' : α) (h : k + a = a') : k + termg n x a = termg n x a'

theorem Mathlib.Tactic.Abel.term_add_const {α : Type u_1} [AddCommMonoid α] (n : ℕ) (x a k a' : α) (h : a + k = a') : term n x a + k = term n x a'

theorem Mathlib.Tactic.Abel.term_add_constg {α : Type u_1} [AddCommGroup α] (n : ℤ) (x a k a' : α) (h : a + k = a') : termg n x a + k = termg n x 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') : term n₁ x a₁ + term n₂ x a₂ = term n' x 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') : termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'

theorem Mathlib.Tactic.Abel.zero_term {α : Type u_1} [AddCommMonoid α] (x a : α) : term 0 x a = a

theorem Mathlib.Tactic.Abel.zero_termg {α : Type u_1} [AddCommGroup α] (x a : α) : termg 0 x a = a

partial def Mathlib.Tactic.Abel.evalAdd : NormalExpr → NormalExpr → M (NormalExpr × Lean.Expr)

Interpret the sum of two expressions in abel's normal form.

theorem Mathlib.Tactic.Abel.term_neg {α : Type u_1} [AddCommGroup α] (n : ℤ) (x a : α) (n' : ℤ) (a' : α) (h₁ : -n = n') (h₂ : -a = a') : -termg n x a = termg n' x a'

def Mathlib.Tactic.Abel.evalNeg : NormalExpr → M (NormalExpr × Lean.Expr)

Interpret a negated expression in abel's normal form.

theorem Mathlib.Tactic.Abel.zero_smul {α : Type u_1} [AddCommMonoid α] (c : ℕ) : smul c 0 = 0

theorem Mathlib.Tactic.Abel.zero_smulg {α : Type u_1} [AddCommGroup α] (c : ℤ) : smulg c 0 = 0

theorem Mathlib.Tactic.Abel.term_smul {α : Type u_1} [AddCommMonoid α] (c n : ℕ) (x a : α) (n' : ℕ) (a' : α) (h₁ : c * n = n') (h₂ : smul c a = a') : smul c (term n x a) = term n' x a'

theorem Mathlib.Tactic.Abel.term_smulg {α : Type u_1} [AddCommGroup α] (c n : ℤ) (x a : α) (n' : ℤ) (a' : α) (h₁ : c * n = n') (h₂ : smulg c a = a') : smulg c (termg n x a) = termg n' x a'

def Mathlib.Tactic.Abel.evalSMul (k : Lean.Expr × ℤ) : NormalExpr → M (NormalExpr × Lean.Expr)

Auxiliary function for evalSMul'.

theorem Mathlib.Tactic.Abel.term_atom {α : Type u_1} [AddCommMonoid α] (x : α) : x = term 1 x 0

theorem Mathlib.Tactic.Abel.term_atomg {α : Type u_1} [AddCommGroup α] (x : α) : x = termg 1 x 0

theorem Mathlib.Tactic.Abel.term_atom_pf {α : Type u_1} [AddCommMonoid α] (x x' : α) (h : x = x') : x = term 1 x' 0

theorem Mathlib.Tactic.Abel.term_atom_pfg {α : Type u_1} [AddCommGroup α] (x x' : α) (h : x = x') : x = termg 1 x' 0

def Mathlib.Tactic.Abel.evalAtom (e : Lean.Expr) : M (NormalExpr × Lean.Expr)

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

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 : smul n x = y) : n • x = y

theorem Mathlib.Tactic.Abel.unfold_smulg {α : Type u_1} [AddCommGroup α] (n : ℕ) (x y : α) (h : smulg (Int.ofNat n) x = y) : ↑n • x = y

theorem Mathlib.Tactic.Abel.unfold_zsmul {α : Type u_1} [AddCommGroup α] (n : ℤ) (x y : α) (h : 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 : smul tl tr = t) : smul l r = t

theorem Mathlib.Tactic.Abel.subst_into_smulg {α : Type u_1} [AddCommGroup α] (l : ℤ) (r : α) (tl : ℤ) (tr t : α) (prl : l = tl) (prr : r = tr) (prt : smulg tl tr = t) : smulg l r = 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 : smulg zl tr = t) : smul l r = 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

def Mathlib.Tactic.Abel.evalSMul' (eval : Lean.Expr → M (NormalExpr × Lean.Expr)) (is_smulg : Bool) (orig e₁ e₂ : Lean.Expr) : M (NormalExpr × Lean.Expr)

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:

• Using smul in a monoid just simplifies the pieces using subst_into_smul
• Using smulg in a group just simplifies the pieces using subst_into_smulg
• Using smul a b in a group requires converting a from a nat to an int and then simplifying smulg ↑a b using subst_into_smul_upcast
• Using smulg in a monoid is impossible (or at least out of scope), because you need a group argument to write a smulg term

partial def Mathlib.Tactic.Abel.eval (e : Lean.Expr) : M (NormalExpr × Lean.Expr)

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

def Mathlib.Tactic.Abel.isAtom (e : Lean.Expr) : Bool

Determine whether e will be handled as an atom by the abel tactic. The match in this function should be preserved to be parallel in case-matching to that in the Mathlib.Tactic.Abel.eval metaprogram.

def Mathlib.Tactic.Abel.abel1 : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.abel1! : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

theorem Mathlib.Tactic.Abel.term_eq {α : Type u_1} [AddCommMonoid α] (n : ℕ) (x a : α) : term n x a = n • x + a

theorem Mathlib.Tactic.Abel.termg_eq {α : Type u_1} [AddCommGroup α] (n : ℤ) (x a : α) : termg n x a = n • x + a

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

def Mathlib.Tactic.Abel.NormalExpr.isAtom : NormalExpr → Bool

True if this represents an atomic expression.

inductive Mathlib.Tactic.Abel.AbelMode : Type

The normalization style for abel_nf.

• term : AbelMode

  The default form

• raw : AbelMode

  Raw form: the representation abel uses internally.

structure Mathlib.Tactic.Abel.AbelNF.Configextends Mathlib.Tactic.AtomM.Recurse.Config : Type

Configuration for abel_nf.

• red : Lean.Meta.TransparencyMode
• zetaDelta : Bool
• contextual : Bool
• mode : AbelMode

  The normalization style.

def Mathlib.Tactic.Abel.elabAbelNFConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM AbelNF.Config

Function elaborating AbelNF.Config.

def Mathlib.Tactic.Abel.cleanup (cfg : AbelNF.Config) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

A cleanup routine, which simplifies expressions in abel normal form to a more human-friendly format.

def Mathlib.Tactic.Abel.evalExpr (e : Lean.Expr) : AtomM Lean.Meta.Simp.Result

Evaluate an expression into its abel normal form.

This is a variant of Mathlib.Tactic.Abel.eval, the main driver of the abel tactic. It differs in

• outputting a Simp.Result, rather than a NormalExpr × Expr;
• throwing an error if the expression e is an atom for the abel tactic.

def Mathlib.Tactic.Abel.abelNF : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.tacticAbel_nf!__ : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.abelNFConv : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.elabAbelNFConv : Lean.Elab.Tactic.Tactic

Elaborator for the abel_nf tactic.

def Mathlib.Tactic.Abel.convAbel_nf!_ : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.tacticAbel! : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.abelConv : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

def Mathlib.Tactic.Abel.convAbel! : Lean.ParserDescr

abel solves equations in the language of additive, commutative monoids and groups.

abel and its variants work as both tactics and conv tactics.

• abel1 fails if the target is not an equality that is provable by the axioms of commutative monoids/groups.
• abel_nf rewrites all group expressions into a normal form.
  • abel_nf at h rewrites in a hypothesis.
  • abel_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, abel_nf also recurses into atoms.
• abel!, abel1!, abel_nf! use a more aggressive reducibility setting to identify atoms.

Examples:

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

We register abel with the hint tactic.