mathlib3 documentation

tactic.ring

`ring` #

Evaluate expressions in the language of commutative (semi)rings. Based on http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf .

def tactic.ring.horner {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b : α) :

α

The normal form that ring uses is mediated by the function horner a x n b := a * x ^ n + b. The reason we use a definition rather than the (more readable) expression on the right is because this expression contains a number of typeclass arguments in different positions, while horner contains only one comm_semiring instance at the top level. See also horner_expr for a description of normal form.

Equations

tactic.ring.horner a x n b = a * x ^ n + b

meta structure tactic.ring.cache :

This cache contains data required by the ring tactic during execution.

@[protected, instance]

meta def tactic.ring.ring_m.alternative :

alternative tactic.ring.ring_m

meta def tactic.ring.ring_m (α : Type) :

The monad that ring works in. This is a reader monad containing a mutable cache (using ref for mutability), as well as the list of atoms-up-to-defeq encountered thus far, used for atom sorting.

Instances for tactic.ring.ring_m

@[protected, instance]

meta def tactic.ring.ring_m.monad :

monad tactic.ring.ring_m

meta def tactic.ring.get_cache :

tactic.ring.ring_m tactic.ring.cache

Get the ring data from the monad.

meta def tactic.ring.get_atom (n : ℕ) :

tactic.ring.ring_m expr

Get an already encountered atom by its index.

meta def tactic.ring.add_atom (e : expr) :

tactic.ring.ring_m ℕ

Get the index corresponding to an atomic expression, if it has already been encountered, or put it in the list of atoms and return the new index, otherwise.

meta def tactic.ring.lift {α : Type} (m : tactic α) :

tactic.ring.ring_m α

Lift a tactic into the ring_m monad.

meta def tactic.ring.ring_m.run' (red : tactic.transparency) (atoms : tactic.ref (buffer expr)) (e : expr) {α : Type} (m : tactic.ring.ring_m α) :

Run a ring_m tactic in the tactic monad. This version of ring_m.run uses an external atoms ref, so that subexpressions can be named across multiple ring_m calls.

meta def tactic.ring.ring_m.run (red : tactic.transparency) (e : expr) {α : Type} (m : tactic.ring.ring_m α) :

Run a ring_m tactic in the tactic monad.

meta def tactic.ring.ic_lift' (icf : tactic.ring.cache → tactic.ref tactic.instance_cache) {α : Type} (f : tactic.instance_cache → tactic (tactic.instance_cache × α)) :

tactic.ring.ring_m α

Lift an instance cache tactic (probably from norm_num) to the ring_m monad. This version is abstract over the instance cache in question (either the ring α, or ℕ for exponents).

meta def tactic.ring.ic_lift {α : Type} :

(tactic.instance_cache → tactic (tactic.instance_cache × α)) → tactic.ring.ring_m α

Lift an instance cache tactic (probably from norm_num) to the ring_m monad. This uses the instance cache corresponding to the ring α.

meta def tactic.ring.nc_lift {α : Type} :

(tactic.instance_cache → tactic (tactic.instance_cache × α)) → tactic.ring.ring_m α

Lift an instance cache tactic (probably from norm_num) to the ring_m monad. This uses the instance cache corresponding to ℕ, which is used for computations in the exponent.

meta def tactic.ring.cache.cs_app (c : tactic.ring.cache) (n : name) :

list expr → expr

Apply a theorem that expects a comm_semiring instance. This is a special case of ic_lift mk_app, but it comes up often because horner and all its theorems have this assumption; it also does not require the tactic monad which improves access speed a bit.

meta inductive tactic.ring.horner_expr :

Every expression in the language of commutative semirings can be viewed as a sum of monomials, where each monomial is a product of powers of atoms. We fix a global order on atoms (up to definitional equality), and then separate the terms according to their smallest atom. So the top level expression is a * x^n + b where x is the smallest atom and n > 0 is a numeral, and n is maximal (so a contains at least one monomial not containing an x), and b contains no monomials with an x (hence all atoms in b are larger than x).

If there is no x satisfying these constraints, then the expression must be a numeral. Even though we are working over rings, we allow rational constants when these can be interpreted in the ring, so we can solve problems like x / 3 = 1 / 3 * x even though these are not technically in the language of rings.

These constraints ensure that there is a unique normal form for each ring expression, and so the algorithm is simply to calculate the normal form of each side and compare for equality.

To allow us to efficiently pattern match on normal forms, we maintain this inductive type that holds a normalized expression together with its structure. All the exprs in this type could be removed without loss of information, and conversely the horner_expr structure and the ℕ and ℚ values can be recovered from the top level expr, but we keep both in order to keep proof producing normalization functions efficient.

Instances for tactic.ring.horner_expr

meta def tactic.ring.horner_expr.e :

tactic.ring.horner_expr → expr

Get the expression corresponding to a horner_expr. This can be calculated recursively from the structure, but we cache the exprs in all subterms so that this function can be computed in constant time.

meta def tactic.ring.horner_expr.is_zero :

tactic.ring.horner_expr → bool

Is this expr the constant 0?

@[protected, instance]

meta def tactic.ring.expr.has_coe :

has_coe tactic.ring.horner_expr expr

@[protected, instance]

meta def tactic.ring.horner_expr.has_coe_to_fun :

has_coe_to_fun tactic.ring.horner_expr (λ (_x : tactic.ring.horner_expr), expr → expr)

meta def tactic.ring.horner_expr.xadd' (c : tactic.ring.cache) (a : tactic.ring.horner_expr) (x n : expr × ℕ) (b : tactic.ring.horner_expr) :

tactic.ring.horner_expr

Construct a xadd node, generating the cached expr using the input cache.

meta def tactic.ring.horner_expr.to_string :

tactic.ring.horner_expr → string

Pretty printer for horner_expr.

meta def tactic.ring.horner_expr.pp :

tactic.ring.horner_expr → tactic format

Pretty printer for horner_expr.

@[protected, instance]

meta def tactic.ring.horner_expr.has_to_tactic_format :

has_to_tactic_format tactic.ring.horner_expr

meta def tactic.ring.horner_expr.refl_conv (e : tactic.ring.horner_expr) :

tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Reflexivity conversion for a horner_expr.

theorem tactic.ring.zero_horner {α : Type u_1} [comm_semiring α] (x : α) (n : ℕ) (b : α) :

tactic.ring.horner 0 x n b = b

theorem tactic.ring.horner_horner {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ n₂ : ℕ) (b : α) (n' : ℕ) (h : n₁ + n₂ = n') :

tactic.ring.horner (tactic.ring.horner a₁ x n₁ 0) x n₂ b = tactic.ring.horner a₁ x n' b

meta def tactic.ring.eval_horner :

tactic.ring.horner_expr → expr × ℕ → expr × ℕ → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate horner a n x b where a and b are already in normal form.

theorem tactic.ring.const_add_horner {α : Type u_1} [comm_semiring α] (k a x : α) (n : ℕ) (b b' : α) (h : k + b = b') :

k + tactic.ring.horner a x n b = tactic.ring.horner a x n b'

theorem tactic.ring.horner_add_const {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b k b' : α) (h : b + k = b') :

tactic.ring.horner a x n b + k = tactic.ring.horner a x n b'

theorem tactic.ring.horner_add_horner_lt {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (b₂ : α) (k : ℕ) (a' b' : α) (h₁ : n₁ + k = n₂) (h₂ : a₁ + tactic.ring.horner a₂ x k 0 = a') (h₃ : b₁ + b₂ = b') :

tactic.ring.horner a₁ x n₁ b₁ + tactic.ring.horner a₂ x n₂ b₂ = tactic.ring.horner a' x n₁ b'

theorem tactic.ring.horner_add_horner_gt {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (b₂ : α) (k : ℕ) (a' b' : α) (h₁ : n₂ + k = n₁) (h₂ : tactic.ring.horner a₁ x k 0 + a₂ = a') (h₃ : b₁ + b₂ = b') :

tactic.ring.horner a₁ x n₁ b₁ + tactic.ring.horner a₂ x n₂ b₂ = tactic.ring.horner a' x n₂ b'

theorem tactic.ring.horner_add_horner_eq {α : Type u_1} [comm_semiring α] (a₁ x : α) (n : ℕ) (b₁ a₂ b₂ a' b' t : α) (h₁ : a₁ + a₂ = a') (h₂ : b₁ + b₂ = b') (h₃ : tactic.ring.horner a' x n b' = t) :

tactic.ring.horner a₁ x n b₁ + tactic.ring.horner a₂ x n b₂ = t

meta def tactic.ring.eval_add :

tactic.ring.horner_expr → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a + b where a and b are already in normal form.

theorem tactic.ring.horner_neg {α : Type u_1} [comm_ring α] (a x : α) (n : ℕ) (b a' b' : α) (h₁ : -a = a') (h₂ : -b = b') :

-tactic.ring.horner a x n b = tactic.ring.horner a' x n b'

meta def tactic.ring.eval_neg :

tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate -a where a is already in normal form.

theorem tactic.ring.horner_const_mul {α : Type u_1} [comm_semiring α] (c a x : α) (n : ℕ) (b a' b' : α) (h₁ : c * a = a') (h₂ : c * b = b') :

c * tactic.ring.horner a x n b = tactic.ring.horner a' x n b'

theorem tactic.ring.horner_mul_const {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b c a' b' : α) (h₁ : a * c = a') (h₂ : b * c = b') :

tactic.ring.horner a x n b * c = tactic.ring.horner a' x n b'

meta def tactic.ring.eval_const_mul (k : expr × ℚ) :

tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate k * a where k is a rational numeral and a is in normal form.

theorem tactic.ring.horner_mul_horner_zero {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (aa t : α) (h₁ : tactic.ring.horner a₁ x n₁ b₁ * a₂ = aa) (h₂ : tactic.ring.horner aa x n₂ 0 = t) :

tactic.ring.horner a₁ x n₁ b₁ * tactic.ring.horner a₂ x n₂ 0 = t

theorem tactic.ring.horner_mul_horner {α : Type u_1} [comm_semiring α] (a₁ x : α) (n₁ : ℕ) (b₁ a₂ : α) (n₂ : ℕ) (b₂ aa haa ab bb t : α) (h₁ : tactic.ring.horner a₁ x n₁ b₁ * a₂ = aa) (h₂ : tactic.ring.horner aa x n₂ 0 = haa) (h₃ : a₁ * b₂ = ab) (h₄ : b₁ * b₂ = bb) (H : haa + tactic.ring.horner ab x n₁ bb = t) :

tactic.ring.horner a₁ x n₁ b₁ * tactic.ring.horner a₂ x n₂ b₂ = t

meta def tactic.ring.eval_mul :

tactic.ring.horner_expr → tactic.ring.horner_expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a * b where a and b are in normal form.

theorem tactic.ring.horner_pow {α : Type u_1} [comm_semiring α] (a x : α) (n m n' : ℕ) (a' : α) (h₁ : n * m = n') (h₂ : a ^ m = a') :

tactic.ring.horner a x n 0 ^ m = tactic.ring.horner a' x n' 0

theorem tactic.ring.pow_succ {α : Type u_1} [comm_semiring α] (a : α) (n : ℕ) (b c : α) (h₁ : a ^ n = b) (h₂ : b * a = c) :

a ^ (n + 1) = c

meta def tactic.ring.eval_pow :

tactic.ring.horner_expr → expr × ℕ → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a ^ n where a is in normal form and n is a natural numeral.

theorem tactic.ring.horner_atom {α : Type u_1} [comm_semiring α] (x : α) :

x = tactic.ring.horner 1 x 1 0

meta def tactic.ring.eval_atom (e : expr) :

tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a where a is an atom.

meta def tactic.ring.eval_norm_atom (norm_atom : expr → tactic (expr × expr)) (e : expr) :

tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a where a is an atom.

theorem tactic.ring.subst_into_pow {α : Type u_1} [monoid α] (l : α) (r : ℕ) (tl : α) (tr : ℕ) (t : α) (prl : l = tl) (prr : r = tr) (prt : tl ^ tr = t) :

l ^ r = t

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

a - b = c

theorem tactic.ring.unfold_div {α : Type u_1} [division_ring α] (a b c : α) (h : a * b⁻¹ = c) :

a / b = c

meta def tactic.ring.eval (norm_atom : expr → tactic (expr × expr)) :

expr → tactic.ring.ring_m (tactic.ring.horner_expr × expr)

Evaluate a ring expression e recursively to normal form, together with a proof of equality.

meta def tactic.ring.eval' (red : tactic.transparency) (atoms : tactic.ref (buffer expr)) (norm_atom : expr → tactic (expr × expr)) (e : expr) :

tactic (expr × expr)

Evaluate a ring expression e recursively to normal form, together with a proof of equality.

theorem tactic.ring.horner_def' {α : Type u_1} [comm_semiring α] (a x : α) (n : ℕ) (b : α) :

tactic.ring.horner a x n b = x ^ n * a + b

theorem tactic.ring.mul_assoc_rev {α : Type u_1} [semigroup α] (a b c : α) :

a * (b * c) = a * b * c

theorem tactic.ring.pow_add_rev {α : Type u_1} [monoid α] (a : α) (m n : ℕ) :

a ^ m * a ^ n = a ^ (m + n)

theorem tactic.ring.pow_add_rev_right {α : Type u_1} [monoid α] (a b : α) (m n : ℕ) :

b * a ^ m * a ^ n = b * a ^ (m + n)

theorem tactic.ring.add_neg_eq_sub {α : Type u_1} [add_group α] (a b : α) :

a + -b = a - b

inductive tactic.ring.normalize_mode :

If ring fails to close the goal, it falls back on normalizing the expression to a "pretty" form so that you can see why it failed. This setting adjusts the resulting form:

raw is the form that ring actually uses internally, with iterated applications of horner. Not very readable but useful if you don't want any postprocessing. This results in terms like horner (horner (horner 3 y 1 0) x 2 1) x 1 (horner 1 y 1 0).
horner maintains the Horner form structure, but it unfolds the horner definition itself, and tries to otherwise minimize parentheses. This results in terms like (3 * x ^ 2 * y + 1) * x + y.
SOP means sum of products form, expanding everything to monomials. This results in terms like 3 * x ^ 3 * y + x + y.

Instances for tactic.ring.normalize_mode

tactic.ring.normalize_mode.has_sizeof_inst
tactic.ring.normalize_mode.has_reflect
tactic.ring.normalize_mode.inhabited

@[protected, instance]

def tactic.ring.normalize_mode.decidable_eq :

decidable_eq tactic.ring.normalize_mode

@[protected, instance]

meta def tactic.ring.normalize_mode.has_reflect :

has_reflect tactic.ring.normalize_mode

@[protected, instance]

def tactic.ring.normalize_mode.inhabited :

inhabited tactic.ring.normalize_mode

Equations

tactic.ring.normalize_mode.inhabited = {default := tactic.ring.normalize_mode.horner}

meta def tactic.ring.normalize' (atoms : tactic.ref (buffer expr)) (red : tactic.transparency) (mode : tactic.ring.normalize_mode := tactic.ring.normalize_mode.horner) (recursive : bool := bool.tt) :

expr → (bool := bool.ff) → tactic (expr × expr)

A ring-based normalization simplifier that rewrites ring expressions into the specified mode. See normalize. This version takes a list of atoms to persist across multiple calls.

atoms: a mutable reference containing the atom set from the previous call
red: the reducibility setting to use when comparing atoms for defeq
mode: the normalization style (see normalize_mode)
recursive: if true, atoms will be reduced recursively using normalize'
e: the expression to normalize
inner: This should be set to ff. It is used internally to disable normalization at the top level when called from eval in order to prevent an infinite loop eval' -> eval_atom -> normalize' -> eval' when called on something that can't be simplified like x.

meta def tactic.ring.normalize (red : tactic.transparency) (mode : tactic.ring.normalize_mode := tactic.ring.normalize_mode.horner) (recursive : bool := bool.tt) (e : expr) :

tactic (expr × expr)

A ring-based normalization simplifier that rewrites ring expressions into the specified mode.

raw is the form that ring actually uses internally, with iterated applications of horner. Not very readable but useful if you don't want any postprocessing. This results in terms like horner (horner (horner 3 y 1 0) x 2 1) x 1 (horner 1 y 1 0).
horner maintains the Horner form structure, but it unfolds the horner definition itself, and tries to otherwise minimize parentheses. This results in terms like (3 * x ^ 2 * y + 1) * x + y.
SOP means sum of products form, expanding everything to monomials. This results in terms like 3 * x ^ 3 * y + x + y.

structure tactic.ring.ring_nf_cfg :

recursive : bool

Configuration for ring_nf.

recursive: if true, atoms inside ring expressions will be reduced recursively

Instances for tactic.ring.ring_nf_cfg

tactic.ring.ring_nf_cfg.has_sizeof_inst
tactic.ring.ring_nf_cfg.inhabited

@[protected, instance]

def tactic.ring.ring_nf_cfg.inhabited :

inhabited tactic.ring.ring_nf_cfg

meta def tactic.interactive.ring1 (red : interactive.parse (optional (lean.parser.tk "!"))) :

Tactic for solving equations in the language of commutative (semi)rings. This version of ring fails if the target is not an equality that is provable by the axioms of commutative (semi)rings.

meta def tactic.interactive.ring.mode :

lean.parser tactic.ring.normalize_mode

Parser for ring_nf's mode argument, which can only be the "keywords" raw, horner or SOP. (Because these are not actually keywords we use a name parser and postprocess the result.)

meta def tactic.interactive.ring_nf (red : interactive.parse (optional (lean.parser.tk "!"))) (SOP : interactive.parse tactic.interactive.ring.mode) (loc : interactive.parse interactive.types.location) (cfg : tactic.ring.ring_nf_cfg := {recursive := bool.tt}) :

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form. When writing a normal form, ring_nf SOP will use sum-of-products form instead of horner form. ring_nf! will use a more aggressive reducibility setting to identify atoms.

meta def tactic.interactive.ring (red : interactive.parse (optional (lean.parser.tk "!"))) :

Tactic for solving equations in the language of commutative (semi)rings. ring! will use a more aggressive reducibility setting to identify atoms.

If the goal is not solvable, it falls back to rewriting all ring expressions into a normal form, with a suggestion to use ring_nf instead, if this is the intent. See also ring1, which is the same as ring but without the fallback behavior.

Based on Proving Equalities in a Commutative Ring Done Right in Coq by Benjamin Grégoire and Assia Mahboubi.

def tactic_doc.tactic.ring :

tactic_doc_entry

Tactic for solving equations in the language of commutative (semi)rings. ring! will use a more aggressive reducibility setting to identify atoms.

If the goal is not solvable, it falls back to rewriting all ring expressions into a normal form, with a suggestion to use ring_nf instead, if this is the intent. See also ring1, which is the same as ring but without the fallback behavior.

Based on Proving Equalities in a Commutative Ring Done Right in Coq by Benjamin Grégoire and Assia Mahboubi.

meta def conv.interactive.ring_nf (red : interactive.parse (optional (lean.parser.tk "!"))) (SOP : interactive.parse tactic.interactive.ring.mode) (cfg : tactic.ring.ring_nf_cfg := {recursive := bool.tt}) :

Normalises expressions in commutative (semi-)rings inside of a conv block using the tactic ring.

meta def conv.interactive.ring (red : interactive.parse (optional (lean.parser.tk "!"))) :

Normalises expressions in commutative (semi-)rings inside of a conv block using the tactic ring.