Add ring solver#39
Conversation
Extracts the structure-independent parts of the ring solver (atom collection, two-pass polynomial-AST conversion, deadlock detection, auto-quantification, reflection plumbing) into a new generic core `Tactic.Solver.Algebra`, parameterised by a `Theory` record that describes a particular algebraic structure. The ring solver is now an instantiation of this core for `CommutativeSemiring` against stdlib's `Algebra.Solver.Ring.NaturalCoefficients.Default`.
Adds a `CommutativeRing` side to `solve-≈`, alongside the existing `CommutativeSemiring` support. This comes at no extra cost at the call site, and we automatically detect what ring is being used.
I dislike this fix, but I can't think of anything better right now
omelkonian
left a comment
omelkonian
left a comment
There was a problem hiding this comment.
Nice one!
If I understood correctly, this is a convenient wrapper around stdlib's ring solver, doing a better job than the stdlib solve-∀, right?
As a future improvement, would it make sense to automatically discover the commRing instance / record that solve-≈ now takes explicitly?
|
Yes, it's purely a frontend. I'm not sure automatic discovery is possible (at least consistently). The difficult thing that this frontend does is discovering exactly what to reduce in the goal expression. And for this, the instance is an input. I think it might be possible in certain scenarios, but e.g. if you want to solve equations over So all in all I think it's a moderate effort with uncertain success and a relatively minor benefit if it works out. For now I think there are better things to work on. |
2 participants
Adds a practical ring solver based on the machinery on the standard library. The focus here is on something that one should expect to work by default - to that end, there's over 100 tests on various abstract & concrete scenarios. There is a documented limitation (it doesn't help solving metas) but other than that I'm not aware of any cases where you should expect a ring solver to work but this one doesn't.
There's also a comparison with reflective ring solvers that are part of the standard library in
Tactic.Solver.Ring.Tests.Comparison, demonstrating the various issues and that they are fixed with this solver.There is a lot of infrastructure here that should be generically usable for other solvers - currently it is used to deal with both commutative rings and commutative semirings automagically.