nat-division-basic.agda

{- The following code gives the basic idea of division by repeated
   subtraction.  We have to ask Agda not to check termination of this
   function, because it is not structurally terminating.  The versions
   in nat-division.agda and nat-division-wf.agda correct this problem,
   and can be judged by Agda to be terminating. -}

module nat-division-basic where

open import bool
open import eq
open import nat
open import product
open import sum

{-# TERMINATING #-}
div : (x d : ℕ) → d =ℕ 0 ≡ ff → ℕ × ℕ
div 0 _ _ = 0 , 0
div x d p with (x < d)
div x d p | tt = 0 , x 
div x d p | ff with div (x ∸ d) d p
div x d p | ff | q , r = suc q , r 

test-div : ℕ × ℕ
test-div = div 17 3 refl