At present, there are 3 such modules, two of which (Commutative and IdempotentCommutative) are not yet superseded by counterparts under Tactic.*Solver (only Monoid has been reimplemented).

There is a huge amount of duplicated code between the three, which could/should be refactored into a common core, basically consisting of:

• a FreeMonoid construction
• the existing generic solver based on Relation.Binary.Reflection, exporting solve
• a 'Tactic' module, exporting prove, parametrised on a suitable API Normal for normal forms

The three individual modules would then reduce entirely to their construction of a suitable implementation of the Normal API, together with appropriate public re-export of solve and prove from the (instantiated) generic constructions.

NB. Tactic.MonoidSolver also contains an implementation (a different one! the 'functorial' version of variables, rather than the Fin-based one) of the free monoid, together with its semantics via the Cayley construction, so downstream there would/should be ample opportunity to refactor that as well... at such time as we have a common implementation of FreeMonoid (cf. #1962 ) on which we can agree.

UPDATED: indeed, further downstream refactoring would be possible (see discussion here or else #2457 ). Once you have a suitable API of Normal forms (parameterised by a RawMonoid M):

• the normalise function can be expressed generically, given a rawMonoid structure on Normal forms, together with an interpretation of var
• the correct function can be expressed generically, given a MonoidHomomorphism from Normal to M, together with the 'obvious' correctness/coherence condition on (the interpretation of) var, on the assumption that M admits IsMonoid (ie M is actually a Monoid)
• at which point, all the additional existing machinery involving prove etc. can be folded in on top of the above two definable operations.