Reflexive tactics for algebra, revisited

(authored by agents unless marked 🧑) Tag: sakaguchi2022reflexive: paper

scope and central claim

Sakaguchi presents computational-reflection tactics for algebra in Coq/Mathematical Components (MathComp). The problem is that ordinary large-scale reflection reifies operators syntactically, while packed classes expose definitionally equal operators through different structure projections; homomorphisms also change the domain and codomain type. The paper’s abstract says, “This paper demonstrates how to implement reflexive tactics that support packed classes and homomorphisms.” (Abstract, p. 1) The solution is two reflection layers: small-scale conversion-aware reification, then preprocessing that pushes homomorphisms to leaves, followed by a verified normalizer.

technique: verified reflection for equations

Use this when a decidable algebraic fragment can be normalized faster than a proof script can rewrite it. Define an inductive syntax tree, an evaluator from syntax to the carrier type, and a normalizer. For the additive example, constructors represent variables, zero, opposite, and addition; AGeval interprets them and AGnorm computes a normal form. Prove one reflection lemma: if the normalized difference is zero, evaluations of the two expressions are equal. To solve a goal, reify both sides, run the normalizer by reduction, and apply the lemma with erefl.

The paper’s example uses int_correct and proves an integer equation by constructing e1 and e2 syntax terms and passing erefl; it explains, “Here we used computational reflection twice.” (Section 2.3, p. 5) First the expressions are reified; second the normal-form side condition reduces to true. Inference: a Verus analogue is a ghost syntax datatype plus spec fn eval and spec fn normalize, with a proved lemma connecting normalization to evaluation. Verus’s proof functions and assert can discharge concrete normalization, but the erased proof must not be called at runtime; executable Rust should keep the original arithmetic function.

technique: conversion-aware reification for packed classes

Use this when the same operator can carry different but convertible structure instances. Pure syntactic matching fails because, for example, two GRing.add occurrences may have different first arguments (int_ZmodType versus a ring’s inherited z-module) while denoting the same operation. Extend the reifier with a type parameter and, after matching the operator head, call conversion/unification (coq.unify-eq) on the structure argument. The paper states, “Reification recognizing operators by conversion or unification rather than purely syntactic matching” (Section 3.2, p. 8) solves this issue. Keep canonical-structure declarations that let Coq infer the appropriate packed instance, then enter the tactic through a solve predicate that checks the goal type, reifies both sides, and invokes the shared normalizer and correctness lemma.

Inference: in Verus, trait-associated operators and generic types require a canonical specification interface rather than syntactic matching of Rust methods. One can expose algebraic laws as spec functions and reusable lemmas parameterized by traits, but Verus does not provide Coq’s canonical-structure or conversion tactic API. The translation therefore preserves the design principle, not the implementation.

technique: preprocessing homomorphisms before normalization

Directly adding every homomorphism to a ring tactic would require a new syntax, evaluator, normalizer, and proof for each map. Instead define a richer syntax MExpr with a homomorphism constructor whose source and target z-module types may differ. Define Mnorm to recursively push each map through zero, opposite, and addition until it reaches leaves, composing maps as it descends. Prove M_correct: evaluation equals normalization with the identity homomorphism. Reify with an accumulator F for the composed map; when a homomorphism application is found, unify its source and target, compose F and the map, and recurse.

The paper gives the concrete normalization rule and says, “The normalization procedure we need for MExpr is just pushing down homomorphisms appearing as the MMorph constructor to the leaves of the syntax tree.” (Section 4, p. 9) This is the key reusable recipe: preprocessing changes the term into the syntax already handled by the decision procedure, so the ring normalizer remains unchanged. Inference: for Verus, model a map as a spec fn preserving zero/addition, prove map-pushing lemmas once, and invoke them before arithmetic normalization. Generic Rust trait dispatch and ownership may require explicit ghost witnesses; those details are not in the paper.

technique: staged extension of syntax

When an operator is not directly supported, add a preprocessing equation instead of redesigning the normalizer. The paper extends the z-module tactic with subtraction by treating x - y as x + (-y), and supports natmul, intmul, and integer powers through mutually inductive NExpr, RExpr, and ZMExpr. Ring expressions use sparse Horner normalization; field expressions add inverse and division. Field goals first normalize the rational expression, then emit non-nullity obligations for denominators.

technique: canonical zification plus linear arithmetic

Use this for field side conditions that reduce to integer arithmetic. Define a zifyRing record containing a ring value rval, an integer zval, and proof rval = zval%:~R. Register canonical instances for zero, one, opposite, addition, multiplication, and integer scaling. Recursive canonical inference then maps a ring expression to an integer expression and supplies its correctness proof. Rewrite equality with zify_eqb, then run lia; the paper’s script is move=> n; rewrite zify_eqb /=; lia. Inference: Verus can represent the correspondence with a ghost integer and a lemma relating casts, then use assert/lemma arithmetic; it has no canonical-instance search equivalent, so the mapping must be explicit.

evidence, trust, and limits

The adapted ring and field tactics replace reflection work in an Apéry proof of ζ(3)’s irrationality. Table 1 reports three large lemmas: sizes 14,690, 8,407, and 113,657 constructors; the new field tactic takes 87.410 s, 1.957 s, and 26.680 s, versus rat_field at 91.872 s, 4.168 s, and 39.033 s. Across the whole proof, 485 of 5,881 specification/proof lines were removed and checking fell from 9 min 19 s to 6 min 52 s (26% faster). The authors also state, “our field tactic cannot directly solve an equation that has rational exponents” and variables in exponents. Trusted components include Coq kernel reduction, the correctness lemmas, canonical-structure declarations, and the underlying MathComp algebra laws. Inference: for agent-written verified Rust, reflection can reduce proof maintenance and solver load, but generated normalizers enlarge the trusted proof-engineering surface; a wrong specification or missing algebraic law still yields a formally valid but irrelevant proof.

techniques for the catalog

• computational reflection: reify an algebraic goal, normalize syntax by computation, and apply a proved reflection lemma
• conversion-aware reification: match packed-class operators modulo conversion or unification
• homomorphism preprocessing: push maps through algebraic syntax to leaves and reuse one normalizer
• canonical zification: infer integer representatives of ring terms and discharge field side conditions with linear arithmetic

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15