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