### 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

- Asking the identity, along with
`e1`

and`e2`

, be written down in the ring solver's syntax tree (this`_:*_`

) - Turing both the left hand side and the right hand side into a normal form
- 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