mathlib 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 α] :
α → α → α → α

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
meta structure tactic.ring.cache  :
Type

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

meta def tactic.ring.ring_m  :
Type → 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.

Get the ring data from the monad.

Get an already encountered atom by its index.

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} :

Lift a tactic into the ring_m monad.

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

Run a ring_m tactic in the tactic monad.

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).

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

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.

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  :
Type

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.

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.

Is this expr the constant 0?

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

Pretty printer for horner_expr.

Pretty printer for horner_expr.

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

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

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' : α) :
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' : α) :
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' : α) :
n₁ + k = n₂a₁ + tactic.ring.horner a₂ x k 0 = a'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' : α) :
n₂ + k = n₁tactic.ring.horner a₁ x k 0 + a₂ = a'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 : α) :
a₁ + a₂ = a'b₁ + b₂ = b'tactic.ring.horner a' x n b' = ttactic.ring.horner a₁ x n b₁ + tactic.ring.horner a₂ x n b₂ = t

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' : α) :
-a = a'-b = b'-tactic.ring.horner a x n b = tactic.ring.horner a' x n b'

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' : α) :
c * a = a'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' : α) :
a * c = a'b * c = b'(tactic.ring.horner a x n b) * c = tactic.ring.horner a' x n b'

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 : α) :
(tactic.ring.horner a₁ x n₁ b₁) * a₂ = aatactic.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 : α) :
(tactic.ring.horner a₁ x n₁ b₁) * a₂ = aatactic.ring.horner aa x n₂ 0 = haaa₁ * b₂ = abb₁ * b₂ = bbhaa + tactic.ring.horner ab x n₁ bb = t(tactic.ring.horner a₁ x n₁ b₁) * tactic.ring.horner a₂ x n₂ b₂ = t

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' : α) :
n * m = n'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 : α) :
a ^ n = bb * a = ca ^ (n + 1) = c

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 : α) :

Evaluate a where a is an atom.

theorem tactic.ring.subst_into_pow {α : Type u_1} [monoid α] (l : α) (r : ) (tl : α) (tr : ) (t : α) :
l = tlr = trtl ^ tr = tl ^ r = t

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

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

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

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  :
Type

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.

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.

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.

Parser for ring'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.)

Tactic for solving equations in the language of commutative (semi)rings. 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 ring expressions into a normal form. When writing a normal form, ring SOP will use sum-of-products form instead of horner form. ring! will use a more aggressive reducibility setting to identify atoms.

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

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