# Using The Ring Solver

### First example: a semiring solver for the natural numbers

The Standard Library's natural numbers come "pre-loaded" with a natural number semiring solver, so we will use that as a starting point. This example imports natural numbers, equality, and the pre-defined solver from the standard library.

```  open import Data.Nat using (_+_; _*_; ℕ)
open import Relation.Binary.Core using (_≡_; refl)
import Data.Nat.Properties
open Data.Nat.Properties.SemiringSolver
using (prove; solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)
```

The first thing we want to observe is that, for numerical functions, Agda will take what we wrote down (say, `4 + 6 ≡ 10`) and do some work on it (to compute `10 ≡ 10`): in these cases, a solver is unnecessary, as the "`refl`" axiom will do the job.

```  lem1 : (4 + 6 ≡ 10)
lem1 = refl
```

However, we certainly can use the "trivial" or "0-variable" ring solver to solve these formulas; the `refl` below fulfills the proof obligation `10 ≡ 10`.

```  lem2 : (4 + 6 ≡ 10)
lem2 = solve 0 (con 4 :+ con 6 := con 10) refl
```

Where the ring solver gets interesting is when we have that first argument to `solve` as a number greater than 0. In order to prove the basic identity `(2 * (x + 4) ≡ 8 + 2 * x)`, we use the solver with the argument 1 (because we have one variable, `x`).

```  lem3 : (x : ℕ) → (2 * (x + 4) ≡ 8 + 2 * x)
lem3 = solve 1 (λ x' → con 2 :* (x' :+ con 4) := con 8 :+ con 2 :* x') refl
```

In general, all the ring solver does is solve equations of the form `e1 ≡ e2` by

1. Asking the identity, along with `e1` and `e2`, be written down in the ring solver's syntax tree (this `_:*_`)
2. Turing both the left hand side and the right hand side into a normal form
3. Requiring the user to prove that the two normal forms are equal

The ring solver "succeeds" if the left hand side and right hand side are, in fact, identical - in this case, the axiom `refl` will satisfy the proof obligation in step 3. If they are not, the proof obligation (shown as the argument `eq` in the example below below) may be extremely complicated (in this case, more complicated than the original formula!)

```  lem4 : (x y z : ℕ)
→ ((a b c : ℕ)
→ (a + 0) + (b + 0 + 0) ≡ (a + 0) + ((b + 0) + ((c + (c + 0) + 0))))
→ x + y ≡ z * 2 + (y + x)
lem4 x y z eq =
solve 3 (λ x y z → x :+ y := z :* con 2 :+ (y :+ x))
(λ {x y z} → eq x y z) x y z
```

The proof obligation generated by this failed trace does not give any good path to expressing the fact that, if `z` is zero, the identity will actually hold. The example does give a good look at the structure of the normal forms. In this example they look a bit like a series of nested, zero-terminated lists: see Algebra.RingSolver or "Proving Equalities in a Commutative Ring Done Right in Coq" by Grégoire and Mahboubi, which describes the theory behind the ring solver in more detail.

#### A few more examples

These come from the test suite for a (significantly less efficient) solver written in Twelf.

```  lem5 : (x y z : ℕ) → z + (x + y) ≡ x + 0 + 0 + z + 0 + y
lem5 = solve 3
(λ x y z → z :+ (x :+ y) := x :+ con 0 :+ con 0 :+ z :+ con 0 :+ y) refl

lem6 : (a b c d e f g h i : ℕ)
→ a * (b + (c * (d + (e * (f + (g * (h + i))))))) ≡
a * (b + (c * (d + (e * (f + (g * (h))))))) + a * (c * 1 * e) * g * i
lem6 = solve 9
(λ a b c d e f g h i →
a :* (b :+ (c :* (d :+ (e :* (f :+ (g :* (h :+ i))))))) :=
a :* (b :+ (c :* (d :+ (e :* (f :+ (g :* h))))))
:+ a :* (c :* con 1 :* e) :* g :* i) refl
```