Commutative Monoid Solver

[TOTBWF]

trafficstars

When doing stuff with integers, it's pretty common to see some really gnarly goals involving nats. For instance, this monster comes up when you try to define integer multiplication

a * x + b * y + (y + a * y + (x + b * x)) ≡ a * y + b * x + (x + a * x + (y + b * y))

A simple commutative monoid solver would make quick work of this, so it would be a nice-to-have.

Design

The basic idea is to reflect expressions in some monoid into the following data type:

data Expr : Type ℓ where
  ε   : Expr
  _⊗_ : Expr → Expr → Expr
  [_↑] : M → Expr

Then, we can do a sort of NbE style proof where we interpret this into some semantic domain. In our case, this will be sorted lists. Then, we shall define a sort of "readback" function that takes a sorted list and reflects it back into Expr.

However, this poses some problems! In particular, we will need a notion of decidable ordering on M, which is no good. However, we can circumvent this by using an ordering on Term! This requires quite a bit of machinery though, so it is probably best to split the work across several PRs.

[plt-amy]

Progress update: We have a (commutative semi?)ring solver for Nat (Data.Nat.Solver). Need to generalise to arbitrary commutative rings

[TOTBWF]

We can also use the variable machinery to define solvers for commutative monoids/groups pretty easily.

[TOTBWF]

The abelian group one is pretty much mandatory for abelian categories IMO

[plt-amy]

Gonna close this as superceded by the nat and ring solvers