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
Advertisements
This entry was posted in Computers and tagged , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s