問題タブ [totality]

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

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

Stepsそして与えられた と のペアについてdを計算する再帰関数を書きますn:

ただし、steps再帰呼び出しが十分に根拠のある明確な理由がないため ( と の間qに構造的な関係がないため)、 は合計として受け入れられませんn。

しかし、私にも機能があります

退屈な証拠で。

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

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issuesには、次のように記載されています。

第 2 に、現在の実装ではこれまでの努力が限定的であったため、関数が total であると信じているがそうではない場合が依然としてある可能性があります。まだ証明のためにそれを当てにしないでください!

これは Idris を証明に当てにできないということですか、それとも全体性チェッカーを必要としない証明を作成する方法はありますか?