The eq operation on atoms works modulo definitional equality, ignoring their values. The invariants on atom ensure indices are unique per value. Thus, eq indicates equality as long as the atoms come from the same context.

We order atoms on the order of appearance in the main expression.

Return the proof information associated to the ex.

Return the original, non-normalized version of this ex.

Note that arguments to another ex are always "pre-normalized": their orig and pretty are equal, and their proof is reflexivity.

Return the normalized version of this ex.

Return the normalisation proof of the given expression. If the proof is refl, we give none instead, which helps to control the size of proof terms. To get an actual term, use ex.proof_term, or use mk_proof with the correct set of arguments.

Update the orig and proof fields of the ex_info. Intended for use in ex.set_info.

Update the ex_info of the given expression.

We use this to combine intermediate normalisation proofs. Since pretty only depends on the subexpressions, which do not change, we do not set pretty.

Convert an ex to a string.

Equality test for expressions.

Since equivalence of atoms is not the same as equality, we cannot make a true (=) operator for ex either.

The ordering on expressions.

As for ex.eq, this is a linear order only in one context.

The ring_exp_m monad is used instead of tactic to store the context.

Access the instance cache.

Lift an operation in the tactic monad to the ring_exp_m monad.

This operation will not access the cache.

Change the context of the given computation, so that expressions are evaluated in the exponent ring, instead of the base ring.

Specialized version of mk_app where the first two arguments are {α} [some_class α]. Should be faster because it can use the cached instances.

Specialized version of mk_app where the first two arguments are {α} [comm_semiring α]. Should be faster because it can use the cached instances.

Specialized version of mk_app ``has_add.add. Should be faster because it can use the cached instances.

Specialized version of mk_app ``has_mul.mul. Should be faster because it can use the cached instances.

Specialized version of mk_app ``has_pow.pow. Should be faster because it can use the cached instances.

Construct a normalization proof term or return the cached one.

Construct a normalization proof term or return the cached one.

If all 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 mk_proof_or_refl.

Use the proof terms as arguments to the given lemma. If the lemma could reduce to reflexivity, consider using mk_proof_or_refl.

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 shortcut for adding the original terms of two expressions.

A shortcut for multiplying the original terms of two expressions.

A shortcut for exponentiating the original terms of two expressions.

Constructs ex.zero with the correct arguments.

Constructs ex.sum with the correct arguments.

Constructs ex.coeff with the correct arguments.

There are more efficient constructors for specific numerals: if x = 0, you should use ex_zero; if x = 1, use ex_one.

Constructs ex.coeff 1 with the correct arguments. This is a special case for optimization purposes.

Constructs ex.prod with the correct arguments.

Constructs ex.var with the correct arguments.

Constructs ex.sum_b with the correct arguments.

Constructs ex.exp with the correct arguments.

Conversion from ex base to ex exp.

Conversion from ex exp to ex prod.

Conversion from ex prod to ex sum.

A more efficient conversion from atom to ex sum.

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: if p = -q, then the result should be ex.zero : ex sum instead. The caller must detect when this happens!

The returned value is of the form ex.coeff _ (p + q), with the proof of expr.of_rat p + expr.of_rat q = expr.of_rat (p + q).

Compute the product of two coefficients.

The returned value is of the form ex.coeff _ (p * q), with the proof of expr.of_rat p * expr.of_rat q = expr.of_rat (p * q).

Given a proof that the expressions ps_o and ps'.orig are equal, show that ps_o and 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:

| ps_o@`(nat.succ %%p_o) := do
  ps' ← eval `(%%p_o + 1),
  pf ← lift $ mk_app ``nat.succ_eq_add_one [p_o],
  rewrite ps_o ps' pf

Given arguments ps, qs of the form ps' * x and ps' * y respectively return ps + qs = ps' * (x + y) (with x and y arbitrary coefficients). For other arguments, return overlap.none.

Add two expressions.

• 0 + qs = 0
• ps + 0 = 0
• ps * x + ps * y = ps * (x + y) (for x, y coefficients; uses add_overlap)
• (p + ps) + (q + qs) = p + (ps + (q + qs)) (if p.lt q)
• (p + ps) + (q + qs) = q + ((p + ps) + qs) (if not p.lt q)

Multiply two expressions.

• x * y = (x * y) (for x, y coefficients)
• x * (q * qs) = q * (qs * x) (for x coefficient)
• (p * ps) * y = p * (ps * y) (for y coefficient)
• (p_b^p_e * ps) * (p_b^q_e * qs) = p_b^(p_e + q_e) * (ps * qs) (if p_e and q_e are identical except coefficient)
• (p * ps) * (q * qs) = p * (ps * (q * qs)) (if p.lt q)
• (p * ps) * (q * qs) = q * ((p * ps) * qs) (if not p.lt q)

Multiply two expressions.

• 0 * qs = 0
• (p + ps) * qs = (p * qs) + (ps * qs)

Multiply two expressions.

• ps * 0 = 0
• ps * (q + qs) = (ps * q) + (ps * qs)

Compute the exponentiation of two coefficients.

The returned value is of the form ex.coeff _ (p ^ q), with the proof of expr.of_rat p ^ expr.of_rat q = expr.of_rat (p ^ q).

Exponentiate two expressions.

• (p ^ ps) ^ qs = p ^ (ps * qs)

Exponentiate two expressions.

• 1 ^ qs = 1
• x ^ qs = x ^ qs (for x coefficient)
• (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)

Exponentiate two expressions.

• ps ^ 0 = 1
• ps ^ (q + qs) = ps ^ q * ps ^ qs

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 a instead. This tactic gets rid of the dummy additions, multiplications and exponentiations.

Returns a normalized expression e' and a proof that e.pretty = e'.

Performs a lookup of the atom a in the list of known atoms, or allocates a new one.

If 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 resolve_atom, 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_base if eval doesn't work instead of directly calling resolve_atom, since 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.

Negate an expression by multiplying with -1.

Only works if there is a ring instance; otherwise it will fail.

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

Compute a normalized form (of type ex) from an expression (of type expr).

This is the main driver of the ring_exp tactic, calling out to add, mul, pow, etc. to parse the expr.

Run eval on the expression and return the result together with normalization proof.

See also eval_simple if you want something that behaves like norm_num.

Run eval on the expression and simplify the result.

Returns a simplified normalized expression, together with an equality proof.

See also eval_with_proof if you just want to check the equality of two expressions.

Compute the eval_info for a given type α.

Use e to build the context for running mx.

Repeatedly apply eval_simple on (sub)expressions.

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.

The variant 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 (where ring only understands constant exponents). The variants ring_exp! and ring_exp_eq! use a more aggessive reducibility setting to determine equality of atoms.

For example:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring_exp
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring_exp
example (x y : ℕ) : x + id y = y + id x := by ring_exp!

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