mathlib documentation

tactic.ring2

ring2

An experimental variant on the ring tactic that uses computational reflection instead of proof generation. Useful for kernel benchmarking.

meta def tree.reflect'  :
levelexprtree exprexpr

(reflect' t u α) quasiquotes a tree (t: tree expr) of quoted values of type α at level u into an expr which reifies to a tree α containing the reifications of the exprs from the original t.

def tree.get_or_zero {α : Type u_1} [has_zero α] :
tree αpos_num → α

Returns an element indexed by n, or zero if n isn't a valid index. See tree.get.

Equations
inductive tactic.ring2.csring_expr  :
Type

A reflected/meta representation of an expression in a commutative semiring. This representation is a direct translation of such expressions - see horner_expr for a normal form.

inductive tactic.ring2.horner_expr  :
Type

An efficient representation of expressions in a commutative semiring using the sparse Horner normal form. This type admits non-optimal instantiations (e.g. P can be represented as P+0+0), so to get good performance out of it, care must be taken to maintain an optimal, canonical form.

True iff the horner_expr argument is a valid csring_expr. For that to be the case, all its constants must be non-negative.

Equations

Represent a csring_expr.atom in Horner form.

Equations

Alternative constructor for (horner a x n b) which maintains canonical form by simplifying special cases of a.

Equations

Equations
  • a₁.add_aux A₁ x₁ (a₂.horner x₂ n₂ b₂) n₁ b₁ B₁ = let e₂ : tactic.ring2.horner_expr := a₂.horner x₂ n₂ b₂ in tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ (a₁.add_aux A₁ x₁ b₂ n₁ b₁ B₁) (λ (k : pos_num), a₁.add_aux A₁ x₁ a₂ k 0 id) (x₁.cmp x₂)
  • a₁.add_aux A₁ x₁ (tactic.ring2.horner_expr.const n₂) n₁ b₁ B₁ = tactic.ring2.horner_expr.add_const n₂ (a₁.horner x₁ n₁ b₁)
  • tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ _f_1 _f_2 ordering.gt = a₂.horner x₂ n₂ _f_1
  • tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ _f_1 _f_2 ordering.eq = tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ (λ (k : pos_num), _f_2 k) (n₁.sub' n₂)
  • tactic.ring2.horner_expr.add_aux._match_1 a₁ A₁ x₁ a₂ x₂ n₂ b₂ n₁ B₁ e₂ _f_1 _f_2 ordering.lt = a₁.horner x₁ n₁ (B₁ e₂)
  • tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ _f_1 (znum.neg k) = (A₁ (a₂.horner x₁ k 0)).horner x₁ n₁ (B₁ b₂)
  • tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ _f_1 (znum.pos k) = (_f_1 k).horner x₁ n₂ (B₁ b₂)
  • tactic.ring2.horner_expr.add_aux._match_2 A₁ x₁ a₂ n₂ b₂ n₁ B₁ _f_1 znum.zero = (A₁ a₂).horner' x₁ n₁ (B₁ b₂)

Equations

Equations

Equations

Equations

For any given tree t of atoms and any reflected expression r, the Horner form of r is a valid csring expression, and under t, the Horner form evaluates to the same thing as r.

The main proof-by-reflection theorem. Given reflected csring expressions r₁ and r₂ plus a storage t of atoms, if both expressions go to the same Horner normal form, then the original non-reflected expressions are equal. H follows from kernel reduction and is therefore rfl.

Reflects a csring expression into a csring_expr, together with a dlist of atoms, i.e. opaque variables over which the expression is a polynomial.

In the output of reflect_expr, atoms are initialized with incorrect indices. The indices cannot be computed until the whole tree is built, so another pass over the expressions is needed - this is what replace does. The computation (expressed in the state monad) fixes up atoms to match their positions in the atom tree. The initial state is a list of all atom occurrences in the goal, left-to-right.

ring2 solves equations in the language of rings.

It supports only the commutative semiring operations, i.e. it does not normalize subtraction or division.

This variant on the ring tactic uses kernel computation instead of proof generation. In general, you should use ring instead of ring2.