如何在Agda中定义除法运算符？ [英] How to define division operator in Agda?

问题描述

我想分两个自然数。我做了这样的功能

  _ / _：N  - > N  - > frac 
 m / one = m / one 
（suc m）/ n = ??我不知道该写什么。 
  

Please help。

解决方案

这是@gallais说的，你可以明确地使用有根据的递归，但我不喜欢这种方法，因为它是完全不可读的。数据类型

  record是{α} {A：Setα}（x：A）：Setαwhere $ b $b¡ = x 
打开是
 
！ ：∀{α} {A：Setα}  - > （x：A）→>是x 
！ _ = _ 
  

允许将值提升到类型级别，例如，您可以定义类型安全 pred 函数：

  pred + +：∀{n}  - >是（成功） - > ℕ
 pred + = pred∘$ 
  

然后

  test-1：pred +（！1）≡0 
 test-1 = refl 
  

typechecks，而

 失败：pred +（！0） ≡0 
 fail = refl 
  

没有。可以用相同的方式定义减数与正减数（以确保充分发现）：

  _- +：：∀ {m}  - > ℕ - >是（成功） - > ℕ
n-+ im = n∸im im 
  

然后使用我描述的这里，你可以重复减去另一个数字，直到差值小于第二个数字：

  lem：∀{nm} {im：Is（suc m）}  - > m < n  - > n + 1 im  lem {suc n} {m}（s≤s_）=s≤'s（≤⇒≤'（n∸m≤mnn））
 
 iter-sub：∀{m}  - > ℕ - >是（成功） - >列表ℕ
 iter-sub n im = calls（λn  - > n-+ im）< -well-founded lem（_≤？_（im））n 
  
 
 $ b 
例如 
 
 
  test-1 ：iter-sub 10（！3）≡10∷7∷4∷[] 
 test-1 = refl 
 
 test-2：iter-sub 16（！4）≡16∷16∷ 12∷8∷4∷[] 
 test-2 = refl 
  
  div + 然后就是
 
 
  _div +_：∀{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 b $ b（0∷1∷2∷3∷4∷5∷6∷7∷8∷9∷[]）
≡（0∷0∷0∷1∷1∷1∷ 2∷2∷2∷3∷[]）
 test-3 = refl 
  
注但是，标准库中的版本还包含健全性证明： 
 
 
 属性：dividend≡toℕremaining + quotient * divisor 
  
整个代码。
 
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.
解决方案
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.

                        
这篇关于如何在Agda中定义除法运算符？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！