A tactic for solving equations in commutative (semi)rings, where the exponents can also contain variables.
More precisely, expressions of the following form are supported:
- constants (non-negative integers)
- coefficients (any rational number, embedded into the (semi)ring)
- addition of expressions
- multiplication of expressions
- exponentiation of expressions (the exponent must have type
- subtraction and negation of expressions (if the base is a full ring)
The motivating example is proving
2 * 2^n * b = b * 2^(n+1),
something that the
ring tactic cannot do, but
The basic approach to prove equalities is to normalise both sides and check for equality.
The normalisation is guided by building a value in the type
ex at the meta level,
together with a proof (at the base level) that the original value is equal to
the normalised version.
The normalised version and normalisation proofs are also stored in the
The outline of the file:
- Define an inductive family of types
ex, parametrised over
ex_type, which can represent expressions with
^and rational numerals. The parametrisation over
ex_typeensures that associativity and distributivity are applied, by restricting which kinds of subexpressions appear as arguments to the various operators.
- Represent addition, multiplication and exponentiation in the
extype, thus allowing us to map expressions to
evalfunction drives this). We apply associativity and distributivity of the operators here (helped by
ex_type) and commutativity as well (by sorting the subterms; unfortunately not helped by anything). Any expression not of the above formats is treated as an atom (the same as a variable).
There are some details we glossed over which make the plan more complicated:
- The order on atoms is not initially obvious. We construct a list containing them in order of initial appearance in the expression, then use the index into the list as a key to order on.
- In the tactic, a normalized expression
ps : exlives in the meta-world, but the normalization proofs live in the real world. Thus, we cannot directly say
ps.orig = ps.prettyanywhere, but we have to carefully construct the proof when we compute
ps. This was a major source of bugs in development!
pow, the exponent must be a natural number, while the base can be any semiring
α. We swap out operations for the base ring
αwith those for the exponent ring
ℕas soon as we deal with exponents. This is accomplished by the
in_exponentfunction and is relatively painless since we work in a
- The normalized form of an expression is the one that is useful for the tactic,
but not as nice to read. To remedy this, the user-facing normalization calls
Caveats and future work
Subtraction cancels out identical terms, but division does not.
a - a = 0 := by ring_exp solves the goal,
a / a := 1 by ring_exp doesn't.
0 / 0 is generally defined to be
so division cancelling out is not true in general.
Multiplication of powers can be simplified a little bit further:
2 ^ n * 2 ^ n = 4 ^ n := by ring_exp could be implemented
in a similar way that
2 * a + 2 * a = 4 * a := by ring_exp already works.
This feature wasn't needed yet, so it's not implemented yet.
ring, semiring, exponent, power
atom structure is used to represent atomic expressions:
ring_exp cannot parse any further.
a + (a % b) has
(a % b) as atoms.
ring_exp_eq tactic does not normalize the subexpressions in atoms,
ring_exp does if
ring_exp_eq was not sufficient.
Atoms in fact represent equivalence classes of expressions,
modulo definitional equality.
index : ℕ should be a unique number for each class,
value : expr contains a representative of this class.
resolve_atom determines the appropriate atom
for a given expression.
In this section, we define the
ex type and its basic operations.
First, we introduce the supporting types
For understanding the code, it's easier to check out
ex itself first,
then refer back to the supporting types.
The arithmetic operations on
ex need additional definitions,
so they are defined in a later section.
ex stores information for its normalization proof.
orig expression is the expression that was passed to
pretty expression is the normalised form that the
(I didn't call this something like
norm, because there are already
too many things called
norm in mathematics!)
proof contains an optional proof term of type
%%orig = %%pretty.
none for the proof indicates that everything reduces to reflexivity.
(Which saves space in quite a lot of cases.)
- zero : tactic.ring_exp.ex_info → tactic.ring_exp.ex tactic.ring_exp.ex_type.sum
- sum : tactic.ring_exp.ex_info → tactic.ring_exp.ex tactic.ring_exp.ex_type.prod → tactic.ring_exp.ex tactic.ring_exp.ex_type.sum → tactic.ring_exp.ex tactic.ring_exp.ex_type.sum
- coeff : tactic.ring_exp.ex_info → tactic.ring_exp.coeff → tactic.ring_exp.ex tactic.ring_exp.ex_type.prod
- prod : tactic.ring_exp.ex_info → tactic.ring_exp.ex tactic.ring_exp.ex_type.exp → tactic.ring_exp.ex tactic.ring_exp.ex_type.prod → tactic.ring_exp.ex tactic.ring_exp.ex_type.prod
- var : tactic.ring_exp.ex_info → tactic.ring_exp.atom → tactic.ring_exp.ex tactic.ring_exp.ex_type.base
- sum_b : tactic.ring_exp.ex_info → tactic.ring_exp.ex tactic.ring_exp.ex_type.sum → tactic.ring_exp.ex tactic.ring_exp.ex_type.base
- exp : tactic.ring_exp.ex_info → tactic.ring_exp.ex tactic.ring_exp.ex_type.base → tactic.ring_exp.ex tactic.ring_exp.ex_type.prod → tactic.ring_exp.ex tactic.ring_exp.ex_type.exp
coeff constructor is the base case for
ex prod, and is used for numerals.
The code maintains the invariant that the coefficient is never
var constructor is the base case for
ex exp, and is used for atoms.
sum_b constructor allows for addition in the base of an exponentiation;
it serves a similar purpose as the parentheses in
(a + b)^c.
The code maintains the invariant that the argument to
sum_b is not
sum _ zero.
All of the constructors contain an
used to carry around (arguments to) proof terms.
ex_type parameter enforces some simplification invariants,
the following ones must be manually maintained at the risk of insufficient power:
- the argument to
coeffmust be nonzero (to ensure
0 = 0 * 1)
- the argument to
sum_bmust be of the form
sum a (sum b bs)(to ensure
(a + 0)^n = a^n)
- normalisation proofs of subexpressions must be
- if we replace
nil, the resulting list is sorted according to the
ltrelation defined further down; similarly for
a + b = b + a).
The first two invariants could be encoded in a subtype of
but aren't (yet) to spare some implementation burden.
The other invariants cannot be encoded because we need the
tactic monad to check them.
(For example, the correct equality check of
is_def_eq : expr → expr → tactic unit.)
Return the normalisation proof of the given expression.
If the proof is
refl, we give
which helps to control the size of proof terms.
To get an actual term, use
mk_proof with the correct set of arguments.
ex_info of the given expression.
We use this to combine intermediate normalisation proofs.
pretty only depends on the subexpressions,
which do not change, we do not set
This section defines the operations (on
ex) that use tactics.
They live in the
which adds a cache and a list of encountered atoms to the
Throughout this section, we will be constructing proof terms. The lemmas used in the construction are all defined over a commutative semiring α.
- α : expr
- univ : level
- csr_instance : expr
- ha_instance : expr
- hm_instance : expr
- hp_instance : expr
- ring_instance : option expr
- dr_instance : option expr
- zero : expr
- one : expr
Stores the information needed in the
eval function and its dependencies,
so they can (re)construct expressions.
eval_info structure stores this information for one type,
context combines the two types, one for bases and one for exponents.
context contains the full set of information needed for the
This structure has two copies of
one is for the base (typically some semiring
α) and another for the exponent (always
When evaluating an exponent, we put
ex_info have trivial proofs, return a trivial proof.
Otherwise, construct all proof terms.
Useful in applications where trivial proofs combine to another trivial proof,
most importantly to pass to
Use the proof terms as arguments to the given lemma. Often, we construct a proof term using congruence where reflexivity suffices. To solve this, the following function tries to get away with reflexivity.
A more efficient conversion from
The result should be the same as
ex_var p >>= base_to_exp >>= exp_to_prod >>= prod_to_sum,
except we need to calculate less intermediate steps.
Compute the sum of two coefficients.
Note that the result might not be a valid expression:
p = -q, then the result should be
ex.zero : ex sum instead.
The caller must detect when this happens!
Compute the product of two coefficients.
In this section we deal with rewriting terms to fit in the basic grammar of
nat.succ n is rewritten to
n + 1 before it is evaluated further.
Given a proof that the expressions
ps'.orig are equal,
ps'.pretty are equal.
Useful to deal with aliases in
eval. For instance,
nat.succ p can be handled
as an alias of
p + 1 as follows:
- none : tactic.ring_exp.overlap
- nonzero : tactic.ring_exp.ex tactic.ring_exp.ex_type.prod → tactic.ring_exp.overlap
- zero : tactic.ring_exp.ex tactic.ring_exp.ex_type.sum → tactic.ring_exp.overlap
Represents the way in which two products are equal except coefficient.
This type is used in the function
In order to deal with equations of the form
a * 2 + a = 3 * a,
add function will add up overlapping products,
a * 2 + a into
a * 3.
We need to distinguish
a * 2 + a from
a * 2 + b in order to do this,
overlap type carries the information on how it overlaps.
none corresponds to non-overlapping products, e.g.
a * 2 + b;
nonzero to overlapping products adding to non-zero, e.g.
a * 2 + a
ex prod field will then look like
a * 3 with a proof that
a * 2 + a = a * 3);
zero to overlapping products adding to zero, e.g.
a * 2 + a * -2.
We distinguish those two cases because in the second, the whole product reduces to
A potential extension to the tactic would also do this for the base of exponents,
e.g. to show
2^n * 2^n = 4^n.
qs of the form
ps' * x and
ps' * y respectively
ps + qs = ps' * (x + y) (with
y arbitrary coefficients).
For other arguments, return
Add two expressions.
0 + qs = 0
ps + 0 = 0
ps * x + ps * y = ps * (x + y)(for
(p + ps) + (q + qs) = p + (ps + (q + qs))(if
(p + ps) + (q + qs) = q + ((p + ps) + qs)(if not
Multiply two expressions.
x * y = (x * y)(for
x * (q * qs) = q * (qs * x)(for
(p * ps) * y = p * (ps * y)(for
(p_b^p_e * ps) * (p_b^q_e * qs) = p_b^(p_e + q_e) * (ps * qs)(if
q_eare identical except coefficient)
(p * ps) * (q * qs) = p * (ps * (q * qs))(if
(p * ps) * (q * qs) = q * ((p * ps) * qs)(if not
Compute the exponentiation of two coefficients.
Exponentiate two expressions.
1 ^ qs = 1
x ^ qs = x ^ qs(for
(p * ps) ^ qs = p ^ qs + ps ^ qs
Exponentiate two expressions.
ps ^ 1 = ps
0 ^ qs = 0(note that this is handled after
ps ^ 0 = 1)
(p + 0) ^ qs = p ^ qs
ps ^ (qs + 1) = ps * ps ^ qs(note that this is handled after
p + 0 ^ qs = p ^ qs)
ps ^ qs = ps ^ qs(otherwise)
Give a simpler, more human-readable representation of the normalized expression.
Normalized expressions might have the form
a^1 * 1 + 0,
since the dummy operations reduce special cases in pattern-matching.
Humans prefer to read
This tactic gets rid of the dummy additions, multiplications and exponentiations.
Performs a lookup of the atom
a in the list of known atoms,
or allocates a new one.
a is not definitionally equal to any of the list's entries,
a new atom is appended to the list and returned.
The index of this atom is kept track of in the second inductive argument.
This function is mostly useful in
which updates the state with the new list of atoms.
Convert the expression to an atom: either look up a definitionally equal atom, or allocate it as a new atom.
You probably want to use
eval doesn't work
instead of directly calling
eval_base can also handle numerals.
Treat the expression atomically: as a coefficient or atom.
Handles cases where
eval cannot treat the expression as a known operation
because it is just a number or single variable.
Invert an expression by simplifying, applying
has_inv.inv and treating the result as an atom.
Only works if there is a
division_ring instance; otherwise it will
This section deals with going from
ex and back.
The main attraction is
eval, which uses
to calculate an
ex from a given
Other functions use
exes to produce
exprs together with a proof,
or produce the context to run
ring_exp_m from an
Tactic for solving equations of commutative (semi)rings,
allowing variables in the exponent.
This version of
ring_exp fails if the target is not an equality.
ring_exp_eq! will use a more aggressive reducibility setting
to determine equality of atoms.
Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent.
This tactic extends
ring: it should solve every goal that
ring can solve.
Additionally, it knows how to evaluate expressions with complicated exponents
ring only understands constant exponents).
ring_exp_eq! use a more aggessive reducibility setting to determine
equality of atoms.