如何在Agda中定义除法运算符？

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

typechecks,而

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

整个代码.