functional programming - How to define division operator in Agda?

Question

I want to divide two natural number. I have made function like this

_/_ : N -> N -> frac
m / one = m / one
(suc m) / n = ??        I dont know what to write here.

Please help.

Answer 1

As @gallais says you can use well-founded recursion explicitly, but I don't like this approach, because it's totally unreadable.

This datatype

record Is {α} {A : Set α} (x : A) : Set α where
  ? = x
open Is

! : ? {α} {A : Set α} -> (x : A) -> Is x
! _ = _

allows to lift values to the type level, for example you can define a type-safe pred function:

pred? : ? {n} -> Is (suc n) -> ?
pred? = pred ° ?

Then

test-1 : pred? (! 1) ≡ 0
test-1 = refl

typechecks, while

fail : pred? (! 0) ≡ 0
fail = refl

doesn't. It's possible to define subtraction with positive subtrahend (to ensure well-foundness) in the same way:

_-?_ : ? {m} -> ? -> Is (suc m) -> ?
n -? im = n ? ? im

Then using stuff that I described here, you can repeatedly subtract one number from another until the difference is smaller than the second number:

lem : ? {n m} {im : Is (suc m)} -> m < n -> n -? im <′ n
lem {suc n} {m} (s≤s _) = s≤′s (≤?≤′ (n?m≤n m n))

iter-sub : ? {m} -> ? -> Is (suc m) -> List ?
iter-sub n im = calls (λ n -> n -? im) <-well-founded lem (_≤?_ (? im)) n

For example

test-1 : iter-sub 10 (! 3) ≡ 10 ∷ 7 ∷ 4 ∷ []
test-1 = refl

test-2 : iter-sub 16 (! 4) ≡ 16 ∷ 12 ∷ 8 ∷ 4 ∷ []
test-2 = refl

div? then is simply

_div?_ : ? {m} -> ? -> Is (suc m) -> ?
n div? im = length (iter-sub n im)

And a version similar to the one in the Data.Nat.DivMod module (only without the Mod part):

_div_ : ? -> (m : ?) {_ : False (m ? 0)} -> ?
n div  0      = λ{()}
n div (suc m) = n div? (! (suc m))

Some tests:

test-3 : map (λ n -> n div 3)
           (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
         ≡ (0 ∷ 0 ∷ 0 ∷ 1 ∷ 1 ∷ 1 ∷ 2 ∷ 2 ∷ 2 ∷ 3 ∷ [])
test-3 = refl

Note however, that the version in the standard library also contains the soundness proof:

property  : dividend ≡ to? remainder + quotient * divisor

The whole code.