An experimental variant on the ring tactic that uses computational reflection instead of proof generation. Useful for kernel benchmarking.
(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.
Returns an element indexed by n, or zero if n isn't a valid index. See tree.get.
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.
Evaluates a reflected csring_expr into an element of the original comm_semiring type α, retrieving opaque elements (atoms) from the tree t.
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.
Represent a csring_expr.atom in Horner form.
Alternative constructor for (horner a x n b) which maintains canonical form by simplifying special cases of a.
Brings expressions into Horner normal form.
Evaluates a reflected horner_expr - see csring_expr.eval.
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.
Tactic for solving equations in the language of rings. This variant on the ring tactic uses kernel computation instead of proof generation.