UsingTheRingSolver

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