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 α
orAddCommMonoid α
expression.
Populate a context
object for evaluating e
.
Equations
- One or more equations did not get rendered due to their size.
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.
Apply the function n : ∀ {α} [inst : AddWhatever α], _
to the
implicit parameters in the context, and the given list of arguments.
Equations
- c.app n inst = Lean.mkAppN (((Lean.Expr.const n [c.univ]).app c.α).app inst)
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.
Equations
- c.mkApp n inst l = do let __do_lift ← Lean.Meta.synthInstance ((Lean.Expr.const inst [c.univ]).app c.α) pure (c.app n __do_lift l)
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.
Equations
- Mathlib.Tactic.Abel.addG (p.str s) = p.str (s ++ "g")
- Mathlib.Tactic.Abel.addG x = x
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.
Equations
- Mathlib.Tactic.Abel.iapp n xs = do let c ← read pure (c.app (if c.isGroup = true then Mathlib.Tactic.Abel.addG n else n) c.inst xs)
A type synonym used by abel
to represent n • x + a
in an additive commutative monoid.
Equations
- Mathlib.Tactic.Abel.term n x a = n • x + a
A type synonym used by abel
to represent n • x + a
in an additive commutative group.
Equations
- Mathlib.Tactic.Abel.termg n x a = n • x + a
Evaluate a term with coefficient n
, atom x
and successor terms a
.
Equations
- Mathlib.Tactic.Abel.mkTerm n x a = Mathlib.Tactic.Abel.iapp `Mathlib.Tactic.Abel.term #[n, x, a]
Interpret an integer as a coefficient to a term.
Equations
- Mathlib.Tactic.Abel.intToExpr n = do let __do_lift ← read liftM ((Lean.mkConst (if __do_lift.isGroup = true then `Int else `Nat)).ofInt n)
Equations
- Mathlib.Tactic.Abel.instInhabitedNormalExpr = { default := Mathlib.Tactic.Abel.NormalExpr.zero default }
Extract the expression from a normal form.
Equations
- (Mathlib.Tactic.Abel.NormalExpr.zero e).e = e
- (Mathlib.Tactic.Abel.NormalExpr.nterm e n x_1 a).e = e
Construct the normal form representing a single term.
Equations
- Mathlib.Tactic.Abel.NormalExpr.term' n x a = do let __do_lift ← Mathlib.Tactic.Abel.mkTerm n.1 x.2 a.e pure (Mathlib.Tactic.Abel.NormalExpr.nterm __do_lift n x a)
Construct the normal form representing zero.
Equations
- Mathlib.Tactic.Abel.NormalExpr.zero' = do let __do_lift ← read pure (Mathlib.Tactic.Abel.NormalExpr.zero __do_lift.α0)
Interpret the sum of two expressions in abel
's normal form.
Interpret a negated expression in abel
's normal form.
Equations
- One or more equations did not get rendered due to their size.
A synonym for •
, used internally in abel
.
Equations
- Mathlib.Tactic.Abel.smul n x = n • x
A synonym for •
, used internally in abel
.
Equations
- Mathlib.Tactic.Abel.smulg n x = n • x
Auxiliary function for evalSMul'
.
Equations
- One or more equations did not get rendered due to their size.
Interpret an expression as an atom for abel
's normal form.
Equations
- One or more equations did not get rendered due to their size.
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 usingsubst_into_smul
- Using
smulg
in a group just simplifies the pieces usingsubst_into_smulg
- Using
smul a b
in a group requires convertinga
from a nat to an int and then simplifyingsmulg ↑a b
usingsubst_into_smul_upcast
- Using
smulg
in a monoid is impossible (or at least out of scope), because you need a group argument to write asmulg
term
Equations
- One or more equations did not get rendered due to their size.
Evaluate an expression into its abel
normal form, by recursing into subexpressions.
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- Mathlib.Tactic.Abel.abel1! = Lean.ParserDescr.node `Mathlib.Tactic.Abel.abel1! 1024 (Lean.ParserDescr.nonReservedSymbol "abel1!" false)
A type synonym used by abel
to represent n • x + a
in an additive commutative group.
True if this represents an atomic expression.
Equations
- (Mathlib.Tactic.Abel.NormalExpr.nterm e (fst, 1) x_1 (Mathlib.Tactic.Abel.NormalExpr.zero e_1)).isAtom = true
- x.isAtom = false
The normalization style for abel_nf
.
- term: Mathlib.Tactic.Abel.AbelMode
The default form
- raw: Mathlib.Tactic.Abel.AbelMode
Raw form: the representation
abel
uses internally.
Configuration for abel_nf
.
the reducibility setting to use when comparing atoms for defeq
- recursive : Bool
if true, atoms inside ring expressions will be reduced recursively
- mode : Mathlib.Tactic.Abel.AbelMode
The normalization style.
Function elaborating AbelNF.Config
.
Equations
- One or more equations did not get rendered due to their size.
The core of abel_nf
, which rewrites the expression e
into abel
normal form.
s
: a reference to the mutable state ofabel
, for persisting across calls. This ensures that atom ordering is used consistently.cfg
: the configuration optionse
: the expression to rewrite
Equations
- One or more equations did not get rendered due to their size.
The recursive case of abelNF
.
root
: true when the function is called directly fromabelNFCore
and false when called byevalAtom
in recursive mode.parent
: The input expression to simplify. Inpre
we make use of bothparent
ande
to determine if we are at the top level in order to prevent a loopgo -> eval -> evalAtom -> go
which makes no progress.
The evalAtom
implementation passed to eval
calls go
if cfg.recursive
is true,
and does nothing otherwise.
Use abel_nf
to rewrite the main goal.
Equations
- One or more equations did not get rendered due to their size.
Use abel_nf
to rewrite hypothesis h
.
Equations
- One or more equations did not get rendered due to their size.
Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel
.
Equations
- One or more equations did not get rendered due to their size.
Unsupported legacy syntax from mathlib3, which allowed passing additional terms to abel!
.
Equations
- One or more equations did not get rendered due to their size.
Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.
abel_nf!
will use a more aggressive reducibility setting to identify atoms.abel_nf (config := cfg)
allows for additional configuration:abel_nf
works as both a tactic and a conv tactic. In tactic mode,abel_nf at h
can be used to rewrite in a hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.
abel_nf!
will use a more aggressive reducibility setting to identify atoms.abel_nf (config := cfg)
allows for additional configuration:abel_nf
works as both a tactic and a conv tactic. In tactic mode,abel_nf at h
can be used to rewrite in a hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.
abel_nf!
will use a more aggressive reducibility setting to identify atoms.abel_nf (config := cfg)
allows for additional configuration:abel_nf
works as both a tactic and a conv tactic. In tactic mode,abel_nf at h
can be used to rewrite in a hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Elaborator for the abel_nf
tactic.
Equations
- One or more equations did not get rendered due to their size.
Simplification tactic for expressions in the language of abelian groups, which rewrites all group expressions into a normal form.
abel_nf!
will use a more aggressive reducibility setting to identify atoms.abel_nf (config := cfg)
allows for additional configuration:abel_nf
works as both a tactic and a conv tactic. In tactic mode,abel_nf at h
can be used to rewrite in a hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Tactic for evaluating expressions in abelian groups.
abel!
will use a more aggressive reducibility setting to determine equality of atoms.abel1
fails if the target is not an equality.
For example:
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
Equations
- Mathlib.Tactic.Abel.abel = Lean.ParserDescr.node `Mathlib.Tactic.Abel.abel 1024 (Lean.ParserDescr.nonReservedSymbol "abel" false)
Tactic for evaluating expressions in abelian groups.
abel!
will use a more aggressive reducibility setting to determine equality of atoms.abel1
fails if the target is not an equality.
For example:
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
Equations
- Mathlib.Tactic.Abel.tacticAbel! = Lean.ParserDescr.node `Mathlib.Tactic.Abel.tacticAbel! 1024 (Lean.ParserDescr.nonReservedSymbol "abel!" false)
The tactic abel
evaluates expressions in abelian groups.
This is the conv tactic version, which rewrites a target which is an abel equality to True
.
See also the abel
tactic.
Equations
- Mathlib.Tactic.Abel.abelConv = Lean.ParserDescr.node `Mathlib.Tactic.Abel.abelConv 1024 (Lean.ParserDescr.nonReservedSymbol "abel" false)
The tactic abel
evaluates expressions in abelian groups.
This is the conv tactic version, which rewrites a target which is an abel equality to True
.
See also the abel
tactic.
Equations
- Mathlib.Tactic.Abel.convAbel! = Lean.ParserDescr.node `Mathlib.Tactic.Abel.convAbel! 1024 (Lean.ParserDescr.nonReservedSymbol "abel!" false)