open import 1Lab.Reflection.Variables
open import 1Lab.Reflection
open import 1Lab.Path
open import 1Lab.Type

open import Data.Nat.Properties
open import Data.Fin.Base
open import Data.List

module Data.Nat.Solver where


# The Nat Solverπ

This module defines a solver for equations in the commutative semiring of natural numbers. Our approach splits cleanly into 3 distinct parts:

• Horner normal forms for polynomials
• Evaluation of reflected terms into polynomials
• The reflection interface

## Horner Normal Formsπ

If we ignore the suc and zero constructors, and their respective equations, the core problem at hand is trying to compute normal forms for polynomials. Luckily, like most problems involving polynomials, this has been thoroughly studied! There are many possible normal forms to choose from, but the most useful for our task is Horner normal form, as it admits a particularly nice inductive characterization.

The core idea is that we can rewrite a (univariate) polynomial of the form $a_0 + a_1 x + a_2 x^2 + a_3 x^3 + \cdots + a_n x^n$ into the following form: $a_0 + x ( a_1 + x ( a_2 + x ( a_3 + \cdots + x ( a_{n-1} + x a_n ) ) ) )$

However, we need multivariate polynomials, not just univariate! To do this, we exploit the isomorphism between $A[X_0, \cdots, X_n]$ and $A[X_0][X_1]\cdots[X_n]$. This allows us to define the normal form of a multivariate polynomial as (essentially) a product of univariate ones.

We start by defining the type of n-ary multivariate polynomials.

data Poly {a} (A : Type a) : Nat β Type a where


The first polynomial we define is the constant polynomial $c \in A[X_0]$.

  const : (c : A) β Poly A 0


Next, we define the 0 polynomial $0 \in A[X_0, \cdots, X_n]$. Note that we do _not. include $A[X_0]$ here! This is important for ensuring that our data type defines a (somewhat) unique normal form. If we had instead chosen Poly A n, we could represent the $0$ polynomial using either const 0 or zerop, which complicates matters somewhat.

  zerop  : β {n} β Poly A (suc n)


Finally, we define both addition and multiplication by $X_0$ in one fell swoop. This constructor represents the polynomial $p * X_0 + q$, where $p \in A[X_0]\cdots[X_n]$, and $q \in A[X_1]\cdots[X_n]$.

This flipping of the index may seem confusing at first, but it serves an important purpose: it makes evaluation really easy! When evaluating, we will need some environment Vec A n which assigns values to the various indeterminates $X_i$. In the variable case, the indexing will ensure that our environment is non-empty, whence we can use the tail of the vector to evaluate q! In this sense, not only does this constructor handle addition and multiplication by $X_0$, it also handles weakening.

  _*X+_ : β {n} β (p : Poly A (suc n)) β (q : Poly A n) β Poly A (suc n)

infixl 2 _*X+_

private variable
a : Level
A : Type a
n : Nat

-- NOTE: These little helper lemmas become very useful, and make
-- some of the really involved proofs a lot less painful.
commute-inner : β w x y z β (w + x) + (y + z) β‘ (w + y) + (x + z)
commute-inner w x y z =
(w + x) + (y + z) β‘Λβ¨ +-associative w x (y + z) β©β‘Λ
w + (x + (y + z)) β‘β¨ ap (w +_) (+-associative x y z) β©β‘
w + ((x + y) + z) β‘β¨ ap (Ξ» Ο β w + (Ο + z)) (+-commutative x y) β©β‘
w + (y + x + z)   β‘Λβ¨ ap (w +_) (+-associative y x z) β©β‘Λ
w + (y + (x + z)) β‘β¨  +-associative w y (x + z) β©β‘
(w + y) + (x + z) β

commute-last : β x y z β (x * y) * z β‘ (x * z) * y
commute-last x y z =
x * y * z   β‘β¨ *-associative x y z β©β‘
x * (y * z) β‘β¨ ap (x *_) (*-commutative y z) β©β‘
x * (z * y) β‘Λβ¨ *-associative x z y β©β‘Λ
x * z * y β


Note that this representation, while convenient, does pose some problems. We pay for the (relative) uniqueness by having larger terms: For instance, the polynomial $X^4 + 1$ is represented as

private
xβ΄+1 : Poly Nat 1
xβ΄+1 = zerop *X+ const 1 *X+ const 0 *X+ const 0 *X+ const 0 *X+ const 0


This could be alleviated by using a sparse representation, but this is decidedly more difficult. As the solver is not expected to deal with polynomials with large degrees, this term blow-up will not be a problem in practice.

### Operations on Horner Normal Formsπ

Now, letβs define a handful of functions for constructing and combining polynomials. The naming here can get a bit confusing, so letβs stick with the convention of adding a subscript p to denote an operation on polynomials. As a further note, the entire following section could be generalized work over an arbitrary semiring, but this would complicate the dependency graph somewhat, so we stick to natural numbers.

As previously mentioned, we have different representations of the $0$ polynomial depending on if we are working with Poly A zero or Poly A (suc n). This is somewhat annoying, so we define a small helper for picking the correct representation.

0β : Poly Nat n
0β {n = zero}  = const zero
0β {n = suc n} = zerop


While we are at it, we also define the polynomial that represents, given a constant $c$, the constant polynomial $c \in A[X_0]\cdots[X_n]$.

constβ : Nat β Poly Nat n
constβ {n = zero}  c = const c
constβ {n = suc n} c = 0β *X+ constβ c


The constant 1 is important enough that it deserves its own syntax.

1β : Poly Nat n
1β = constβ 1


We also define the identity monomials $X_i \in A[X_0]\cdots[X_n]$.

X[_] : Fin n β Poly Nat n
X[_] fzero    = 1β *X+ 0β
X[_] (fsuc i) = 0β *X+ X[ i ]


Now, onto addition of polynomials. This is more or less what one would expect if they wrote out the polynomials and did the addition by hand.

infixl 6 _+β_
infixl 7 _*β_

_+β_ : Poly Nat n β Poly Nat n β Poly Nat n
const cβ +β const cβ = const (cβ + cβ)
zerop +β q = q
(p *X+ q) +β zerop = p *X+ q
(p *X+ r) +β (q *X+ s) = (p +β q) *X+ (r +β s)


Multiplication, however, is somewhat trickier. The problem is that during the course of recursion, we will need to multiply a Poly A n by a Poly A (suc n) β for which we will need mutual recursion, since that multiplication will fall back to the βhomogeneousβ case eventually. We predeclare their types to make Agda happy:

_*β_ : Poly Nat n β Poly Nat n β Poly Nat n
_*ββ²_ : Poly Nat n β Poly Nat (suc n) β Poly Nat (suc n)


First, the homogeneous multiplication. The first two cases are pretty straightforward, but the final one is decidedly less so. To start, we can distribute the multiplication of r over the addition, invoking _+β_ to add the results together. When multiplying q and r, we need to use the aforementioned heterogeneous multiplication, as $q \in A[X_1]\cdots[X_n]$ β note that the index is off by one ($X_1$ vs $X_0$). When multiplying p and r, we need to add on a 0β under the *X, as this is the only way of multiplying by $X_0$.

const cβ  *β const cβ = const (cβ * cβ)
zerop     *β q        = zerop
(p *X+ q) *β r        = ((p *β r) *X+ 0β) +β (q *ββ² r)


For the heterogeneous case, the call graph is simpler, as we can fall back to the homogeneous operator.

r *ββ² zerop     = zerop
r *ββ² (p *X+ q) = (r *ββ² p) *X+ (r *β q)


### Evaluation of Horner Normal Formsπ

Multivariate polynomials represent functions $A^n \to A$, so we should be able to interpret them as such. Luckily, Horner Normal Forms are extremely easy to evaluate. As a historical note, this is why this representation was created in first place! In this light, they should probably be called βSharaf al-Din al-Tusi normal formsβ.

block : Nat β Nat
block x = x

β¦_β§β : Poly Nat n β Vec Nat n β Nat
β¦ const c β§β env        = c
β¦ zerop β§β   env        = 0
β¦ p *X+ q β§β (xβ β· env) = β¦ p β§β (xβ β· env) * xβ + β¦ q β§β env


### Soundness of the Operationsπ

Now, itβs important that the operations we defined actually denote the correct operations on natural numbers. As a warm up, letβs show that the zero polynomial really represents the function $f(x_0, \cdots, x_n) = 0$.

sound-0β : β (env : Vec Nat n) β β¦ 0β β§β env β‘ 0
sound-0β []        = refl
sound-0β (x β· env) = refl


We do the same for the constant polynomials:

sound-constβ : β c β (env : Vec Nat n) β β¦ constβ c β§β env β‘ c
sound-constβ c [] = refl
sound-constβ c (x β· env) = sound-constβ c env


At the risk of repeating ourselves, we also show the same for the monomial $X_i$.

sound-X[_] : β i β (env : Vec Nat n) β β¦ X[ i ] β§β env β‘ lookup env i
sound-X[ fzero ] (xβ β· env) =
β¦ constβ 1 β§β env * xβ + β¦ 0β β§β env β‘β¨ apβ (Ξ» Ο Ο β Ο * xβ + Ο) (sound-constβ 1 env) (sound-0β env) β©β‘
1 * xβ + 0                           β‘β¨ +-zeror (1 * xβ) β©β‘
1 * xβ                               β‘β¨ *-onel xβ β©β‘
xβ β
sound-X[ fsuc i ] (_ β· env) = sound-X[ i ] env


Now, for something more involved: letβs show that addition of polynomials really deserves the name βadditionβ β under the semantics mapping β¦_β§β, adding two polynomials then evaluating is the same thing as evaluating each then adding the results.

sound-+β : β p q β (env : Vec Nat n)
β β¦ p +β q β§β env β‘ β¦ p β§β env + β¦ q β§β env
sound-+β (const c1) (const c2) env = refl
sound-+β zerop q env = refl
sound-+β (p *X+ r) zerop env =
sym (+-zeror (β¦ (p *X+ r) +β zerop β§β env))
sound-+β (p *X+ r) (q *X+ s) (xβ β· env) =
β¦p+qβ§ * xβ + β¦r+sβ§                β‘β¨ apβ (Ξ» Ο Ο β Ο * xβ + Ο) (sound-+β p q (xβ β· env)) (sound-+β r s env) β©β‘
(β¦pβ§ + β¦qβ§) * xβ + (β¦rβ§ + β¦sβ§)    β‘β¨ ap (Ξ» Ο β Ο + (β¦rβ§ + β¦sβ§)) (*-distrib-+r β¦pβ§ β¦qβ§ xβ) β©β‘
β¦pβ§ * xβ + β¦qβ§ * xβ + (β¦rβ§ + β¦sβ§) β‘β¨ commute-inner (β¦pβ§ * xβ) (β¦qβ§ * xβ) β¦rβ§ β¦sβ§ β©β‘
β¦pβ§ * xβ + β¦rβ§ + (β¦qβ§ * xβ + β¦sβ§) β
where
β¦p+qβ§ = β¦ p +β q β§β (xβ β· env)
β¦r+sβ§ = β¦ r +β s β§β env
β¦pβ§ = β¦ p β§β (xβ β· env)
β¦rβ§ = β¦ r β§β env
β¦qβ§ = β¦ q β§β (xβ β· env)
β¦sβ§ = β¦ s β§β env


Wow, that was a bit painful! This is a common theme when writing proof automation: it distills down a lot of the annoying proofs we need to write across the entire code-base into one extremely painful proof. Thus, conservation of frustration is preserved.

Philosophical reflections aside, letβs move onto multiplication of polynomials. As the homogeneous and heterogeneous multiplication were defined in a mutually recursive manner, we must do so for their proofs of soundness as well.

sound-*β
: β p q β (env : Vec Nat n)
β β¦ p *β q β§β env β‘ β¦ p β§β env * β¦ q β§β env
sound-*ββ²
: β p q β (xβ : Nat) β (env : Vec Nat n)
β β¦ p *ββ² q β§β (xβ β· env) β‘ β¦ p β§β env * β¦ q β§β (xβ β· env)


The first couple of cases of homogeneous multiplication donβt look so badβ¦

sound-*β (const c1) (const c2) env = refl
sound-*β zerop q env = refl
sound-*β (p *X+ r) zerop (xβ β· env) =
β¦ p *β zerop β§β (xβ β· env) * xβ + β¦ 0β β§β env β‘β¨ apβ (Ξ» Ο Ο β Ο * xβ + Ο) (sound-*β p zerop (xβ β· env)) (sound-0β env) β©β‘
β¦pβ§ * 0 * xβ + 0                              β‘β¨ ap (Ξ» Ο β (Ο * xβ) + 0) (*-zeror β¦pβ§) β©β‘
0                                             β‘Λβ¨ *-zeror (β¦pβ§ * xβ + β¦rβ§) β©β‘Λ
(β¦pβ§ * xβ + β¦rβ§) * 0 β
where
β¦pβ§ = β¦ p β§β (xβ β· env)
β¦rβ§ = β¦ r β§β env


However, the case where we need to distribute is not so easy. The consists of repeatedly expanding out the polynomial operations into those on natural numbers, then doing a brutal bit of symbol shuffling. Thereβs not too much to be gained from dwelling on this, so letβs move on.

sound-*β (p *X+ r) (q *X+ s) (xβ β· env) =
β¦p*β¨qx+sβ©+r*qβ§ * xβ + β¦ 0β +β (r *β s) β§β env                β‘β¨ ap (Ξ» Ο β β¦p*β¨qx+sβ©+r*qβ§ * xβ + Ο) (sound-+β 0β (r *β s) env) β©β‘
β¦p*β¨qx+sβ©+r*qβ§ * xβ + (β¦ 0β β§β env + β¦ r *β s β§β env)        β‘β¨ apβ (Ξ» Ο Ο β β¦p*β¨qx+sβ©+r*qβ§ * xβ + (Ο + Ο)) (sound-0β env) (sound-*β r s env) β©β‘
β¦p*β¨qx+sβ©+r*qβ§ * xβ + (β¦rβ§ * β¦sβ§)                            β‘β¨ ap (Ξ» Ο β Ο * xβ + β¦rβ§ * β¦sβ§) (sound-+β (p *β (q *X+ s)) (r *ββ² q) (xβ β· env)) β©β‘
(β¦p*β¨qx+sβ©β§ + β¦r*qβ§) * xβ + β¦rβ§ * β¦sβ§                        β‘β¨ apβ (Ξ» Ο Ο β (Ο + Ο) * xβ + β¦rβ§ * β¦sβ§) (sound-*β p (q *X+ s) (xβ β· env)) (sound-*ββ² r q xβ env) β©β‘
(β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) + β¦rβ§ * β¦qβ§) * xβ + β¦rβ§ * β¦sβ§        β‘β¨ ap (Ξ» Ο β Ο + β¦rβ§ * β¦sβ§) (*-distrib-+r (β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§)) (β¦rβ§ * β¦qβ§) xβ) β©β‘
β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ + β¦rβ§ * β¦qβ§ * xβ + β¦rβ§ * β¦sβ§     β‘Λβ¨ +-associative (β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ) (β¦rβ§ * β¦qβ§ * xβ) (β¦rβ§ * β¦sβ§) β©β‘Λ
β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ + (β¦rβ§ * β¦qβ§ * xβ + β¦rβ§ * β¦sβ§)   β‘β¨ ap (Ξ» Ο β  β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ + (Ο + β¦rβ§ * β¦sβ§)) (*-associative β¦rβ§ β¦qβ§ xβ) β©β‘
β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ + (β¦rβ§ * (β¦qβ§ * xβ) + β¦rβ§ * β¦sβ§) β‘Λβ¨ ap (Ξ» Ο β β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ + Ο) (*-distrib-+l (β¦qβ§ * xβ) β¦sβ§ β¦rβ§) β©β‘Λ
β¦pβ§ * (β¦qβ§ * xβ + β¦sβ§) * xβ + β¦rβ§ * (β¦qβ§ * xβ + β¦sβ§)         β‘β¨ ap (Ξ» Ο β Ο + β¦rβ§ * (β¦qβ§ * xβ + β¦sβ§)) (commute-last β¦pβ§ (β¦qβ§ * xβ + β¦sβ§) xβ) β©β‘
β¦pβ§ * xβ * (β¦qβ§ * xβ + β¦sβ§) + β¦rβ§ * (β¦qβ§ * xβ + β¦sβ§)         β‘Λβ¨ *-distrib-+r (β¦pβ§ * xβ) β¦rβ§ (β¦qβ§ * xβ + β¦sβ§) β©β‘Λ
(β¦pβ§ * xβ + β¦rβ§) * (β¦qβ§ * xβ + β¦sβ§)                          β
where
β¦p*β¨qx+sβ©+r*qβ§ = β¦ (p *β (q *X+ s)) +β (r *ββ² q) β§β (xβ β· env)
β¦p*β¨qx+sβ©β§ = β¦ p *β (q *X+ s) β§β (xβ β· env)
β¦r*qβ§ = β¦ r *ββ² q β§β (xβ β· env)
β¦pβ§ = β¦ p β§β (xβ β· env)
β¦rβ§ = β¦ r β§β env
β¦qβ§ = β¦ q β§β (xβ β· env)
β¦sβ§ = β¦ s β§β env


As a nice palate cleanser, the proofs for heterogeneous multiplication are nowhere near as bad.

sound-*ββ² p zerop xβ env = sym (*-zeror (β¦ p β§β env))
sound-*ββ² r (p *X+ q) xβ env =
β¦ r *ββ² p β§β (xβ β· env) * xβ + β¦ r *β q β§β env β‘β¨ apβ (Ξ» Ο Ο β Ο * xβ + Ο) (sound-*ββ² r p xβ env) (sound-*β r q env) β©β‘
β¦rβ§ * β¦pβ§ * xβ + β¦rβ§ * β¦qβ§                     β‘β¨ ap (Ξ» Ο β Ο + β¦rβ§ * β¦qβ§) (*-associative β¦rβ§ β¦pβ§ xβ) β©β‘
β¦rβ§ * (β¦pβ§ * xβ) + β¦rβ§ * β¦qβ§                   β‘Λβ¨ *-distrib-+l  (β¦pβ§ * xβ) β¦qβ§ β¦rβ§ β©β‘Λ
β¦rβ§ * (β¦pβ§ * xβ + β¦qβ§)                         β
where
β¦rβ§ = β¦ r β§β env
β¦pβ§ = β¦ p β§β (xβ β· env)
β¦qβ§ = β¦ q β§β env


This concludes phase one of the solver.

## Evaluation into Polynomialsπ

Now that weβve gotten the first phase of the solver done, letβs move on to expressions in the language of natural numbers. Our first move shall be defining expressions in the equational theory of natural numbers.

However, there is an efficiency problem we need to take care of here. If we naively expand out _+_ and _*_ during reflection, we could end up in a situation where we need to contend with a huge amount of suc constructors when large literals get involved. Therefore, we prevent reduction of such functions, but this means this phase of the solver needs to be aware of nat literals.

With that in mind, letβs define our expressions. Note that things that the solver is unable to deal with (for instance, functions that arenβt _+_ or _*_) are represented as variables, and will be replaced during evaluation.

data Expr : Nat β Type where
β΅0   : β {n} β Expr n
β΅lit : β {n} β Nat    β Expr n
β΅_   : β {n} β Fin n  β Expr n
β΅1+_ : β {n} β Expr n β Expr n
_β΅+_ : β {n} β Expr n β Expr n β Expr n
_β΅*_ : β {n} β Expr n β Expr n β Expr n


We also define an interpretation of expressions into functions $\mathbb{N}^n \to \mathbb{N}$.

β¦_β§β : Expr n β Vec Nat n β Nat
β¦ β΅ i      β§β env = lookup env i
β¦ β΅0       β§β env = 0
β¦ β΅1+ e    β§β env = suc (β¦ e β§β env)
β¦ β΅lit k   β§β env = k
β¦ e1 β΅+ e2 β§β env = β¦ e1 β§β env + β¦ e2 β§β env
β¦ e1 β΅* e2 β§β env = β¦ e1 β§β env * β¦ e2 β§β env


We also define an evaluation of expressions into polynomials. The only thing to note here is the evaluation of quoted suc constructors as polynomial addition. This is somewhat inneficient, but in practice we rarely have too many suc constructors to deal with, as we handle literals separately.

β_ : Expr n β Poly Nat n
β (β΅ i)      = X[ i ]
β β΅0         = 0β
β (β΅1+ e)    = constβ 1 +β β e
β β΅lit k     = constβ k
β (eβ β΅+ eβ) = (β eβ) +β (β eβ)
β (eβ β΅* eβ) = (β eβ) *β (β eβ)


### Soundness of Evaluationπ

With all of that machinery in place, our final proof shall be to show that evaluating an expression into a polynomial has the same semantics as the original expression. Luckily, most of the legwork is already done, so we can sit back and enjoy the fruits of our labour.

sound : β e β (env : Vec Nat n) β β¦ β e β§β env β‘ β¦ e β§β env
sound (β΅ i) env = sound-X[ i ] env
sound β΅0 env = sound-0β env
sound (β΅1+ e) env =
β¦ constβ 1 +β (β e) β§β env       β‘β¨ sound-+β (constβ 1) (β e) env β©β‘
β¦ constβ 1 β§β env + β¦ β e β§β env β‘β¨ ap (Ξ» Ο β Ο + β¦ β e β§β env ) (sound-constβ 1 env) β©β‘
suc (β¦ β e β§β env)               β‘β¨ ap suc (sound e env) β©β‘
suc (β¦ e β§β env) β
sound (β΅lit k) env = sound-constβ k env
sound (eβ β΅+ eβ) env =
β¦ (β eβ) +β (β eβ) β§β env     β‘β¨ sound-+β (β eβ) (β eβ) env β©β‘
β¦ β eβ β§β env + β¦ β eβ β§β env β‘β¨ apβ _+_ (sound eβ env) (sound eβ env) β©β‘
β¦ eβ β§β env + β¦ eβ β§β env     β
sound (eβ β΅* eβ) env =
β¦ (β eβ) *β (β eβ) β§β env     β‘β¨ sound-*β (β eβ) (β eβ) env β©β‘
β¦ β eβ β§β env * β¦ β eβ β§β env β‘β¨ apβ _*_ (sound eβ env) (sound eβ env) β©β‘
β¦ eβ β§β env * β¦ eβ β§β env     β



Now, all we need to do is expose an interface for the reflection portion of the solver. The abstract here is VERY IMPORTANT, as it prevents the proof from unfolding into an enormous term that kills our compile times.

abstract
solve : β eβ eβ β (env : Vec Nat n)
β (β¦ β eβ β§β env β‘ β¦ β eβ β§β env)
β β¦ eβ β§β env    β‘ β¦ eβ β§β env
solve eβ eβ env p = sym (sound eβ env) Β·Β· p Β·Β· sound eβ env


We also expose a function for βsimplifyingβ expressions. In reality this will almost always make the term more complicated, but itβs useful for debugging purposes.

expand : (e : Expr n) β (env : Vec Nat n) β Nat
expand e env = β¦ β e β§β env


## Reflectionπ

Now, for the truly difficult part: the reflection interface. We begin by defining some pattern synonyms for expressions we want to reflect into our Expr type.

private
pattern nat-lit n =
def (quote Number.fromNat) (_ β· _ β· _ β· (lit (nat n)) vβ· _)
pattern β³zeroβ³ =
con (quote zero) []
pattern β³sucβ³ x =
con (quote suc) (x vβ· [])
pattern _β³+β³_ x y =
def (quote _+_) (x vβ· y vβ· _)
pattern _β³*β³_ x y =
def (quote _*_) (x vβ· y vβ· _)


Next, we construct quoted a Expr from a term, replacing any unknown Term nodes with variables. This uses the Variable interface for managing the Fin variables and the environment. A discussion of the internals of this is out of scope of this solver; we have already looked into the abyss too deeply.

private
build-expr : Variables Nat β Term β TC (Term Γ Variables Nat)
build-expr vs (nat-lit n) = do
β΅n β quoteTC n
returnTC $con (quote β΅lit) (β΅n vβ· []) , vs build-expr vs β³zeroβ³ = do returnTC$ con (quote β΅0) (unknown hβ· []) , vs
build-expr vs (β³sucβ³ t) = do
e , vs β build-expr vs t
returnTC $con (quote β΅1+_) (unknown hβ· e vβ· []) , vs build-expr vs (tβ β³+β³ tβ) = do eβ , vs β build-expr vs tβ eβ , vs β build-expr vs tβ returnTC$ con (quote _β΅+_) (unknown hβ· eβ vβ· eβ vβ· []) , vs
build-expr vs (tβ β³*β³ tβ) = do
eβ , vs β build-expr vs tβ
eβ , vs β build-expr vs tβ
returnTC $con (quote _β΅*_) (unknown hβ· eβ vβ· eβ vβ· []) , vs build-expr vs tm = do (v , vsβ²) β bind-var vs tm returnTC$ con (quote β΅_) (v vβ· []) , vsβ²


Next, letβs define the quoted forms of some terms that we will use to interface with the solver.

private
β³expandβ³ : Term β Term β Term
β³expandβ³ e env = def (quote expand) (unknown hβ· e vβ· env vβ· [])

β³solveβ³ : Term β Term β Term β Term
β³solveβ³ lhs rhs env =
def (quote solve)
(unknown hβ· lhs vβ· rhs vβ· env vβ· def (quote refl) [] vβ· [])


### The Actual Macrosπ

Now, the actual reflection API calls. In order to keep drawing this file out, we start by defining some useful debugging macros. As we noted a looong time ago, we donβt want to unfold the _+_ or _*_ functions, so letβs make a list of those names so that we can call withReduceDefs more easily.

private
don't-reduce : List Name
don't-reduce = quote _+_ β· quote _*_ β· quote Number.fromNat β· []


The repr! macro prints out a bunch of information about a given expression of type Nat. This is very useful when we are debugging.

repr-macro : Nat β Term β TC β€
repr-macro n hole =
withNormalisation false $withReduceDefs (false , don't-reduce)$ do
tm β quoteTC n
e , vs β build-expr empty-vars tm
size , env β environment vs
repr β normalise $def (quote β_) (size hβ· e vβ· []) typeError$ strErr "The expression\n  " β·
termErr tm β·
strErr "\nIs represented by the expression\n  " β·
termErr e β·
strErr "\nAnd the polynomial\n  " β·
termErr repr β·
strErr "\nThe environment is\n  " β·
termErr env β· []
macro
repr! : Nat β Term β TC β€
repr! n = repr-macro n


Slightly more useful is the expand! macro. This takes in a natural number, and will fill in the hole with its expanded form. This is intended to be used with the agda2-elaborate-give command in Emacs, which is bound to C-c RET by default.

expand-macro : Nat β Term β TC β€
expand-macro n hole =
withNormalisation false $withReduceDefs (false , don't-reduce)$ do
tm β quoteTC n
e , vs β build-expr empty-vars tm
size , env β environment vs
expanded β reduce (β³expandβ³ e env)
unify hole expanded

macro
expand! : Nat β Term β TC β€
expand! n = expand-macro n


Now, finally, we have reached the summit. The nat! macro allows us to automatically solve equations involving natural numbers.

solve-macro : Term β TC β€
solve-macro hole =
withNormalisation false $withReduceDefs (false , don't-reduce)$ do
goal β inferType hole >>= reduce

just (lhs , rhs) β get-boundary goal
where nothing β typeError $strErr "Can't determine boundary: " β· termErr goal β· [] elhs , vs β build-expr empty-vars lhs erhs , vs β build-expr vs rhs size , env β environment vs (noConstraints$ unify hole (β³solveβ³ elhs erhs env)) <|> do
nf-lhs β normalise (β³expandβ³ elhs env)
nf-rhs β normalise (β³expandβ³ erhs env)
typeError (strErr "Could not solve the following goal:\n  " β·
termErr lhs β· strErr " β‘ " β· termErr rhs β·
strErr "\nComputed normal forms:\n  LHS: " β·
termErr nf-lhs β·
strErr "\n  RHS: " β·
termErr nf-rhs β· [])

macro
nat! : Term β TC β€
nat! = solve-macro


# Examplesπ

Congratulations! We now have a solver. Letβs marvel at all of our hard work for a moment.

private
wow-good-job : β x y z
β (x + 5 + suc y) * z β‘ z * 5 + x * z + z + z * y
wow-good-job x y z = nat!


Thus concludes our journey. There is still room for improvement, however. A sparse representation would be much more efficient, but these proofs are already quite difficult to begin with. For the brave, here is what a sparse representation might look like.

private
data SparsePoly {a} (A : Type a) : Nat β Type a where
const-sparse : β {n} β A β SparsePoly A n
shift        : β {n} β (j : Nat) β SparsePoly A n
β SparsePoly A (j + n)
_*X^_+_      : β {n} β SparsePoly A (suc n) β Nat β SparsePoly A n
β SparsePoly A (suc n)