Как определить оператора деления в Агде?

Question

Я хочу разделить два натуральных числа. Я сделал функцию, как это

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

Пожалуйста помоги.

Answer 1

Как говорит @gallais, вы можете явно использовать обоснованную рекурсию, но мне не нравится этот подход, потому что он абсолютно нечитабелен.

Этот тип данных

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

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

позволяет поднять значения до уровня типа, например, вы можете определить тип-сейф pred функция:

pred⁺ : ∀ {n} -> Is (suc n) -> ℕ
pred⁺ = pred ∘ ¡

затем

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

проверки типов, в то время как

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

не делает. Можно определить вычитание с положительным вычитаемым (чтобы обеспечить правильность) таким же образом:

_-⁺_ : ∀ {m} -> ℕ -> Is (suc m) -> ℕ
n -⁺ im = n ∸ ¡ im

Затем, используя материал, который я описал здесь, вы можете многократно вычитать одно число из другого, пока разница не станет меньше второго числа:

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

Например

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⁺ тогда просто

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

И версия, аналогичная той, что в Data.Nat.DivMod модуль (только без Mod часть):

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

Некоторые тесты:

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

Однако обратите внимание, что версия в стандартной библиотеке также содержит доказательство надежности:

property  : dividend ≡ toℕ remainder + quotient * divisor

Весь код

Answer 2

Деление обычно определяется как повторное вычитание, которое требует немного необычного принципа индукции. Смотрите, например, определение в стандартной библиотеке.