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 .
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
contains only one
comm_semiring instance at the top level. See also
horner_expr for a
description of normal form.
- tactic.ring.horner a x n b = a * x ^ n + b
- raw : tactic.ring.normalize_mode
- SOP : tactic.ring.normalize_mode
- horner : tactic.ring.normalize_mode
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:
rawis the form that
ringactually 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).
hornermaintains the Horner form structure, but it unfolds the
hornerdefinition itself, and tries to otherwise minimize parentheses. This results in terms like
(3 * x ^ 2 * y + 1) * x + y.
SOPmeans sum of products form, expanding everything to monomials. This results in terms like
3 * x ^ 3 * y + x + y.
- recursive : bool
recursive: if true, atoms inside ring expressions will be reduced recursively
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.
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.