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.
At present, there are 3 such modules, two of which (
CommutativeandIdempotentCommutative) are not yet superseded by counterparts underTactic.*Solver(onlyMonoidhas 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:
FreeMonoidconstructionRelation.Binary.Reflection, exportingsolveprove, parametrised on a suitable APINormalfor normal formsThe three individual modules would then reduce entirely to their construction of a suitable implementation of the
NormalAPI, together with appropriatepublicre-export ofsolveandprovefrom the (instantiated) generic constructions.NB.
Tactic.MonoidSolveralso contains an implementation (a different one! the 'functorial' version of variables, rather than theFin-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 ofFreeMonoid(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
Normalforms (parameterised by aRawMonoid M):normalisefunction can be expressed generically, given arawMonoidstructure onNormalforms, together with an interpretation ofvarcorrectfunction can be expressed generically, given aMonoidHomomorphismfromNormaltoM, together with the 'obvious' correctness/coherence condition on (the interpretation of)var, on the assumption thatMadmitsIsMonoid(ieMis actually aMonoid)proveetc. can be folded in on top of the above two definable operations.