問題タブ [idris]

Coq ソースを Idris に変換するための有用なガイドラインは何ですか? 私が集めたものによると、Idris の組み込み戦術ライブラリは最小限ですが拡張可能です。

私が証明しようとしているのは、私の考えでは合理的な定理です。

帰納法による証明は、私がこれを証明する必要があるポイントに到達します:

これは、対話型証明器を使用して証明しようとすると (簡単にするために補題)、次のようになります。

マイナスの定義について何かが欠けているに違いないと感じたので、ソースで調べました。

私が必要とする定義はすぐそこにあります！minus left Z = left. 私の理解では、イドリスはここに置き換えるだけでよくminus m 0、mこれは反射的に真実です。私は何を逃したのですか？

依存型の有用性に関する卒業論文を書いています。ソートされたリストにのみ構築できるコンテナを構築しようとしているため、構築によってソートされていることが証明されます。

SMore先頭に追加される要素が、ソートされたリストの最小 (最初) の要素より小さいか等しいことを実行時に証明する必要があります。

sinsertソートされていないリストをソートするために、ソートされたリストを受け取り、要素を挿入してソートされたリストを返す関数を作成しました。

証明 ( ?iins21、?iins22) の作成に問題があります。助けていただければ幸いです。成り立たない仮定に頼っているのかもしれませんが、私にはわかりません。

また、ソートされたリストを構築するためのより良いソリューションを提供することをお勧めします (おそらく、ソートされているという証明値を持つ通常のリストですか?)

私は依存型に不慣れで、2 つの違いについて混乱しています。通常、型は別の型によってパラメーター化され、何らかの値によってインデックス付けされていると言う人がいるようです。しかし、依存型付き言語では、型と用語の間に区別はありませんか? パラメータとインデックスの違いは基本的なものですか? プログラミングと定理証明の両方で意味の違いを示す例を教えてください。

これをコンパイルしたい：

コンパイラは と統合できないため、これはコンパイルに失敗しnますn + m。これは for Vect の署名によるものであることは理解していますがtake、 if で統合できることをコンパイラに示す方法がわかりませんm = 0。

Haskell では、次のように記述できます。

Idris でそれを行わずに同等のものを書くことは可能ですかifThenElse(私の実際のケースは上記のものよりも複雑です)?