How to use Agda ring solvers to prove equations?

AgdaSolver.agda

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1
-}

open import Data.List
open import Relation.Binary.PropositionalEquality

module AgdaSolver where

  module Tactic-ℕ where
    -- There is a handy tactic for solving equations that involve ring
    -- operations and variables only.

    open import Data.Nat
    open import Data.Nat.Tactic.RingSolver

    -- Universally quantified statements are taken care of by solve-∀
    cow : ∀ (m n : ℕ) → m * (2 * n + 1) ≡ n * m * 2 + m
    cow = solve-∀

    -- When performing a single step, we use solve, which wants the list of free
    -- variables.
    bull : ∀ (m n : ℕ) → m * (2 * n + 1) ≡ n * m * 2 + m
    bull m n = solve (m ∷ n ∷ [])

    -- The following example fails because we have a compound
    -- sub-expression “f n” instead of a variable. Below we show how to handle it.
    -- calf : ∀ (f : ℕ → ℕ) (m n : ℕ) → m * (2 * f n + 1) ≡ f n * m * 2 + m
    -- calf f = solve-∀

  module Tactic-ℤ where
    -- The above examples do *not* work for the integers because there is something
    -- about _*_ on ℤ that trips it up. But _+_ works ok.

    open import Data.Integer
    open import Data.Integer.Tactic.RingSolver

    sheep : ∀ (m n : ℤ) → m + n + n ≡ n + m + n
    sheep = solve-∀

    ram : ∀ (m n : ℤ) → m + n + n ≡ n + m + n
    ram m n = solve (m ∷ n ∷ [])

  module Solver-ℕ where
    -- We can also use solvers that are less automatic but more flexible.

    open import Data.Nat
    open import Data.Nat.Solver using (module +-*-Solver)
    open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)

    -- the first argument to solve is the number of variables, the second one is
    -- the reified equation (i.e., the equation written in the special mini-language of the solver),
    -- and as far as I can tell, the third one can always just be refl
    hen : ∀ (m n : ℕ) → m * (2 * n + 1) ≡ n * m * 2 + m
    hen = solve 2 (λ m n → m :* (con 2 :* n :+ con 1) := n :* m :* con 2 :+ m) refl

    -- the reified expression is used as a kind of pattern through which we can
    -- handle compund subexpressions
    rooster : ∀ (f g : ℕ → ℕ) (m n : ℕ) → g (g m) * (2 * f n + 1) ≡ f n * g (g m) * 2 + g (g m)
    rooster f g m n = solve 2 (λ x y → x :* (con 2 :* y :+ con 1) := y :* x :* con 2 :+ x) refl (g (g m)) (f n)

  module Solver-ℤ where
    -- The same for integers

    open import Data.Integer
    open import Data.Integer.Solver using (module +-*-Solver)
    open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)

    -- the first argument to solve is the number of variables, the second one is
    -- the reified equation (i.e., the equation written in the special mini-language of the solver),
    -- and as far as I can tell, the third one can always just be refl
    deer : ∀ (m n : ℤ) → m * ((+ 2) * n + (+ 1)) ≡ n * m * (+ 2) + m
    deer = solve 2 (λ m n → m :* (con (+ 2) :* n :+ con (+ 1)) := n :* m :* con (+ 2) :+ m) refl

    -- the reified expression is used as a kind of pattern through which we can
    -- handle compund subexpressions
    stag : ∀ (f g : ℤ → ℤ) (m n : ℤ) → g (g m) * ((+ 2) * f n + (+ 1)) ≡ f n * g (g m) * (+ 2) + g (g m)
    stag f g m n = solve 2 (λ x y → x :* (con (+ 2) :* y :+ con (+ 1)) := y :* x :* con (+ 2) :+ x) refl (g (g m)) (f n)