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} (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
• n b = a * x ^ n + b
meta structure tactic.ring.cache  :
Type

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

@[instance]
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.

@[instance]

Get the ring data from the monad.

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

Get an already encountered atom by its index.

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

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

Lift a tactic into the ring_m monad.

meta def tactic.ring.ring_m.run' (red : tactic.transparency) (atoms : tactic.ref ) (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' {α : Type}  :

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

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

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
• const :

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?

@[instance]
@[instance]

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

Pretty printer for horner_expr.

Pretty printer for horner_expr.

@[instance]

Reflexivity conversion for a horner_expr.

theorem tactic.ring.zero_horner {α : Type u_1} (x : α) (n : ) (b : α) :
n b = b
theorem tactic.ring.horner_horner {α : Type u_1} (a₁ x : α) (n₁ n₂ : ) (b : α) (n' : ) (h : n₁ + n₂ = n') :
tactic.ring.horner x n₁ 0) x n₂ b = 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} (k a x : α) (n : ) (b b' : α) (h : k + b = b') :
k + n b = n b'
theorem tactic.ring.horner_add_const {α : Type u_1} (a x : α) (n : ) (b k b' : α) (h : b + k = b') :
n b + k = n b'
theorem tactic.ring.horner_add_horner_lt {α : Type u_1} (a₁ x : α) (n₁ : ) (b₁ a₂ : α) (n₂ : ) (b₂ : α) (k : ) (a' b' : α) (h₁ : n₁ + k = n₂) (h₂ : a₁ + k 0 = a') (h₃ : b₁ + b₂ = b') :
n₁ b₁ + n₂ b₂ = n₁ b'
theorem tactic.ring.horner_add_horner_gt {α : Type u_1} (a₁ x : α) (n₁ : ) (b₁ a₂ : α) (n₂ : ) (b₂ : α) (k : ) (a' b' : α) (h₁ : n₂ + k = n₁) (h₂ : k 0 + a₂ = a') (h₃ : b₁ + b₂ = b') :
n₁ b₁ + n₂ b₂ = n₂ b'
theorem tactic.ring.horner_add_horner_eq {α : Type u_1} (a₁ x : α) (n : ) (b₁ a₂ b₂ a' b' t : α) (h₁ : a₁ + a₂ = a') (h₂ : b₁ + b₂ = b') (h₃ : n b' = t) :
n b₁ + 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' : α) (h₁ : -a = a') (h₂ : -b = b') :
- n b = n b'

Evaluate -a where a is already in normal form.

theorem tactic.ring.horner_const_mul {α : Type u_1} (c a x : α) (n : ) (b a' b' : α) (h₁ : c * a = a') (h₂ : c * b = b') :
c * n b = n b'
theorem tactic.ring.horner_mul_const {α : Type u_1} (a x : α) (n : ) (b c a' b' : α) (h₁ : a * c = a') (h₂ : b * c = b') :
n b) * c = 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} (a₁ x : α) (n₁ : ) (b₁ a₂ : α) (n₂ : ) (aa t : α) (h₁ : x n₁ b₁) * a₂ = aa) (h₂ : n₂ 0 = t) :
x n₁ b₁) * n₂ 0 = t
theorem tactic.ring.horner_mul_horner {α : Type u_1} (a₁ x : α) (n₁ : ) (b₁ a₂ : α) (n₂ : ) (b₂ aa haa ab bb t : α) (h₁ : x n₁ b₁) * a₂ = aa) (h₂ : n₂ 0 = haa) (h₃ : a₁ * b₂ = ab) (h₄ : b₁ * b₂ = bb) (H : haa + n₁ bb = t) :
x n₁ b₁) * n₂ b₂ = t

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

theorem tactic.ring.horner_pow {α : Type u_1} (a x : α) (n m n' : ) (a' : α) (h₁ : n * m = n') (h₂ : a ^ m = a') :
n 0 ^ m = n' 0
theorem tactic.ring.pow_succ {α : Type u_1} (a : α) (n : ) (b c : α) (h₁ : a ^ n = b) (h₂ : b * a = c) :
a ^ (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} (x : α) :
x = 1 0
meta def tactic.ring.eval_atom (e : 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} (a b c : α) (h : a * b⁻¹ = c) :
a / b = c

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 ) (e : expr) :

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

theorem tactic.ring.horner_def' {α : Type u_1} (a x : α) (n : ) (b : α) :
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.
@[instance]
@[instance]
Equations

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

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.

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.

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

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