3

d ≥ 2でn > 0の自然数があるとします。この場合、 nからdを分割して、n = m * d kを取得できます。ここで、mはdで割り切れません。

このd分割可能な部分の繰り返しの削除を再帰スキームとして使用したいと思います。だから私はmStepsにつながるデータ型を作ると思った:

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)

退屈な証拠で。

合計であるとイドリスに説明するためwfに の定義で使用できますか?stepssteps

4

1 に答える 1

2

これは、十分に根拠のある再帰を使用して、求めていることを実行する 1 つの方法です。しかし、もっと良い方法があることは確かです。以下では、目標を達成できる標準LT関数を使用しますが、回避する必要がある障害がいくつかあります。

残念ながら、は関数であり、型コンストラクターやデータ コンストラクターではありません。つまり、 の 型クラスLTの実装を定義することはできません 。次のコードは、この状況の回避策です。WellFoundedLT

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にしました。divModcontrib/Data/Nat/DivMod/IteratedSubtraction.idr

完全なコードはこちらから入手できます。

警告: 合計チェッカー (Idris 0.99 のリリース バージョン) は合計として受け入れませんsteps。これは最近修正され、私たちの問題に対して機能します (Idris 0.99-git:17f0899c でテストしました)。

于 2016-12-20T20:57:14.377 に答える