ring_exp tactic #
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
Implementation notes #
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
expression section #
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.
operations section #
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 α.
rewrite section #
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.
wiring section #
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