mathlib documentation

tactic.abel

The abel tactic

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

meta structure tactic.abel.cache  :
Type

meta def tactic.abel.add_g  :

def tactic.abel.term {α : Type u_1} [add_comm_monoid α] :
α → α → α

Equations
def tactic.abel.termg {α : Type u_1} [add_comm_group α] :
α → α → α

Equations
theorem tactic.abel.const_add_term {α : Type u_1} [add_comm_monoid α] (k : α) (n : ) (x a a' : α) :
k + a = a'k + tactic.abel.term n x a = tactic.abel.term n x a'

theorem tactic.abel.const_add_termg {α : Type u_1} [add_comm_group α] (k : α) (n : ) (x a a' : α) :
k + a = a'k + tactic.abel.termg n x a = tactic.abel.termg n x a'

theorem tactic.abel.term_add_const {α : Type u_1} [add_comm_monoid α] (n : ) (x a k a' : α) :
a + k = a'tactic.abel.term n x a + k = tactic.abel.term n x a'

theorem tactic.abel.term_add_constg {α : Type u_1} [add_comm_group α] (n : ) (x a k a' : α) :
a + k = a'tactic.abel.termg n x a + k = tactic.abel.termg n x a'

theorem tactic.abel.term_add_term {α : Type u_1} [add_comm_monoid α] (n₁ : ) (x a₁ : α) (n₂ : ) (a₂ : α) (n' : ) (a' : α) :
n₁ + n₂ = n'a₁ + a₂ = a'tactic.abel.term n₁ x a₁ + tactic.abel.term n₂ x a₂ = tactic.abel.term n' x a'

theorem tactic.abel.term_add_termg {α : Type u_1} [add_comm_group α] (n₁ : ) (x a₁ : α) (n₂ : ) (a₂ : α) (n' : ) (a' : α) :
n₁ + n₂ = n'a₁ + a₂ = a'tactic.abel.termg n₁ x a₁ + tactic.abel.termg n₂ x a₂ = tactic.abel.termg n' x a'

theorem tactic.abel.zero_term {α : Type u_1} [add_comm_monoid α] (x a : α) :

theorem tactic.abel.zero_termg {α : Type u_1} [add_comm_group α] (x a : α) :

theorem tactic.abel.term_neg {α : Type u_1} [add_comm_group α] (n : ) (x a : α) (n' : ) (a' : α) :
-n = n'-a = a'-tactic.abel.termg n x a = tactic.abel.termg n' x a'

def tactic.abel.smul {α : Type u_1} [add_comm_monoid α] :
α → α

Equations
def tactic.abel.smulg {α : Type u_1} [add_comm_group α] :
α → α

Equations
theorem tactic.abel.zero_smul {α : Type u_1} [add_comm_monoid α] (c : ) :

theorem tactic.abel.zero_smulg {α : Type u_1} [add_comm_group α] (c : ) :

theorem tactic.abel.term_smul {α : Type u_1} [add_comm_monoid α] (c n : ) (x a : α) (n' : ) (a' : α) :
c * n = n'tactic.abel.smul c a = a'tactic.abel.smul c (tactic.abel.term n x a) = tactic.abel.term n' x a'

theorem tactic.abel.term_smulg {α : Type u_1} [add_comm_group α] (c n : ) (x a : α) (n' : ) (a' : α) :

theorem tactic.abel.term_atom {α : Type u_1} [add_comm_monoid α] (x : α) :

theorem tactic.abel.term_atomg {α : Type u_1} [add_comm_group α] (x : α) :

theorem tactic.abel.unfold_sub {α : Type u_1} [add_group α] (a b c : α) :
a + -b = ca - b = c

theorem tactic.abel.unfold_smul {α : Type u_1} [add_comm_monoid α] (n : ) (x y : α) :
tactic.abel.smul n x = yn •ℕ x = y

theorem tactic.abel.unfold_smulg {α : Type u_1} [add_comm_group α] (n : ) (x y : α) :

theorem tactic.abel.unfold_gsmul {α : Type u_1} [add_comm_group α] (n : ) (x y : α) :
tactic.abel.smulg n x = yn •ℤ x = y

theorem tactic.abel.subst_into_smul {α : Type u_1} [add_comm_monoid α] (l : ) (r : α) (tl : ) (tr t : α) :
l = tlr = trtactic.abel.smul tl tr = ttactic.abel.smul l r = t

theorem tactic.abel.subst_into_smulg {α : Type u_1} [add_comm_group α] (l : ) (r : α) (tl : ) (tr t : α) :
l = tlr = trtactic.abel.smulg tl tr = ttactic.abel.smulg l r = t

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.

Evaluate expressions in the language of additive, commutative monoids and groups. It attempts to prove the goal outright if there is no at specifier and the target is an equality, but if this fails, it falls back to rewriting all monoid expressions into a normal form. If there is an at specifier, it rewrites the given target into a normal form.

example {α : Type*} {a b : α} [add_comm_monoid α] : a + (b + a) = a + a + b := by abel
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - ((b + a) + a) = -a := by abel
example {α : Type*} {a b : α} [add_comm_group α] (hyp : a + a - a = b - b) : a = 0 :=
by { abel at hyp, exact hyp }