Use `Reflection` to build user friendly interfaces for the solvers

[gallais]

Cf. https://github.com/wjzz/Agda-reflection-for-semiring-solver for inspiration

[MatthewDaggitt]

Wow, that would be neat! I would actually use the solvers then...

[oisdk]

I actually have a preliminary implementation of this (as part of a larger project on a ring solver that I've been working on for a couple months now). It works a little differently to the linked implementation (it uses Relation.Binary.Reflection, for instance), and it works with arbitrary types (i.e. it doesn't have to be able to match on the carrier type, so we don't have to write logic like this for every type we want to use the solver with).

It's still in the preliminary stages, but I've gotten it to the stage where the following (as well as any other examples I could think of) works:

{-# OPTIONS --without-K #-}

module Polynomials.Ring.Nat.Examples where

open import Polynomials.Ring.Simple.AlmostCommutativeRing
open import Polynomials.Ring.Simple.Reflection
open import Agda.Builtin.FromNat
open Number {{...}} public

open import Data.Nat as ℕ using (ℕ)
import Data.Nat.Literals
open import Data.Integer as ℤ using (ℤ)
import Data.Integer.Literals

instance
  NatLit : Number ℕ
  NatLit = Data.Nat.Literals.number

instance
  IntLit : Number ℤ
  IntLit = Data.Integer.Literals.number

module Nat where
  open import Data.Nat.Properties

  NatRing : AlmostCommutativeRing _ _
  NatRing = fromCommutativeSemiring *-+-commutativeSemiring ℕ._≟_

  open AlmostCommutativeRing NatRing

  lemma₁ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + x + y
  lemma₁ = solve NatRing

  lemma₂ : ∀ x y z → x * y + z ≈ z + y * x
  lemma₂ = solve NatRing

module Int where
  open import Data.Integer.Properties

  IntRing : AlmostCommutativeRing _ _
  IntRing = fromCommutativeRing +-*-commutativeRing ℤ._≟_

  open AlmostCommutativeRing IntRing

  lemma₃ : ∀ x → x + - x ≈ 0
  lemma₃ = solve IntRing

  lemma₄ : ∀ x y → y + y * - 1 ≈ (x + x) + - (x * 2)
  lemma₄ = solve IntRing

As I say, it's not yet finished, but I can put a pull request together in the coming weeks if people think it might be useful.

[gallais]

Nice!

as well as any other examples I could think of

Does it work if the variables are introduced on the LHS rather than quantified universally?

A potentially tricky use case: when the solver should treat an expression as if it were a
variable e.g. m ^ n * 1 ≈ m ^ n.

I suppose it could be defined as an auxiliary tactics e.g. opaque (m ^ n) prf where
prf has the same type as the goal except that all occurences of m ^ n have been
replaced by a universally quantified fresh variable.
And then you could write opaque (m ^ n) $ solve NatRing.

[oisdk]

It only works with the universally quantified form, yeah. So that example would have to be written as:

lemma₅ : ∀ m n → (m * n) * 1 ≈ m * n
lemma₅ m n = ((∀ m*n → m*n * 1 ≈ m*n) ∋ solve IntRing) _

(You'll also notice I haven't implemented exponentiation yet!)

The implementation currently is actually quite small: it just looks for any uses of the ring operators, then any variables, then builds the Expr AST out of it, and calls off to the current ring solver. (well, actually it's a different implementation that's sparse like in the Grégoire and Mahboubi paper, but its interface is basically the same)

[MatthewDaggitt]

Looks like great work. Yes please do put together a PR if you have the chance!