3

假设我有一些自然数d ≥ 2和n > 0；在这种情况下，我可以从n中分离出d并得到n = m * d k，其中m不能被d整除。

我想使用这种重复删除d可分部分作为递归方案；所以我想我会为Steps通往m的数据类型：

import Data.Nat.DivMod

data Steps: (d : Nat) -> {auto dValid: d `GTE` 2} -> (n : Nat) -> Type where
  Base: (rem: Nat) -> (rem `GT` 0) -> (rem `LT` d) -> (quot : Nat) -> Steps d {dValid} (rem + quot * d)
  Step: Steps d {dValid} n -> Steps d {dValid} (n * d)

并编写一个递归函数，计算Steps给定对的d和n：

total lemma: x * y `GT` 0 -> x `GT` 0
lemma {x = Z} LTEZero impossible
lemma {x = Z} (LTESucc _) impossible
lemma {x = (S k)} prf = LTESucc LTEZero

steps : (d : Nat) -> {auto dValid: d `GTE` 2} -> (n : Nat) -> {auto nValid: n `GT` 0} -> Steps d {dValid} n
steps Z {dValid = LTEZero} _ impossible
steps Z {dValid = (LTESucc _)} _ impossible
steps (S d) {dValid} n {nValid} with (divMod n d)
  steps (S d) (q * S d) {nValid} | MkDivMod q Z _ = Step (steps (S d) {dValid} q {nValid = lemma nValid})
  steps (S d) (S rem + q * S d) | MkDivMod q (S rem) remSmall = Base (S rem) (LTESucc LTEZero) remSmall q

但是，steps不被接受为全部，因为没有明显的理由说明递归调用是有充分根据的（q和之间没有结构关系n）。

但我也有一个功能

total wf : (S x) `LT` (S x) * S (S y)

用一个无聊的证明。

我可以用towf的定义steps来向Idris解释那steps是total吗？

4

1 回答 1

2

这是使用有根据的递归来完成您所要求的事情的一种方法。不过我敢肯定，还有更好的方法。在接下来的内容中，我将使用标准LT函数，它可以让我们实现我们的目标，但是我们需要解决一些障碍。

不幸的是，LT是一个函数，而不是类型构造函数或数据构造函数，这意味着我们无法 WellFounded 为LT. 以下代码是针对这种情况的解决方法：

total
accIndLt : {P : Nat -> Type} ->
         (step : (x : Nat) -> ((y : Nat) -> LT y x -> P y) -> P x) ->
         (z : Nat) -> Accessible LT z -> P z
accIndLt {P} step z (Access f) =
  step z $ \y, lt => accIndLt {P} step y (f y lt)

total
wfIndLt : {P : Nat -> Type} ->
        (step : (x : Nat) -> ((y : Nat) -> LT y x -> P y) -> P x) ->
        (x : Nat) -> P x
wfIndLt step x = accIndLt step x (ltAccessible x)

我们将需要一些辅助引理来处理小于关系，这些引理可以在这个要点（Order模块）中找到。这是我最近开始的个人图书馆的一个子集。我确信可以最小化辅助引理的证明，但这不是我的目标。

导入Order模块后，我们就可以解决问题了（我对原代码稍作修改，不难改或者写一个包装器来拥有原来的类型）：

total
steps : (n : Nat) -> {auto nValid : 0 `LT` n} -> (d : Nat) -> Steps (S (S d)) n
steps n {nValid} d = wfIndLt {P = P} step n d nValid
  where
    P : (n : Nat) -> Type
    P n = (d : Nat) -> (nV : 0 `LT` n) -> Steps (S (S d)) n

    step : (n : Nat) -> (rec : (q : Nat) -> q `LT` n -> P q) -> P n
    step n rec d nV with (divMod n (S d))
      step (S r + q * S (S d)) rec d nV | (MkDivMod q (S r) prf) =
        Base (S r) (LTESucc LTEZero) prf q
      step (Z + q * S (S d))       rec d nV | (MkDivMod q Z     _) =
        let qGt0 = multLtNonZeroArgumentsLeft nV in
        let lt = multLtSelfRight (S (S d)) qGt0 (LTESucc (LTESucc LTEZero)) in
        Step (rec q lt d qGt0)

我以模块steps中的divMod功能为模型contrib/Data/Nat/DivMod/IteratedSubtraction.idr。

完整代码可在此处获得。

警告：整体检查器（从 Idris 0.99 开始，发布版本）不接受整体steps。它最近已修复并适用于我们的问题（我使用 Idris 0.99-git:17f0899c 对其进行了测试）。

于 2016-12-20T20:57:14.377 回答