# Tactics modulo associativity and cancellation for category theory

Kazuhiko Sakaguchi

<figure><img src="image_1.png" /></figure>

## To cite this version:

Kazuhiko Sakaguchi. Tactics modulo associativity and cancellation for category theory. 2026. hal-05521070

HAL Id: hal-05521070

https://hal.science/hal-05521070v1

Preprint submitted on 20 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Tactics modulo associativity and cancellation for category theory

Kazuhiko Sakaguchi

<figure><img src="image_3.png" /></figure>

CNRS, ENS de Lyon, UCBL, LIP, UMR 5668, France

## Abstract

We propose ROCQ tactics for equational reasoning in category theory, that enable reasoning modulo the common equational laws: associativity, i.e., $(f; g); h = f; (g; h)$, identity, i.e., id; $f = f = f$; id, and cancellation, i.e., $f; f^{-1} = id$. Our tactics consist of two building blocks: reflexive normalisation procedures modulo equational laws, and matching procedures written in ROCQ-ELPI. Unlike the modulo associativity and commutativity tactics of Braibant and Pous [4], our tactics support morphisms whose types are constrained by their source and target objects. The paper is written as a tutorial, showing how to implement and gradually extend the tactics we propose.

**2012 ACM Subject Classification** Computing methodologies → Theorem proving algorithms; Theory of computation → Automated reasoning; Theory of computation → Type theory; Theory of computation → Constraint and logic programming

**Keywords and phrases** Rocq, Elpi, proof by reflection, category theory

## 1 Introduction

Pen-and-paper proofs in category theory typically deal with associativity of morphism composition<fnref n="1" /> implicitly, and whether $f; g; h$ means $(f; g); h$ or $f; (g; h)$ hardly matters. Unfortunately, this is not the case in interactive theorem provers (ITPs). Suppose we wish to use a hypothesis $H : \forall x, a; (x; c) = f$ to rewrite $(a; b); (c; d)$ to $f; d$. To do so, we first need to rewrite the given term to $(a; (b; c)); d$ using the associativity of $;$, so that the system can find the subterm $a; (b; c)$ that syntactically matches with the LHS of $H$.

We implemented versions of *reflexivity* and *rewrite* tactics for categorical reasoning in the ROCQ Prover [15], that address the above issue by enabling reasoning modulo the following equational theories:

**AU** is the theory of associativity, i.e., $(f; g); h = f; (g; h)$, and units, i.e., id; $f = f = f$; id.

**G (which stands for group)** extends AU with (partial) left and right inverse, i.e., $f^{-1}$; $f = id$ and $g$; $g^{-1} = id$ where $f$ and $g$ are respectively split epimorphism and monomorphism. For example, our rewriting modulo AU tactic can directly rewrite $(a; b); (c; d)$ to $f; d$ in the example above. Similarly, given a hypothesis $H : f; g = h$ where $g$ is a split monomorphism, our rewriting modulo G tactic can automatically rewrite $f$ to $h; g^{-1}$, since $f = f; (g; g^{-1}) = (f; g); g^{-1}$. While our tactics are specifically implemented for the Graph Rewriting library [3], this paper presents the general implementation methodology of these tactics, that the readers can adapt to other category theory libraries.

Braibant and Pous [4] presented AAC Tactics [5]: a set of ROCQ tactics for reasoning modulo A (associativity) and AC (associativity and commutativity) optionally with U (units). The major differences between AAC Tactics and this work are threefold:

- Our tactics handle morphisms whose types depend on their source and target objects.

- Our tactics do not consider commutativity but cancellation of inverse elements.

- Our tactics do not support uninterpreted function symbols.

<footnote n="1">¹ In this paper, we use the composition operation ; in diagrammatic order, i.e., $f; g := g \circ f$.</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 1 Modulo AU reasoning by reflection.</figcaption></figure>

In fact, one of our contributions is a straightforward way to handle dependently typed terms
in exchange for commutativity (cf. Contribution 2 below).

**Methodology** As in AAC Tactics, our tactics produce *reflexive proofs* [2], which replaces explicit reasoning steps with computation, e.g., execution of a verified decision procedure [9]. Since the trace of such computation does not appear in the proof term, this approach contributes to reducing the size of proof terms and often has performance advantages.

For the modulo AU tactics, this means that we define the following ingredients as depicted in Figure 1: 1) the type of reified syntax trees (binary trees) representing expressions with the composition and identity, 2) the *interpretation* function $\phi$ from syntax trees to expressions, and 3) the *normalisation* function $\text{norm}$ from syntax trees to its (right-leaning) normal form. Showing that two given morphisms (input) $m_1$ and $m_2$ are equal modulo AU amounts to finding their corresponding syntax trees $e_1$ and $e_2$, applying Proposition 2, and computationally checking the (definitional) equations $m_i = \phi(e_i)$ for $i \in \{1, 2\}$ and $\text{norm}(e_1) = \text{norm}(e_2)$.

► **Proposition 1.** For any syntax tree $e$, $\phi(e) = \text{norm}(e)$.

► **Proposition 2.** For any syntax trees $e_1$ and $e_2$, $\text{norm}(e_1) = \text{norm}(e_2)$ implies $\phi(e_1) = \phi(e_2)$.

**Proof.** This is a trivial consequence of Proposition 1. ▼

<figure><img src="image_5.png" /></figure>

To find the right syntax tree $t$ from the input $m$ automatically, we implement 4) the *reification* procedure (Sections 3 and 4), which is the inverse of the interpretation function. While the interpretation and normalisation functions have to be defined in (the calculus of) ROCQ, the *reification* procedure is a *metafunction* that cannot be defined in ROCQ.

We carried out the metaprogramming part of the work in ROCQ-ELPI [14], that lets us write ROCQ commands and tactics in ELPI. ELPI is a dialect of λProlog, a rule-based logic programming language. ROCQ-ELPI has a few advantages in implementing our rewrite tactics, whose specificity is that they may take an equation with universally quantified variables, e.g., $x$ in the hypothesis $H: \forall x, a; (x; c) = f$. Our rewrite tactics replace these variables with *evars* (*existential variables* or *unification variables*), i.e., unknown terms that can later be instantiated, and then, match the pattern with *evars*, e.g., $a; (?_x; c)$ where $?_x$ denotes an evar, against the term we want to rewrite to find the right instantiation for the *evars*. We leverage two features of ELPI in implementing our reification and matching procedures:

- When asked to reify an evar, our reification procedure *suspends* by declaring a *constraint* on the evar [14, Section 2.3]. The constraint automatically *resumes* when the evar get assigned by matching.

- Our matching procedure uses ELPI's backtracking behaviour [14, Section 2.1] to explore all the solutions in a brute-force manner.
In addition, the matching procedure of our modulo G tactics operates on AU normal forms, and produces the witness, which can be checked by reflection, that they are equal modulo cancellation. This design choice enables us to reuse the components of our modulo AU tactics in implementing our modulo G tactics.

**Contributions** The contributions of this paper are twofold:

1. Our modulo G tactics naturally extend the modulo AU tactics. Its implementation is sufficiently simple (195 LoC of ROCQ and 199 LoC of ELPI) to allow readers to adapt it to other category theory libraries, and also, *typed algebras* [11], *i.e.*, generalisations of some algebraic structures where the elements come with a source and a target.
On the other hand, we do not aim at implementing an extension mechanism, *e.g.*, [4, Section 2] and [9, Section 6.2], that allows users to declare objects to be handled by our tactics.

2. We show a straightforward way to support dependently typed terms (morphisms) in the modulo A(U) and G tactics. In other words, we propose a solution to support one aspect of *heterogeneity* discussed as future work by Braibant and Pous [4, Section 6.2].
Note that our solution relies on the fact that our reified terms do not need to represent variables as identifiers, *e.g.*, indices, since our normalisation procedure does not need to compare variables. Therefore, our solution does not extend to the modulo AC(U) tactics. Nonetheless, we argue that dependently-typed composition-like operators for which our solution is useful are non-commutative at the first place: none of the composition-like operators of typed algebras presented by Pous [11] is commutative, and the commutativity law does not type check for a composition-like operator of type $T_{a,b} \rightarrow T_{b,c} \rightarrow T_{a,c}$.

Thanks to Contribution 1, this paper is written as a tutorial that readers can follow to implement their own modulo AG and G tactics. For this purpose, we recommend the ELPI and ROCQ-ELPI tutorials<fnref n="2" /> as further reading. While our actual tactics targets categories, this paper presents only their simplified versions targeting a *monoids*, *i.e.*, categories with only one object. This makes the type of morphisms (which are now elements of the monoid) simply typed, and simplifies the reification and matching procedures by not carrying around type constraints. While this choice comes with the price of obscuring Contribution 2, we make some remarks on how the simplified version of our tactics can be generalised to the dependently-typed case, and the implementation of our tactics for the Graph Rewriting library is available as the supplementary material for further inspection.

**Outline** The rest of this paper is organised as follows. In Section 2, we define the interfaces for monoids, and their left and/or right invertible elements, using canonical structures [10, 19]. In Section 3, we present our *reflexivity modulo AU* (*areflexivity*) tactic, reified terms for reasoning modulo AU, and the reification procedure with no support for open terms, *i.e.*, terms with evars. In Section 4, we present our rewriting modulo AU (*arewrite*) tactic, an extension of the reification procedure to support open terms, and the matching modulo AU procedure. In Section 5, we present our *reflexivity modulo G* (*aireflexivity*) tactic, a new kind of reified terms for representing insertions and deletions of identity modulo G, *e.g.*, $f; f^{-1}$, $f; g; g^{-1}$; $f^{-1}$, and $f; f^{-1}$; $g; g^{-1}$, and the matching modulo G procedure that explores all the possibilities of skipping an identity modulo G. In Section 6, we present our rewrite modulo G (*airewrite*) tactic, and extend the matching modulo G procedure to support open terms. In Section 7, we conclude the paper.

<footnote n="2">² https://github.com/LPCIC/coq-elpi#tutorials</footnote>
4 Tactics modulo associativity and cancellation for category theory

2 Preliminaries

In this section, we define the interfaces for monoids (Section 2.1), and their left and/or right
invertible elements (Section 2.2). These structures make our tactics applicable to any monoid
instance, and enables the matching procedure to infer inverse elements.

The Graph Rewriting library defines the hierarchies of categories and morphisms [3, Sections 2 and 3] using HIERARCHY BUILDER [6], that compiles high-level description of mathematical structures to packed classes [8]. In this paper, we *neither* use HIERARCHY BUILDER nor packed classes, but we use their underlying inference mechanism called canonical structures [10, 19]. Our rationale is that understanding lower-level implementation details of structures, which HIERARCHY BUILDER rather obscures, is necessary for implementing our tactics, and packed classes are beneficial only when constructing a reasonably large hierarchy with several structures and components involved, which is not the case in our hierarchy.

While it would be feasible to reimplement our tactics for equivalent hierarchies in type
classes [13, 20], it may require a non-trivial adaptation of the reification and matching
procedures, which goes beyond the scope of this paper.

2.1 Monoids

We define the interface for (multiplicative) monoids as follows.

1
    Module MulMonoid.
2
    Structure type :=
3        { sort : Type;
4          one : sort;
5          mul : sort -> sort -> sort;
6          mulA :forall x y z : sort, mul x (mul y z) = mul (mul x y) z;
7          mul1x :forall x : sort, mul one x = x;
8          mulx1 :forall x : sort, mul x one = x; }.
9
End MulMonoid.

The record type<fnref n="3" /> [17] above, called *type*, bundles the components of monoids: the carrier type (*sort*), the operators (*one* and *mul*), and the non-commutative monoid laws (the rest). This definition is surrounded by the *MulMonoid* module [16], that acts as a *namespace*; that is, the names declared inside it are prefixed by the module name, *e.g.*, *MulMonoid.type*, allowing us to reuse the same internal names *type* and *sort* for other structures. Below, we define the shorthands for the names of the record type, operators, and monoid laws:

1 Notation monoidType := MulMonoid.type.
2 Notation one := MulMonoid.one.      Notation mul := MulMonoid.mul.
3 Notation mulA := MulMonoid.mulA.
4 Notation mul1x := MulMonoid.mul1x.  Notation mulx1 := MulMonoid.mulx1.

declare the notations for the monoid operators:

1 Notation "1" := one. Notation "x * y" := (mul x y).

and assume that a variable M always has type monoidType :

1 Implicit Type M : monoidType.

<footnote n="3">³ The `Structure` keyword is a synonym of `Record`. Following the common convention, we use the former to distinguish the record types that are used for automatic instance search by canonical structures.</footnote>
<figure><img src="image_6.png" /><figcaption>Figure 2 The hierarchy of invertible elements of monoids.</figcaption></figure>

Unlike type classes, the carrier type `sort`, from which we infer the monoid instance, appears as a field of `type` rather than its parameter. In order to use a monoid instance `M` of type `monoidType` in a context that expects its carrier type of type `Type`, we declare the `MulMonoid.sort` projection as an implicit coercion [18].

1. `Coercion MulMonoid.sort : monoidType -> Sortclass.`

A monoid instance can be defined as an instance of the `monoidType` record type. In order to use it for automatic instance search by canonical structures, the instance has to be distinguished by the `Canonical` keyword. For example, the canonical monoid instance for lists, i.e., the free monoid, can be declared as follows.

1. `Canonical list_monoidType (T : Type) :=`
2. `{ | MulMonoid.sort := list T; MulMonoid.one := nil; MulMonoid.mul := cat;`
3. `(* Proof of the monoid laws are omitted for brevity. *) |}`.

where `list T` is the type of lists whose elements have type `T`, `nil` is the empty list, and `cat` is the binary concatenation operator for lists. An instance search can be triggered by applying an overloaded monoid operator, e.g., `mul`, to a term of concrete monoid type `T`, or conversely, supplying an overloaded monoid operator in a context that expects a term of type `T`. Type inference of such a term amounts to solving a unification problem of the form `MulMonoid.sort ?_M ≅ T` where ?_M is an evar representing the unknown monoid instance for `T`, to be instantiated. For example, if `T := list U`, the solution is ?_M := `list_monoidType U`, because the head symbol of the `MulMonoid.sort` field of the canonical instance `list_monoidType` is `list`.

## 2.2 Invertible elements

In this section, we define four structures for invertible elements of monoids (Figure 2). Firstly, we define the structure that provides the common notion of inverse, but without the witness that it is actually the inverse. Secondly, we define the two structures of one-sided (left or right) invertible elements, that inherit the definition of inverse from the first structure and add the witness that it is the left or right inverse. Lastly, we define the structure of both-sided (left and right) invertible elements, that inherit the definition of inverse and its properties from the other three structures. In the categorical counterpart [3, Section 2.2], the one-sided invertible elements correspond to split monomorphisms and epimorphisms, and the both-sided invertible elements correspond to isomorphisms.

Given a one-sided (say, left) invertible element, its left inverses are not unique. However, allowing to infer several left inverse elements with canonical structures is a non-trivial task. Therefore, we assume that the inverse of any element can be *canonically* determined if it exists; that is, we can infer at most one inverse element for each element. Our rationale of defining the first structure, that provides the unified notion of inverse for one-sided invertible elements, is that the inverse must be unique if both left and right inverses exist.
**Invertible elements with no witness** We define the structure of invertible elements, but
without the witness that the inferred invertible element is actually the inverse.

1 Module Invertible.

2
3
4
5
6
7

Structure type M : Type := { sort : M; inv : M; }.

End Invertible.

4

5 Notation invertible := Invertible.type.

6 Notation inv := Invertible.inv.

7
Coercion Invertible.sort : invertible --> MulMonoid.sort.

where `sort` and `inv` respectively represent the invertible element and its inverse, and
`invertible` and `inv` are respectively the shorthands for the names of the record type
`Invertible.type` and the inverse constant `Invertible.inv`.

An instance search of the invertible structure can be triggered by a unification problem of the form `Invertible.sort` ?_I ≅ x where ?_I is the unknown invertible instance of the given element x of a monoid.

**Left invertible elements** We define the structure of left invertible elements.

1 Module LInvertible.

2
3
4
5
6
7

Structure type M : Type := { sort : M; inv : M; mulVx : inv * sort = 1; }.

End LInvertible.

4

5 Notation lInvertible := LInvertible.type.

6
Coercion LInvertible.sort : lInvertible --> MulMonoid.sort.

Besides renaming, the only difference from the **invertible** structure above is the addition
of the new field `mulVx` to the **type** record, which says `inv` is the left inverse of **sort**.

To implement the inheritance from `invertible` to `lInvertible`, we define the corresponding subtyping function, as follows.

1 (* In the LInvertible module above *)

2 Definition invertible M (x : type M) :=

3
{
  Invertible.sort := sort x;
  Invertible.inv := inv x
}.

We declare this subtyping function as an implicit coercion from `lInvertible` instances to
`invertible` instances, and declare it as a canonical instance to solve unification problems of
the form `Invertible.sort` ?_I ≅ `LInvertible.sort` x, as follows.

1 Coercion LInvertible.invertible : lInvertible --> invertible.

2

Canonical LInvertible.invertible.

We define the shorthand `mulVx` for `LInvertible.mulVx` as follows. Note that `inv` in the
statement below comes from the **invertible** structure but not the **lInvertible** structure,
and thus, it requires the `LInvertible.invertible` coercion to **typecheck**.

1 Lemma mulVx {M} (x : lInvertible M) : inv x * x = 1.

**Right invertible elements** Symmetrically, we define the structure of right invertible elements.

1 Module RInvertible.

2
3
4
5
6

Structure type M : Type := { sort : M; inv : M; mulxV : sort * inv = 1; }.

Definition invertible M (x : type M) :=

3
{
  Invertible.sort := sort x;
  Invertible.inv := inv x
}.

End RInvertible.
```
6
7 Notation rInvertible := RInvertible.type.
8
9
10
11
12
```

**Both-sided (left and right) invertible elements** We define the structure of left and right invertible elements, which contains all the components of the other three structures of invertible elements. The definitions of three subtyping functions and the declarations that they are implicit coercions and canonical instances, that implement the inheritance from the other three structures, are omitted for brevity.

```
1
2
3
4
5
6
7
8
9
```

## 3 Reflexivity modulo AU

**Reflection** In this section, we implement the reflexivity modulo AU (areflexivity) tactic. To this end, we define our proof-by-reflection setup depicted in Figure 1. We first define reified syntax trees as the following inductive datatype:

```
1
2
3
4
5
6
7
8
9
```

whose three constructors respectively represent the monoid operators `mul` and `one`, and a variable, *i.e.*, any element of the monoid `M`. Any syntax tree can be interpreted and put in its right-leaning normal form respectively by the following functions `ae_eval` and `ae_norm`.

```
1
2
3
4
5
6
7
8
9
10
```

The latter function takes an accumulator `acc` in addition to a syntax tree `e`, and computes the normal form of `ae_eval e * acc`, i.e., `(x1 * (..(xn * acc)..))` given that `e` represents `x1 * .. * xn` modulo AU. Thus, `φ(e)` and `norm(e)` in Section 1 correspond to `ae_eval e` and `ae_norm e 1`, respectively. Then, Propositions 1 and 2 can be proved in ROCQ as the following lemmas.
1 Lemma ae_correct {M} (e : aexpr M) (acc : M) : ae_eval e * acc = ae_norm e acc.

2 Proof. (* By structural induction on e. *) Qed.

3

4 Lemma areflexivity_correct {M} (e1 e2 : aexpr M) :

5 ae_norm e1 1 = ae_norm e2 1 -> ae_eval e1 = ae_eval e2.

Suppose we want to prove a goal (x * y) * z = x * (y * z) for some elements x, y, and z of a monoid M. Thanks to the above reflection lemma, the proof can be done by the following proof term:

1 let e1 := aeMul (aeMul (aeVar x) (aeVar y)) (aeVar z) in

2 let e2 := aeMul (ae_var x) (aeMul (ae_var y) (ae_var z)) in

3 @areflexivity correct M e1 e2 erefl

where e1 and e2 are reified terms of the LHS and RHS, respectively. To type-check this proof term, we use computational reflection twice. Firstly, applying the above term to the given goal requires `ae_eval e1 = ae_eval e2` and the goal to be convertible. Secondly, supplying `eref1`, the reflexivity of the equality `=` as the proof of `ae_norm e1 1 = ae_norm e2 1` requires `ae_norm e1 1` and `ae_norm e2 1` to be convertible.

**Reification** The missing piece for implementing the `areflexivity` tactics is the *reification* procedure that performs the inverse of the interpretation function `ae_eval`. It can be implemented in RocQ-ELPI [14] (Section 1) as follows.

1 `pred quote i:term i:term o:term.`

2 `quote M {{ @one lp:M' }} {{ @ae_one lp:M }} :- coq.unify-eq M M' ok, !.`

3 `quote M {{ @mul lp:M' lp:In1 lp:In2 }} {{ @aeMul lp:M lp:Out1 lp:Out2 }} :-

4 coq.unify-eq M M' ok, !, quote M In1 Out1, quote M In2 Out2.

5 `quote M In {{ @ae_var lp:M lp:In }} :- !.`

Line 1 declares that `quote` is a predicate with three parameters of type `term`, which is the type of RocQ terms embedded in ELPI; in other words, `quote` is a relation between three RocQ terms. These parameters are respectively a monoid `M`, a monoid expression `In` of type `M`, and the reified term `Out` of `In`. Since our objective is to calculate the reified term given the other parameters, we mark the first two parameters as the `input` (`i:`) and the last one as the `output` (`o:`).

The rest of the code gives three rules that specifies the behaviour of `quote`. The syntax `{{ ... }}` is the *quotation* that lets us write RocQ terms embedded in ELPI using the syntax of RocQ, and conversely, `lp:` is the antiquotation that lets us use ELPI syntax in the quoted RocQ terms [14, Section 3.4.1]. The first rule (Line 2) reifies `one` to `ae_one M`. The second rule (Line 3) reifies `mul` to `@ae mul M`, and also, recursively reifies the arguments `In1` and `In2` of `mul` to `Out1` to `Out2`, respectively, by calling `quote` itself. The last rule (Line 5) handles the variables by reifying the other terms to `@ae_var M`.

The first two rules follow the *reification by small-scale reflection* approach [12, Section 3.2]; that is, we compare the two monoid instances `M` and `M'`, respectively given as the first argument of `quote` and the implicit argument of the monoid operator (`one` or `mul`), by conversion. The conversion checking is done by calling the unification API of RocQ (`coq.unify-eq`). This approach allows us to rule out the case where `M` and `M'` are not the same monoid, while supporting the case where they are syntactically unequal but still convertible. Such monoid instances may exist in the presence of structures that inherit from monoids, e.g., groups and rings [1]. The case where `M` and `M'` are inconvertible are handled by the last rule thanks to the backtracking.
Backtracking in ELPI can be controlled by the cut operator (!), that commits to the currently chosen rule by discarding the other rules. In the first two rules, the cut is placed after `coq.unify-eq` since we want to backtrack when the conversion fails; that is, this conversion is considered to be a part of the pattern matching. Thanks to the cut operator, `quote` is deterministic; that is, it returns at most one solution for each invocation. Replacing Line 1 with the following signature instructs the determinacy checker [7] to check this property.

1. `func quote term, term -> term.`

**The tactic** The `areflexivity` tactic can be implemented as the following rule of the `solve` predicate, which is the entry point for tactics in ROCQ-ELPI.

1. `solve (goal _ _ Type _ _ as G) [] :- !,`
2. `coq.unify-eq Type {{ @eq (MulMonoid.sort lp:M) lp:LHS lp:RHS }} ok,`
3. `quote M LHS LHSQ, quote M RHS RHSQ,`
4. `refine {{ @areflexivity correct lp:M lp:LHSQ lp:RHSQ erefl }} G [].`

where `solve G GS` means that the tactic takes a goal `G` and returns a list of subgoals `GS`. We use the empty list `[]` as `GS` since our tactic should not leave any subgoal, i.e., either completely solve the given goal `G` or fail. Line 2 asserts that the goal is an equation over monoid. It does so by unifying the goal with `@eq (MulMonoid.sort ?_M) ?_LHS ?_RHS`. Line 3 reifies the `LHS` and `RHS` to `LHSQ` and `RHSQ`, respectively. Line 4 attempts to close the goal `G` using the proof term `areflexivity correct M LHSQ RHSQ erefl`.

**Dependently-typed case** In order to generalise the `areflexivity` tactic to morphisms in a category, `aexpr` should be defined as an inductive family that takes the source and target objects as parameters. Its interpretation and normalisation procedures, and the lemmas should be adapted accordingly. The adaptation of `ae_norm` to such a datatype requires the *convoy pattern* to typecheck; that is, the `match` expression should return a function that takes `acc`. In this case, our `quote` predicate takes the source and target objects of the input `In`, since we need them for constructing the output `Out`, and we avoid inferring them from the input for performance reasons.

# 4 Rewriting modulo AU

In this section, we implement the rewriting modulo AU (`arewrite`) tactic, which behaves as follows:

1. It takes a subterm `e` of the goal and a proof of an equation `lhs = rhs`. While `e` must be a ground term, the equation may be universally quantified and may include side conditions.

2. It instantiates the quantifiers and side conditions of the given proof with `evars`.

3. It finds `pre` and `post` such that `pre *lhs* *post` is equal to `e`; that is, it matches the pattern `?pre *lhs* *?post` against `e` modulo AU.

4. It rewrites `e` in the goal to `pre *rhs* *post`.

While we reuse our proof-by-reflection setup (Section 3), we introduce a new reflection lemma:

1. Lemma `arewrite correct {M} (elhs : aexpr M) (rhs : M):`
2. `ae_norm e 1 = ae_norm lhs 1 -> ae_eval rhs = rhs -> ae_eval e = rhs.`

where `lhs` and `rhs` are already expanded with `pre` and `post`. While the first hypothesis (`ae_norm e 1 = ae_norm lhs 1`) should be proved by reflection, the second one (`ae_eval lhs = rhs`) corresponds to the equation supplied by the user.

In the rest of this section, we adapt the `quote` predicate to rewriting modulo AU and implement the matching modulo AU procedure.
**Reification** The adaptation of the `quote` predicate is twofold:

- adding the support for open terms, i.e., the presence of evars in the input, and

- flattening the input into a list-like structure, which we call *paths*, to be used by the matching procedure.

We first define paths as a datatype in ELPI as follows:

1. `kind path type.`

2. `type nilp path.`

3. `type consp term -> path -> path.`

4. `type catp path -> path -> path.`

where `path` is the name of the datatype, `nilp` is the constructor representing `one`, `consp` is the constructor representing a multiplication (`mul`) of a variable and a path, and `catp` is another constructor representing a multiplication, but whose LHS must be an evar.

We modify the `quote` predicate to produce the path as follows:

1. `func quote term, term -> term, path.`

2. `quote M In Out (OutP nilp) :- !, quote-rec M In Out OutP.`

3.

4. `func quote-rec term, term -> term, (path -> path).`

5. `quote-rec M {{ @one lp:M' }} {{ @ae_one lp:M }} (p\ p) :- coq.unify-eq M M' ok, !.

6. `quote-rec M {{ @mul lp:M' lp:In1 lp:In2 }}

7. `{{ @aeMul lp:M lp:Out1 lp:Out2 }} (p\ OutP1 (OutP2 p)) :-

8. `coq.unify-eq M M' ok, !, quote-rec M In1 Out1 OutP1, quote-rec M In2 Out2 OutP2.`

9. `quote-rec M In {{ @ae_var lp:M lp:In }} (consp In).`

where the syntax `(x\ e)` represents a function, i.e., $(\lambda x.e)$. To avoid linear-time concatenation of paths, the `quote-rec` predicate produces a path in the form of *difference lists*, i.e., a function of type `path -> path` that prepends the path it represents to the given path.

We further extend the `quote-rec` predicate to support open terms, by adding the rule below as the first rule of `quote-rec`:

1. `quote-rec M In Out (catp OutP) :-`

2. `var In, !, declare_constraint (path.quote M OutP In Out) OutP.`

where `var In` asserts that `In` is a unification variable, i.e., representing an evar in ROCQ. In this case, we suspend the reification process: `declare_constraint C V` declares the constraint `C` on the unification variable `V`, which means that `C` resumes upon the assignment of `V`. Note that we declare the constraint not on the input `In`, but on the path `OutP`. This is because our matching procedure operates on paths and instantiates unification variables in them, and we need to change the roles of input and output here. The constraint `path.quote M OutP In Out`, defined below, is a version of the reification procedure that takes the path `OutP` as the input and produces the input and the reified term.

1. `func path.quote term, path -> term, term.`

2. `path.quote M P Out OutQ :- var P, !, declare_constraint (path.quote M P Out OutQ) P.`

3. `path.quote M nilp {{ @one lp:M }} {{ @ae_one lp:M }} :- !.

4. `path.quote M (consp _ P' as P) Out OutQ :-`

5. `var P', !, declare_constraint (path.quote M P Out OutQ) P'.`

6. `path.quote M (consp X nilp) X {{ @ae_var lp:M lp:X }} :- !.

7. `path.quote M (consp X P)`

8. `{{ @mul lp:M lp:X lp:Out }} {{ @ae_cons lp:M lp:X lp:OutQ }} :-`

9. `path.quote M P Out OutQ.`

The `path.quote` predicate does not need to support `catp` since our matching procedure does not produce it, and can suspend and resume again when the given path is either a unification variable or `consp X P` where `P` is a unification variable.
**Matching** We define our matching procedure as follows:

1. `pred path.match i: path, o: path.`

2. `path.match nilp nilp :- !.`

3. `path.match (consp X P) (consp X' P') :- !, coq.unify-eq X X' ok, path.match P P'.`

4. `path.match P (catp P1' Pr') :- path.split P P1 Pr, P1' = P1, path.match Pr Pr'.`

where `path.match P P'` matches the path (pattern) `P'` against the path `P`, and only `P'` may contain evars. The first two rules handle `nilp` and `consp` in a pointwise manner. The last rule handles the case where `P'` is `catp P1' Pr'` for some evar `P1'`. It proceeds by splitting `P` into a left part `P1` and the rest `Pr`, instantiating `P1'` with `P1` (thus resuming the constraint declared on `P1'`), and matching `Pr'` against `Pr`. The splitting procedure `path.split` is defined as follows:

1. `pred path.split i: path, o: path, o: path.`

2. `path.split P nilp P.`

3. `path.split (consp X P) (consp X P1) Pr :- path.split P P1 Pr.`

Note that these predicates relies on backtracking and are nondeterministic: `path.split` returns all the solutions from left to right in terms of the point that splits the given path, and `path.match` explores all the possibilities of instantiating evars.

**Dependently-typed case** As we described in Section 3, we need to carry around some source and target objects of the morphisms we handle in the dependently-typed case. For example, we chose to add the object in the middle of the composition to the `consp` and `catp` constructors, and extend the `quote`, `quote-rec`, and `path.quote` predicates with the source and target objects of their input. Most notably, the second rule of `path.match` should split the path `P` at the target object of `P1'`, and thus, we extended `path.split` with the object that splits the given path. This change prunes the search space of the matching.

In addition, the Graph Rewriting library generalises the morphism equality from Leibniz equality (eq) to setoid equalities [3, Section 2.1]. Nevertheless, adapting our tactics to setoid equalities is just a matter of adapting our reflection lemmas and discharging the task of inferring a setoid morphism to the standard `setoid_rewrite` tactic.

# 5 Reflexivity modulo G

In this section, we implement the *reflexivity modulo G* (aireflexivity) tactic. Firstly, we implement another layer of reflection that deals only with cancellation, to be combined with the reflection setup from Section 3. This separation between associativity and cancellation allows us to use the reification procedure from Sections 3 and 4 as is. Secondly, we implement a matching modulo G procedure, which we extend to support open terms in Section 6.

**Reflection** We argue that reasoning modulo cancellation amounts to inserting and deleting sequences described by `I` in the following grammar:

$$I := x I^* x^{-1} \qquad (x \text{ is right invertible, i.e., } x \times x^{-1} = 1)$$

$$I^* := 1 | II^* \qquad (\text{The Kleene star on } I)$$

and such insertions and deletions can always be done with no overlap. We define the reified syntax for `I` as a version of rose trees:

1. `Inductive iexpr M : Type := can_inv : rInvertible M -> list (iexpr M) -> iexpr M.`
```hkl
1 func skip-one term, path -> path, term.
2 skip-one M (consp X P) P' {{ @can_inv lp:M lp:Ri lp:Out }} :- !,
3 rinv->linv M X Ri XV, !, % check if X is right invertible
4 skip-ones M P (consp XV' P') OutL, % skip I*
5 coq.unify-eq XV XV' ok, % check if XV' is the inverse of X
6 !, % commit to the first solution
7 mkrocqlist {{ @iexpr lp:M }} OutL Out. % turns a list in ELPI into a list in ROCQ
8
9 pred skip-ones i:term, i:/path, o:/path, o:/list term.
10 skip-ones _ P P [].
11 skip-ones M P P2 [Out1|Out2] :- skip-one M P P1 Out1, !, skip-ones M P1 P2 Out2.
```

Note that `skip-ones` uses backtracking to enumerate the solutions from shorter ones to longer ones, i.e., $I^0$, $I$, $I^2$, and so on. A path may have several prefixes of the form $I$; for example, both $(x(x^{-1}x)x^{-1})$ and its prefix $(xx^{-1})$, where $x^{-1}$ is the both-sided inverse of $x$, are of the form $I$. Given such a path, `skip-one` commits to the first (shortest) solution using the cut operator `!`. This avoids duplicated or missing solutions in the enumeration by `skip-ones` because, if a path has several prefixes of the form $I$, such an ambiguity is always introduced by the presence of a both-sided inverse, and we can always reach to later solutions by repetitively taking the shortest prefix, e.g., $(xx^{-1})(xx^{-1})$.

Lastly, we implement the matching modulo $G$ procedure as two predicates `path.match` and `path.match'`. Both of them take four parameters $M, P, Q$, and `Out`, attempt to match the two paths $P$ and $Q$, and produce the witness `Out` of type `cexpr M` that $P$ and $Q$ are equal modulo cancellation. The former skips a prefix of the form $I^*$ of each path, the latter skip the first item of each path given that they are the same, and they call each other to match the rest of the paths. Therefore, we define them via mutual recursion as follows:

```hkl
1 pred path.match i:term, i:/path, i:/path, o:term.
2 path.match M P Q Out'' :-
3 skip-ones M P P' OutP,
4 skip-ones M Q Q' OutQ,
5 path.match' M P' Q' Out,
6 iexprs->cexpr M {{ false }} OutP Out Out',
7 iexprs->cexpr M {{ true }} OutQ Out' Out''.
8
9 pred path.match' i:term, i:/path, i:/path, o:term.
10 path.match' M nilp nilp {{ @ce_one lp:M }} :- !.
11 path.match' M (consp X P) (consp X' Q) {{ @ce_cons lp:M lp:X lp:Out }} :- !,
12 coq.unify-eq X X' ok, path.match M P Q Out.
```

where `iexprs->cexpr M F IES CE Out` prepends a list `IES` of terms of type `iexpr M` to a term `CE` of type `cexpr M` by the constructor `ce icons F`.

# 6 Rewriting modulo G

In this section, we implement the rewriting modulo $G$ (airewrite) tactic. We first introduce the following reflection lemma:

```hkl
1 Lemma airewrite correct {M} (elhs : aexpr M) (rhs : M) (ce : cexpr M) :
2 ae_norm e 1 = ce_eval false ce 1 -> ce_eval true ce 1 = ae_norm lhsm 1 ->
3 ae_eval lhsm = rhs -> ae_eval e = rhs.
```

where `e` represents the subterm of the goal to be rewritten, `lhs` and `rhs` represent the LHS and RHS of the equation expanded with `pre` and `post` (Section 4), and `ce` is the witness that `e` and `lhs` are equal modulo $G$.
**Matching** In the rest of this section, we extend the matching modulo G procedure (Section 5) with the support for open terms. Firstly, we modify the **skip-one** and **skip-ones** predicates, which respectively finds a prefix of the form *I* and *I*\* of the given path, as follows:

1. `pred skip-one i:term, o, o, o:term.`
2. `skip-one M (consp X P) P'' {{ @can_inv lp:M lp:Ri lp:Out }} :- !,`
3. `rinv->linv M X Ri XV, !,`
4. `skip-ones M P P' OutL,`
5. `((P' = consp XV P'', !, coq.unify-eq XV XV' ok);`
6. `(P' = catp (consp XV Pl) Pr, !, P'' = catp Pl Pr)),`
7. `!`,
8. `mkrocclist {{ @iexpr lp:M }} OutL Out.`
9.
10. `pred skip-ones i:term, o=path, o:term, o:list term.`
11. `% The rules of skip-ones remain unchanged, and are omitted for brevity.`

where `;` is the disjunction operator: `P; Q` first attempts `P` and then `Q`. The changes from Section 5 are twofold:

- These predicates may now instantiate the given path, i.e., their second argument, where unification variables always appear as the first argument of `catp`. Therefore, these parameters are marked as output (`o:`), and `skip-one` is not deterministic anymore.

- In the rule of **skip-one**, if the path `P'` (the output of **skip-ones**) starts with a unification variable, we close the “open parenthesis”, i.e., the right invertible element `X`, by instantiating the head of the unification variable with its inverse `XV`. Since **skip-one** recursively calls itself, it can recursively close several open parentheses; that is, it can split a path of the form `x₁I* ... xnI*?P`, where `xn₁, ..., xn` are right invertible, into `x₁I* ... xnI*xn⁻¹ ... x₁⁻¹` and the rest, by instantiating `?P` with `xₙ⁻¹ ... x₁⁻¹?P`.

Note that our solution is not the only way of “closing the parentheses” since we may find a part of `xₙ⁻¹...x₁⁻¹` after the unification variable. For example, `xy?P x⁻¹` is of the form *I* if we instantiate `?P` with `g⁻¹`. Nevertheless, we argue that it is safe to immediately close the parentheses, i.e., instantiate `?P` with `y⁻¹ x⁻¹?P`, since we can then open the parentheses again, i.e., instantiate `?P`, with `x`. To sum up, our solution to the above example `xy?P x⁻¹` is to instantiate `?P` with `y⁻¹ x⁻¹ x`, which results in `(xy y⁻¹ x⁻¹)(xx⁻¹)`. However, our solution may not work if the unification variable `?P` appear more than once in the path. We intentionally leave such cases *unsupported*, since multiple occurrences of the same unification variable correspond to a cycle in a diagram, which are uncommon in typical categorical reasoning.

Secondly, we modify the matching modulo G procedure, the `path.match` and `path.match'` predicates. We change their signatures, for the same reason as above:

1. `pred path.match i:term, i path, o path, o:term.`
2. `pred path.match' i:term, i path, o path, o:term.`

While their rules remain unchanged from Section 5, we add the following new rule of `path.match':`

1. `path.match' M P (catp QVar Q) Out'' :-`
2. `skip-one_catp M Q [] Qr QlV QlW,`
3. `path.split P Pl Pr,`
4. `path.cat Pl QlV QVar,`
5. `path.match M Pr Qr Out,`
6. `iexprs->cexpr M {{ true }} QlW Out Out',`
7. `path->cexpr M Pl Out' Out''.`
This rule matches a pattern `catp QVar Q`, where `QVar` is a unification variable, against a path `P`. It consists of the following two steps:

- The `skip-one_catp` predicate performs the dual operation of “closing the parentheses”; that is, it splits the given path `Q` into a prefix of the form $I^* x_1 \dots I^* x_n$ and the rest `Qr`, where $x_1, \dots, x_n$ are left invertible. It also produces a path `Q1V`, which is $x_n^{-1} \dots x_1^{-1}$, and a witness `Q1W` that the concatenation of `Q1V` and the prefix, i.e., $x_n^{-1} \dots x_1^{-1} I^* x_1 \dots I^* x_n$, is of the form $I^*$.

Note that the only case where this sequence is *not* of the form `I` is when the prefix is empty. Therefore, the witness `Q1W` is *not* a term of type `iexpr M`, but a list of terms of type `iexpr M`, which is either empty or singleton.

- As in the matching modulo AU procedure (Section 4), `path.split` splits `P` into `P1` and `Pr`. We then instantiate the unification variable `QVar` with the concatenation of `P1` and `Q1V`, obtained by `path.cat`, and match the rest of the pattern `Qr` against `Pr`.

Again, backtracking is at the core of the matching procedure: both `skip-one_catp` and `path.split` explore all the solutions, from left to right in terms of the point that splits the given path. To build the witness, the `path->cexpr` predicate prepends the path `P1` to the witness of type `cexpr M`.

Lastly, the `skip-one_catp` predicate is defined as follows:

1. `pred skip-one_catp i:term, i:path, i:list term, o:path, o:path, o:list term.`
2. `skip-one_catp _ P Acc P nilp Acc.`
3. `skip-one_catp M P Acc Q (consp EV PV) Acc'''' :-`
4. `skip-ones M P (consp E P') Acc',`
5. `linv->rinv M E Ri EV,`
6. `std.append Acc Acc' Acc'', % appends two lists Acc and Acc' into Acc''`
7. `mkrocqlist {{ @iexpr lp:M }} Acc'' Acc''',`
8. `skip-one_catp M P' [{@ @can_inv lp:M lp:Ri lp:Acc'''}] Q PV Acc''''.`

where `linv->rinv` performs the dual of `rinv->linv`; that is, it takes a left invertible element `E`, and returns its inverse `EV` and a right invertible instance `Ri` on `EV`.

## 7 Conclusion

We presented tactics for equational reasoning modulo AU (associativity and unit) and G (AU and inverse) in ROCQ. We implemented two versions of the tactics, and both of them are available in the supplementary material: 1) simply-typed versions presented in the paper, and 2) dependently-typed versions for category theory, built on top of the Graph Rewriting library [3]. The dependently-typed versions of the tactics consist of 195 LoC of ROCQ and 199 LoC of ELPI, excluding the code from the Graph Rewriting library. We argue that the implementation of our tactics is sufficiently simple to allow readers to adapt it to other category theory libraries. Moreover, the present work illustrates a broader shift in ITP, that the development of advanced automation tools, which used to require expert knowledge, e.g., writing a ROCQ plugin in OCAML, is now a lot more accessible to end users thanks to recent technologies, e.g., ROCQ-ELPI. This is one of the reasons why we chose not to provide an extension mechanism for declaring objects to be handled by our tactics, e.g., [4, Section 2] and [9, Section 6.2].

We believe that the following factors largely contributed to the simplicity and conciseness of the implementation of our tactics:

**Avoiding identifiers and variable maps**

Typical reflexive tactics, e.g., [4, 9], use reified syntax trees whose leaves are replaced by identifiers that the proof procedure can compare.
Interpreting such syntax trees requires a so-called *variable map*, that maps identifiers to their corresponding term. The presence of these identifiers and variable maps make handling of heterogeneous, *e.g.*, dependently-typed, syntax trees cumbersome. Therefore, it was crucial to observe that we can perform modulo AU and G reasoning without them.

**The modular design of the proof-by-reflection setup** Our modulo G tactics (Sections 5 and 6) use proof by reflection twice: once for modulo AU reasoning, and once more for modulo cancellation reasoning, of which the former is shared with our modulo AU tactics (Sections 3 and 4). While our approach may have a slight performance disadvantage over designing a reified syntax that deals with modulo G reasoning at once, our approach allowed us to reuse the concept of paths and the reification procedure (Section 4) in the implementation of the modulo G tactics, and thus, enabled us to *gradually* develop our tactics, from modulo AU to modulo G, and from *reflexivity* to *rewrite*.

**The use of Rocq-Elpi** The rule-based nature of ELPI provide a natural and concise way of transforming syntax trees to another form. Quotation and antiquotation (Section 3) allowed us to write ROCQ terms in ELPI code using the ROCQ syntax. The *declare_constraint* predicate (Section 4) enabled us to reify terms with holes and delay the reification of holes. Backtracking, optionally controlled with the cut operator (!), provides a concise way of enumerating the solution of matching modulo AU and G, with neither duplication nor overlap.

Note that the first two factors were hinted by Sakaguchi [12]. He introduced a reflexive *preprocessor* for the *ring* and *field* tactics [9], that eliminates heterogeneity introduced by morphism applications before the application of the proof procedure. His reflexive preprocessor deals with a heterogeneous syntax, and does not require identifiers and variable maps.

**Related work** AAC Tactics [4, 5] are ROCQ tactics for reasoning modulo A/AC, optionally with U (units), which consist of about 1,400 lines of ROCQ and 3,600 lines of OCAML. Therefore, the implementation of our tactics is about 12 times more concise than that of AAC Tactics, although the comparison is not entirely fair because of the implementation language, and also because AAC Tactics have several features we did not implement: modulo AC reasoning, the support for uninterpreted function symbols, extensibility, a reification procedure optimised with memoisation, etc.

**Future work** We could extend our tactics with more equational laws, such as *functoriality* and *naturality*, to support more advanced categorical reasoning in an automated way. While dealing with functoriality by reflection is certainly possible by reusing the preprocessing technique [12], extending the matching procedure to support functoriality appear to be a non-trivial task.

To better understand the advantages and disadvantages brought by ROCQ-ELPI, we could reimplement the plugin part of AAC Tactics in ROCQ-ELPI. Then, we could also extend them with the support for heterogeneity [4, Section 6.2] and subsume both AAC Tactics and the present work.

**Acknowledgments** This work was partially funded by the ANR project CoREACT: Coq-based Rewriting: towards Executable Applied Category Theory (ANR-22-CE48-0015).
References

1 Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: a case study in functional analysis. In Proc. of the 10th International Joint Conference on Automated Reasoning (IJCAR '20), volume 12167 of LNCS, pages 3–20. Springer, 2020. doi:10.1007/978-3-030-51054-1_1.

2 Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William E. Aitken. The semantics of reflected proof. In Proc. of the 5th Annual Symposium on Logic in Computer Science (LICS '90), pages 95–105. IEEE, 1990. doi:10.1109/LICS.1990.113737.

3 Samuel Arsac, Russ Harmer, and Damien Pous. Adhesive category theory for graph rewriting in Rocq. In Proc. of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '26), pages 59–74. ACM, 2026. doi:10.1145/3779031.3779105.

4 Thomas Braibant and Damien Pous. Tactics for reasoning modulo AC in Coq. In Proc. of the 1st International Conference on Certified Programs and Proofs (CPP '11), volume 7086 of LNCS, pages 167–182. Springer, 2011. doi:10.1007/978-3-642-25379-9_14.

5 Thomas Braibant, Damien Pous, and Fabian Kunze. AAC tactics, 2010-. Latest release: 9.0.0 (2025-10-28). URL: https://github.com/rocq-community/aac-tactics.

6 Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In Proc. of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD '20), volume 167 of LIPIcs, pages 34:1–34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.FSCD.2020.34.

7 Davide Fissore and Enrico Tassi. Determinacy checking for Elpi: an higher-order logic programming language with cut. In Proc. of the 28th International Symposium on Practical Aspects of Declarative Languages (PADL '26), volume 16401 of LNCS, pages 77–95. Springer, 2026. doi:10.1007/978-3-032-15981-6_5.

8 François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In Proc. of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09), volume 5674 of LNCS, pages 327–342. Springer, 2009. doi:10.1007/978-3-642-03359-9_23.

9 Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. In Proc. of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '05), volume 3603 of LNCS, pages 98–113. Springer, 2005. doi:10.1007/11541868_7.

10 Assia Mahboubi and Enrico Tassi. Canonical structures for the working Coq user. In Proc. of the 4th International Conference on Interactive Theorem Proving (ITP '13), volume 7998 of LNCS, pages 19–34. Springer, 2013. doi:10.1007/978-3-642-39634-2_5.

11 Damien Pous. Untyping typed algebras and colouring cyclic linear logic. Log. Methods Comput. Sci., 8(2), 2012. doi:10.2168/LMCS-8(2:13)2012.

12 Kazuhiko Sakaguchi. Reflexive tactics for algebra, revisited. In Proc. of the 13th International Conference on Interactive Theorem Proving (ITP '22), volume 237 of LIPIcs, pages 29:1–29:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.ITP.2022.29.

13 Matthieu Sozeau and Nicolas Oury. First-class type classes. In Proc. of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs '08), volume 5170 of LNCS, pages 278–293. Springer, 2008. doi:10.1007/978-3-540-71067-7_23.

14 Enrico Tassi. Elpi: rule-based extension language. Habilitation à diriger des recherches, Université Côte d'Azur, 2026. URL: https://www-sop.inria.fr/members/Enrico.Tassi/hdr/hdr.pdf.

15 The Rocq Development Team. The Rocq Reference Manual, 2025. the PDF version with numbered sections is available at https://github.com/coq/coq/releases/tag/V9.1.0. URL: https://rocq-prover.org/doc/V9.1.0/refman/.

16 The Rocq Development Team. Section 2.1.12 "The Module System". In [15], 2025. URL: https://rocq-prover.org/doc/V9.1.0/refman/language/core/modules.html.
18

Tactics modulo associativity and cancellation for category theory

17 The Rocq Development Team. *Section 2.1.8 “Record types”*. In [15], 2025. URL: https://rocq-prover.org/doc/V9.1.0/refman/language/core/records.html.

18 The Rocq Development Team. *Section 2.2.6 “Implicit Coercions”*. In [15], 2025. URL: https://rocq-prover.org/doc/V9.1.0/refman/addendum/implicit-coercions.html.

19 The Rocq Development Team. *Section 2.2.8 “Canonical Structures”*. In [15], 2025. URL: https://rocq-prover.org/doc/V9.1.0/refman/language/extensions/canonical.html.

20 The Rocq Development Team. *Section 2.2.9 “Typeclasses”*. In [15], 2025. URL: https://rocq-prover.org/doc/V9.1.0/refman/addendum/type-classes.html.