問題タブ [idris]

次のような式は、Idris では完全に有効です。

誰か次のような式を書いてくれませんか?

私はそれをコンパイルすることができないようです。

私はidrisにaaデータ型を持っています:

ユニティ、ラティス、グループ、およびその他のプロパティを持つリングであることを確認しました。

ここで、注入したステートメントの式を保持するオブジェクトを作成したいと思います。すべての操作を表す 4 つのカテゴリから始めたので、そこから適切な構文ツリーが得られます。例えば：

これは実際の表現ではありません。必要な醜い部分をいくつか取り除きましたが、達成しようとしていることのアイデアが得られます。上記は次と同等です。

データ型を 1 つに結合できることがわかりました。そこに到達するために、正しいクラス インスタンスを選択する関数を作成しました。

そのため、型内のすべてのものがこれら 4 つの操作のいずれかを表すことを保証できます。

次のように不平を言うでしょう：

ここで私の質問: データ型のオブジェクトが検証され、4 つの個別のデータ型が 1 つに結合されていることを確認するにはどうすればよいでしょうか。建設中にこれが真実であることを確認したいと思います。今は型クラスの解決が難しいことは理解できますが、イドリスには、後で構築中に解決できるようにしてもらいたいと思っています。これどうやってするの？

コードは実際には必要ありません。考え方の方向性には非常に満足しています。

私は Idris で実験してきましたが、2 つの異なる数値の間のすべての数値を表すために、ある種の型を指定するのは簡単なはずです。たとえばNumRange 5 10、5 から 10 までのすべての数値の型です。浮動小数点数ですが、整数で同じことを行うための型も同様に役立ちます。どうすればこれを行うことができますか？

ほとんどの証明アシスタントは、従属型を持つ関数型プログラミング言語です。プログラム/アルゴリズムを証明できます。代わりに、数学のみに最適な証明アシスタント (たとえば微積分) に興味があります。1つお勧めできますか？Mizar について聞いたことがありますが、ソース コードが閉じられているのは好きではありませんが、数学に最適な場合は使用します。Agda や Idris などの新しい言語は、数学的な証明にどの程度適していますか?

私は Idris と少し作業しており、確率の型を作成しました -とFloatの間の0.0s 1.0:

それらを乗算できるようにしたい：

p1 * p2それが常に確率であることをどのように証明できますか?

Idris version: 0.9.16

I am attempting to describe constructions generated from a base value and an iterated step function:

Using this I can define Plus, describing constructs from iterated addition of a jump value:

Simple example uses of this:

The following describes that values below the base are impossible:

And the following for values between base and jump + base:

I am having trouble defining the following function:

That is: if n isn't base plus a natural multiple of jump, then neither is jump + n.

If I ask Idris to case split m it only shows me IBase - then I get stuck.

Would someone point me in the right direction?

Edit 0: Applying induction to m gives me the following message:

Edit 1: Name updates and here is a copy of the source: http://lpaste.net/125873