The abel tactic
Evaluate expressions in the language of additive, commutative monoids and groups.
Equations
- tactic.abel.term n x a = n •ℕ x + a
Equations
- tactic.abel.termg n x a = n •ℤ x + a
- zero : expr → tactic.abel.normal_expr
- nterm : expr → expr × ℤ → expr → tactic.abel.normal_expr → tactic.abel.normal_expr
@[instance]
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 : α) :
tactic.abel.term 0 x a = a
theorem
tactic.abel.zero_termg
{α : Type u_1}
[add_comm_group α]
(x a : α) :
tactic.abel.termg 0 x a = 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'
Equations
- tactic.abel.smul n x = n •ℕ x
Equations
- tactic.abel.smulg n x = n •ℤ x
theorem
tactic.abel.zero_smul
{α : Type u_1}
[add_comm_monoid α]
(c : ℕ) :
tactic.abel.smul c 0 = 0
theorem
tactic.abel.zero_smulg
{α : Type u_1}
[add_comm_group α]
(c : ℤ) :
tactic.abel.smulg c 0 = 0
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' : α) :
c * n = n' → tactic.abel.smulg c a = a' → tactic.abel.smulg c (tactic.abel.termg n x a) = tactic.abel.termg n' x a'
theorem
tactic.abel.term_atom
{α : Type u_1}
[add_comm_monoid α]
(x : α) :
x = tactic.abel.term 1 x 0
theorem
tactic.abel.term_atomg
{α : Type u_1}
[add_comm_group α]
(x : α) :
x = tactic.abel.termg 1 x 0
theorem
tactic.abel.unfold_smul
{α : Type u_1}
[add_comm_monoid α]
(n : ℕ)
(x y : α) :
tactic.abel.smul n x = y → n •ℕ x = y
theorem
tactic.abel.unfold_smulg
{α : Type u_1}
[add_comm_group α]
(n : ℕ)
(x y : α) :
tactic.abel.smulg (int.of_nat n) x = y → n •ℕ x = y
theorem
tactic.abel.unfold_gsmul
{α : Type u_1}
[add_comm_group α]
(n : ℤ)
(x y : α) :
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 : α) :
l = tl → r = tr → tactic.abel.smul tl tr = t → tactic.abel.smul l r = t
theorem
tactic.abel.subst_into_smulg
{α : Type u_1}
[add_comm_group α]
(l : ℤ)
(r : α)
(tl : ℤ)
(tr t : α) :
l = tl → r = tr → tactic.abel.smulg tl tr = t → tactic.abel.smulg l r = t
@[instance]
- raw : tactic.abel.normalize_mode
- term : tactic.abel.normalize_mode
@[instance]
Equations
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 }