Я хочу разделить два натуральных числа. Я сделал такую функциюКак определить оператор деления в Агда?
_/_ : N -> N -> frac
m/one = m/one
(suc m)/n = ?? I dont know what to write here.
Пожалуйста, помогите.
Я хочу разделить два натуральных числа. Я сделал такую функциюКак определить оператор деления в Агда?
_/_ : N -> N -> frac
m/one = m/one
(suc m)/n = ?? I dont know what to write here.
Пожалуйста, помогите.
Подразделение обычно определяется как итерационная подстановка, которая требует немного необычного принципа индукции. См. the definition in the standard library.
Как @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
нет. Можно определить вычитание с положительной вычитаемого (для обеспечения благополучия foundness) таким же образом:
_-⁺_ : ∀ {m} -> ℕ -> Is (suc m) -> ℕ
n -⁺ im = n ∸ ¡ im
Затем, используя вещи, которые я описал here, вы можете повторно вычитать одно число от другого, пока разница не меньше, чем второй номер:
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
Всего code.