## First steps with Agda: provable factoring

In my last post we looked at the problem of factoring an integer. We ran into an issue with the termination checker and resolved it by wrapping the recursion into a separate inductive data-type that made it explicit. The idiom used is present in Agda’s standard library and can be used “off the shelf” this way:

```module factor-idiomatic where

open import Data.Fin as F
open import Induction.WellFounded
open import Induction.Nat
open import Data.List
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties

factor : (n : ℕ) → Acc _<′_ n → List ℕ
factor 0 _ = 0 ∷ []
factor 1 _ = []
factor (suc (suc n)) (acc p) = helper n ≤′-refl
where helper : (try : ℕ) → ((suc try) <′ (suc (suc n))) → List ℕ
lemma : ∀ {f n} → ((suc f) <′ (suc (suc n))) → (f <′ (suc (suc n)))

helper 0 _ = (suc (suc n)) ∷ []
helper (suc f) proof with ((suc (suc n)) divMod' (suc (suc f)))
... | result q F.zero _ = q ∷ factor (suc (suc f)) (p (suc (suc f)) proof)
... | _ = helper f (lemma proof)

lemma ≤′-refl = ≤′-step ≤′-refl
lemma (≤′-step m≤′n) with ≤′⇒≤ (≤′-step m≤′n)
lemma (≤′-step m≤′n) | s≤s m≤n = ≤⇒≤′ (≤-step m≤n)

factorize : ℕ → List ℕ
factorize n = factor n (<-well-founded n)

factors₃₀ = factorize 30
```

If you look at the sources, `Acc` is defined as

```data Acc {a} {A : Set a} (_<_ : Rel A a) (x : A) : Set a where
acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x
```

which basically boils down to

```data Acc {a} {A : Set a} (_<_ : Rel A a) (x : A) : Set a where
acc : (rs : ∀ y → (y < x) → Acc y) → Acc _<_ x
```

… pretty close to what we defined and used. Importantly, Agda already defines `<-well-founded`, which is equivalent to `generateTerminationProof` we defined earlier. We will use this more idiomatic version of the terminating `factor` definition in this post.

So now we wish to somehow verify that the `List ℕ` we returned really multiplies to `n`. One way to do this is by creating a new data type family

```  data Factorization : ℕ → Set where
...
```

and somehow ensure that `Factorization n` can only be constructed once we have a correct factorization for `n`. So, how about this:

```  data Factorization : ℕ → Set where
factors : (n : ℕ) → (f : List ℕ) → (product f ≡ n) → Factorization n
```

_≡_ is an interesting type. It is parameterized on a value and is indexed on another value of the same type. The only constructor for ≡ is `refl`. In Agda, the values of the type parameters are the same for all the type constructors. However, the constructors do get to choose values for the type indices. So, for instance, the following code is illegal

```open import Data.Nat

data K (a : ℕ) (b : ℕ) : Set where
construct : K a 42
```

since `construct` can’t decide the values of `a` and `b`. However, this is allowed

```open import Data.Nat

data K : ℕ → ℕ → Set where
construct : K 42 42
```

Getting back to `_≡_`, the definition says

```data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
```

meaning given a value `x` of type `A`, `refl` will choose the index of the constructed `_≡_ x` to be `x`. Since `refl` is the only constructor `_≡_` has, `a ≡ b` will have a value only if Agda can somehow prove that `a` and `b` are equal. Moreover, this value, `refl` of type `a ≡ b`, is itself the proof of `a` and `b`‘s equality.

Getting back to defining `Factorization`, the type we last described takes an integer, `n`; a list of integers, `f`; and a proof of the fact that the product of the integers in `f` is `n`. Only after supplying all this can you construct a value of type `Factorization n`. You can also just as easily decompose a value of type `Factorization n` into `n`, `f` and the proof.

However, while it may certainly be possible to go ahead with this definition of `Factorization`, we choose one more amenable to composing; one in which we can easily augment proofs to create larger proofs. I’m talking about something like this:

```data Factorization : ℕ → Set where
singleton : Factorization 1
augment : {old : ℕ} {n : ℕ} → (new-factor : ℕ) →
(Factorization old) → ((new-factor * old) ≡ n) →
Factorization n
```

When we factor `1`, we use the `singleton` constructor. `augment` (the equivalent of cons here) uses an old factorization and a new factor to construct a new `Factorization`. We also have to supply a value of the type `((new-factor * old) ≡ n)` or a proof that `(new-factor * old)` is equal to `n`. Therefore, at every step, our invariant of all the numbers in the an object of type `Factorization n` multiplying up to `n` stays valid. As an example, a valid value of the type `Factorization 20` is `augment 2 (augment 2 (augment 5 singleton proof0) proof1) proof2` where `proof2` is a value (proof) of type (proposition) `2 * 10 ≡ 20`, `proof1` is a value of type `2 * 5 ≡ 20` and so forth.

But how do we generate this value of type `((new-factor * old) ≡ n)`? How do we statically convince Agda that the `new-factor` we’re feeding to the type constructor actually satisfies this constraint? Fortunately, most of our work has already been done.

The `divMod'` function returns a value of type `DivMod'` which, apart from holding the quotient and the remainder also holds a proof (value) of the proposition (type) `quotient * divisor + remainder ≡ dividend`. When the remainder is zero, this proof can be transformed to the one required by the `augment` constructor. This transformation is itself a proof; given a certain condition, it proves another. The Curry-Howard isomorphism maps implication to function types, and the proposition we’re seeking to prove is

```lemma₁ : forall {r} → (q : ℕ) (d : ℕ) (n : ℕ) → (r ≡ 0) →
(r + q * d ≡ n) → (q * d ≡ n)
```

which is the same as “given that (r ≡ 0) and (r + q * d ≡ n), we prove (q * d ≡ n)”. The definition for `lemma₁` is weirdly simple:

```  lemma₁ q d .(q * d) refl refl = refl
```

Agda understands definitional equalities. Since `zero + n ≡ n` is a definitional equality we can get away by telling Agda that the truth of the proposition is “obvious”.

We’ll also need a proof for `n * 1 ≡ n` at some point, so let’s have a look:

```identity* : (n : ℕ) → (n * 1 ≡ n)
identity* zero = refl
identity* (suc n') = cong suc (identity* n')
```

The first thing to observe is that `n * 1 ≡ n` is not a definitional equality and requires a proof. There are two cases, when `n` is `zero` and when it isn’t. Funnily, if you see the definition of `_*_`, you’ll notice `zero * n ≡ zero` is, in fact, a definitional equality so we can get away with `refl` in the `identity* zero`.

The `identity* (suc n')` is slightly more involved. First we recurse to prove `n' * 1 ≡ n'` and then call use `cong` to turn it into a proof of `n * 1 ≡ n`. `cong` can be used to transform a proof of `a ≡ b` to a proof of `f a ≡ f b` and in this case, we set `f` to `suc`.

A small note on a lemma we looked at in the last post

```lemma : ∀ {f n} → ((suc f) <′ (suc (suc n))) → (f <′ (suc (suc n)))
lemma ≤′-refl = ≤′-step ≤′-refl
lemma (≤′-step m≤′n) with ≤′⇒≤ (≤′-step m≤′n)
lemma (≤′-step m≤′n) | s≤s m≤n = ≤⇒≤′ (≤-step m≤n)
```

Agda has two inductive definitions for the “less than” relation on natural numbers. The first one, `_<_` says i) ` zero` is less than any `suc n` and ii) `m < n` implies `(suc m) < (suc n)`. The second definition, `_<'_` says i) `m < (suc m)` and ii) `m < n` implies `m < (suc n)`. Actually, the library version is a little bit more complex than this since it first defines the “less than or equal” (`≤`) relation and then defines `_<_` in terms of `≤`. Similarly for `_≤′_` and `_<′_`. This definition of `lemma` uses both the `_<_` and the `_<′_` variants. I don’t know if there is a better implementation.

Here is the full, code, stitched together:

```module factor-provable where

open import Data.Fin as F hiding(_+_)
open import Induction.WellFounded
open import Induction.Nat
open import Data.List
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

data Factorization : ℕ → Set where
singleton : Factorization 1
augment : {old : ℕ} {n : ℕ} → (new-factor : ℕ) →
(Factorization old) → ((new-factor * old) ≡ n) →
Factorization n

identity* : (n : ℕ) → (n * 1 ≡ n)
identity* zero = refl
identity* (suc n') = cong suc (identity* n')

factor : (n : ℕ) → Acc _<′_ n → Factorization n
factor 0 _ = augment 0 singleton (identity* 0)
factor 1 _ = singleton
factor (suc (suc n)) (acc p) = helper n ≤′-refl
where helper : (try : ℕ) → ((suc try) <′ (suc (suc n))) → Factorization (suc (suc n))
lemma₀ : ∀ {f n} → ((suc f) <′ (suc (suc n))) → (f <′ (suc (suc n)))
lemma₁ : forall {r} → (q : ℕ) (d : ℕ) (n : ℕ) →
(r ≡ 0) → (r + q * d ≡ n) → (q * d ≡ n)

helper 0 _ = augment (suc (suc n)) singleton (identity* (suc (suc n)))
helper (suc f) proof-<′ with ((suc (suc n)) divMod' (suc (suc f)))
... | result q F.zero proof-div =
let rest = factor (suc (suc f)) (p (suc (suc f)) proof-<′)
proof-main = lemma₁ q (suc (suc f)) (suc (suc n)) refl
(sym proof-div)
in augment q rest proof-main
... | _ = helper f (lemma₀ proof-<′)

lemma₀ ≤′-refl = ≤′-step ≤′-refl
lemma₀ (≤′-step m≤′n) with ≤′⇒≤ (≤′-step m≤′n)
lemma₀ (≤′-step m≤′n) | s≤s m≤n = ≤⇒≤′ (≤-step m≤n)

lemma₁ q d .(q * d) refl refl = refl

factorize : (n : ℕ) → Factorization n
factorize n = factor n (<-well-founded n)

factors₅₀ = factorize 50
```
This entry was posted in Computers and tagged , , . Bookmark the permalink.