mathlib documentation

tactic.abel

The abel tactic #

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

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

source
meta def tactic.abel.mk_context (red : tactic.transparency) (e : expr) :
tactic tactic.abel.context

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

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

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

source
meta def tactic.abel.context.mk_app (c : tactic.abel.context) (n inst : name) (l : list expr) :
tactic 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.

source
meta def tactic.abel.add_g  :
name → 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 add_comm_monoid and those taking add_comm_group instances.

source
meta def tactic.abel.context.iapp (c : tactic.abel.context) (n : name) :
list expr → expr

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.

source
def tactic.abel.term {α : Type u_1} [add_comm_monoid α] (n : ℕ) (x a : α) :
α
Equations
source
def tactic.abel.termg {α : Type u_1} [add_comm_group α] (n : ℤ) (x a : α) :
α
Equations
source
meta def tactic.abel.context.mk_term (c : tactic.abel.context) (n x a : expr) :
expr

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

source
meta def tactic.abel.context.int_to_expr (c : tactic.abel.context) (n : ℤ) :
tactic expr

Interpret an integer as a coefficient to a term.

source
meta inductive tactic.abel.normal_expr  :
Type
source
meta def tactic.abel.normal_expr.e  :
tactic.abel.normal_expr → expr
source
@[protected, instance]
meta def tactic.abel.expr.has_coe  :
has_coe tactic.abel.normal_expr expr
source
@[protected, instance]
meta def tactic.abel.normal_expr.has_coe_to_fun  :
has_coe_to_fun tactic.abel.normal_expr (λ (_x : tactic.abel.normal_expr), expr → expr)
source
meta def tactic.abel.normal_expr.term' (c : tactic.abel.context) (n : expr × ℤ) (x : expr) (a : tactic.abel.normal_expr) :
tactic.abel.normal_expr
source
meta def tactic.abel.normal_expr.zero' (c : tactic.abel.context) :
tactic.abel.normal_expr
source
meta def tactic.abel.normal_expr.to_list  :
tactic.abel.normal_expr → list (ℤ × expr)
source
meta def tactic.abel.normal_expr.to_string (e : tactic.abel.normal_expr) :
string
source
meta def tactic.abel.normal_expr.pp (e : tactic.abel.normal_expr) :
tactic format
source
@[protected, instance]
meta def tactic.abel.normal_expr.has_to_tactic_format  :
has_to_tactic_format tactic.abel.normal_expr
source
meta def tactic.abel.normal_expr.refl_conv (e : tactic.abel.normal_expr) :
tactic (tactic.abel.normal_expr × expr)
source
theorem tactic.abel.const_add_term {α : Type u_1} [add_comm_monoid α] (k : α) (n : ℕ) (x a a' : α) (h : k + a = a') :
k + tactic.abel.term n x a = tactic.abel.term n x a'
source
theorem tactic.abel.const_add_termg {α : Type u_1} [add_comm_group α] (k : α) (n : ℤ) (x a a' : α) (h : k + a = a') :
k + tactic.abel.termg n x a = tactic.abel.termg n x a'
source
theorem tactic.abel.term_add_const {α : Type u_1} [add_comm_monoid α] (n : ℕ) (x a k a' : α) (h : a + k = a') :
tactic.abel.term n x a + k = tactic.abel.term n x a'
source
theorem tactic.abel.term_add_constg {α : Type u_1} [add_comm_group α] (n : ℤ) (x a k a' : α) (h : a + k = a') :
tactic.abel.termg n x a + k = tactic.abel.termg n x a'
source
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'
source
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'
source
theorem tactic.abel.zero_term {α : Type u_1} [add_comm_monoid α] (x a : α) :
tactic.abel.term 0 x a = a
source
theorem tactic.abel.zero_termg {α : Type u_1} [add_comm_group α] (x a : α) :
tactic.abel.termg 0 x a = a
source
meta def tactic.abel.eval_add (c : tactic.abel.context) :
tactic.abel.normal_expr → tactic.abel.normal_expr → tactic (tactic.abel.normal_expr × expr)
source
theorem tactic.abel.term_neg {α : Type u_1} [add_comm_group α] (n : ℤ) (x a : α) (n' : ℤ) (a' : α) (h₁ : -n = n') (h₂ : -a = a') :
-tactic.abel.termg n x a = tactic.abel.termg n' x a'
source
meta def tactic.abel.eval_neg (c : tactic.abel.context) :
tactic.abel.normal_expr → tactic (tactic.abel.normal_expr × expr)
source
def tactic.abel.smul {α : Type u_1} [add_comm_monoid α] (n : ℕ) (x : α) :
α
Equations
source
def tactic.abel.smulg {α : Type u_1} [add_comm_group α] (n : ℤ) (x : α) :
α
Equations
source
theorem tactic.abel.zero_smul {α : Type u_1} [add_comm_monoid α] (c : ℕ) :
tactic.abel.smul c 0 = 0
source
theorem tactic.abel.zero_smulg {α : Type u_1} [add_comm_group α] (c : ℤ) :
tactic.abel.smulg c 0 = 0
source
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') :
tactic.abel.smul c (tactic.abel.term n x a) = tactic.abel.term n' x a'
source
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') :
tactic.abel.smulg c (tactic.abel.termg n x a) = tactic.abel.termg n' x a'
source
meta def tactic.abel.eval_smul (c : tactic.abel.context) (k : expr × ℤ) :
tactic.abel.normal_expr → tactic (tactic.abel.normal_expr × expr)
source
theorem tactic.abel.term_atom {α : Type u_1} [add_comm_monoid α] (x : α) :
x = tactic.abel.term 1 x 0
source
theorem tactic.abel.term_atomg {α : Type u_1} [add_comm_group α] (x : α) :
x = tactic.abel.termg 1 x 0
source
meta def tactic.abel.eval_atom (c : tactic.abel.context) (e : expr) :
tactic (tactic.abel.normal_expr × expr)
source
theorem tactic.abel.unfold_sub {α : Type u_1} [add_group α] (a b c : α) (h : a + -b = c) :
a - b = c
source
theorem tactic.abel.unfold_smul {α : Type u_1} [add_comm_monoid α] (n : ℕ) (x y : α) (h : tactic.abel.smul n x = y) :
n • x = y
source
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
source
theorem tactic.abel.unfold_zsmul {α : Type u_1} [add_comm_group α] (n : ℤ) (x y : α) (h : tactic.abel.smulg n x = y) :
n • x = y
source
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) :
tactic.abel.smul l r = t
source
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) :
tactic.abel.smulg l r = t
source
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) :
tactic.abel.smul l r = t
source
meta def tactic.abel.eval_smul' (c : tactic.abel.context) (eval : expr → tactic (tactic.abel.normal_expr × expr)) (is_smulg : bool) (e₁ e₂ : expr) :
tactic (tactic.abel.normal_expr × expr)

Normalize a term 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
source
meta def tactic.abel.eval (c : tactic.abel.context) :
expr → tactic (tactic.abel.normal_expr × expr)
source
meta def tactic.abel.eval' (c : tactic.abel.context) (e : expr) :
tactic (expr × expr)
source
inductive tactic.abel.normalize_mode  :
Type
source
@[protected, instance]
meta def tactic.abel.normalize_mode.has_reflect  :
has_reflect tactic.abel.normalize_mode
source
@[protected, instance]
def tactic.abel.normalize_mode.inhabited  :
inhabited tactic.abel.normalize_mode
Equations
source
meta def tactic.abel.normalize (red : tactic.transparency) (mode : tactic.abel.normalize_mode := tactic.abel.normalize_mode.term) (e : expr) :
tactic (expr × expr)
source
meta def tactic.interactive.abel1 (red : interactive.parse (lean.parser.tk "!")?) :
tactic unit

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.

source
meta def tactic.interactive.abel.mode  :
lean.parser tactic.abel.normalize_mode
source
meta def tactic.interactive.abel (red : interactive.parse (lean.parser.tk "!")?) (SOP : interactive.parse tactic.interactive.abel.mode) (loc : interactive.parse interactive.types.location) :
tactic unit

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!