mathlib documentation

tactic.abel

The abel tactic #

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

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

Populate a context object for evaluating e, up to reducibility level red.

meta def tactic.abel.context.app (c : tactic.abel.context) (n : name) (inst : expr) :

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

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.

meta def tactic.abel.add_g  :

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

This is used to choose between declarations taking add_comm_monoid and those taking add_comm_group instances.

Apply the function n : ∀ {α} [add_comm_{monoid,group} α] to the given list of arguments.

Will use the add_comm_{monoid,group} instance that has been cached in the context.

def tactic.abel.term {α : Type u_1} [add_comm_monoid α] (n : ) (x a : α) :
α
Equations
def tactic.abel.termg {α : Type u_1} [add_comm_group α] (n : ) (x a : α) :
α
Equations

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

Interpret an integer as a coefficient to a term.

theorem tactic.abel.const_add_term {α : Type u_1} [add_comm_monoid α] (k : α) (n : ) (x a a' : α) (h : k + a = a') :
theorem tactic.abel.const_add_termg {α : Type u_1} [add_comm_group α] (k : α) (n : ) (x a a' : α) (h : k + a = a') :
theorem tactic.abel.term_add_const {α : Type u_1} [add_comm_monoid α] (n : ) (x a k a' : α) (h : a + k = a') :
theorem tactic.abel.term_add_constg {α : Type u_1} [add_comm_group α] (n : ) (x a k a' : α) (h : a + k = a') :
theorem tactic.abel.term_add_term {α : Type u_1} [add_comm_monoid α] (n₁ : ) (x a₁ : α) (n₂ : ) (a₂ : α) (n' : ) (a' : α) (h₁ : n₁ + n₂ = n') (h₂ : 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' : α) (h₁ : n₁ + n₂ = n') (h₂ : 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' : α) (h₁ : -n = n') (h₂ : -a = a') :
def tactic.abel.smul {α : Type u_1} [add_comm_monoid α] (n : ) (x : α) :
α
Equations
def tactic.abel.smulg {α : Type u_1} [add_comm_group α] (n : ) (x : α) :
α
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' : α) (h₁ : c * n = n') (h₂ : tactic.abel.smul c a = a') :
theorem tactic.abel.term_smulg {α : Type u_1} [add_comm_group α] (c n : ) (x a : α) (n' : ) (a' : α) (h₁ : c * n = n') (h₂ : tactic.abel.smulg c a = 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} [subtraction_monoid α] (a b c : α) (h : a + -b = c) :
a - b = c
theorem tactic.abel.unfold_smul {α : Type u_1} [add_comm_monoid α] (n : ) (x y : α) (h : tactic.abel.smul n x = y) :
n x = y
theorem tactic.abel.unfold_smulg {α : Type u_1} [add_comm_group α] (n : ) (x y : α) (h : tactic.abel.smulg (int.of_nat n) x = y) :
n x = y
theorem tactic.abel.unfold_zsmul {α : Type u_1} [add_comm_group α] (n : ) (x y : α) (h : tactic.abel.smulg n x = y) :
n x = y
theorem tactic.abel.subst_into_smul {α : Type u_1} [add_comm_monoid α] (l : ) (r : α) (tl : ) (tr t : α) (prl : l = tl) (prr : r = tr) (prt : tactic.abel.smul tl tr = t) :
theorem tactic.abel.subst_into_smulg {α : Type u_1} [add_comm_group α] (l : ) (r : α) (tl : ) (tr t : α) (prl : l = tl) (prr : r = tr) (prt : tactic.abel.smulg tl tr = t) :
theorem tactic.abel.subst_into_smul_upcast {α : Type u_1} [add_comm_group α] (l : ) (r : α) (tl : ) (zl : ) (tr t : α) (prl₁ : l = tl) (prl₂ : tl = zl) (prr : r = tr) (prt : tactic.abel.smulg zl tr = 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:

  • 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
inductive tactic.abel.normalize_mode  :
Type
Instances for tactic.abel.normalize_mode

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.

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.

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

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 }
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - (id a + b) = 0 := by abel!

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.

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

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 }
example {α : Type*} {a b : α} [add_comm_group α] : (a + b) - (id a + b) = 0 := by abel!