問題タブ [leon]

レオンで次のプログラムを試しました

結果 -- 成功

結果 -- 失敗 (終了していません)

システムが生産できないのはなぜですか?誰かが私を導くことができますか?

Inox / Welderでセットのいくつかのプロパティを証明したいのですが、その方法を理解するのに役立つ例がありません。証明したいとしましょう:

content(y::xs).contains(x) && x != y ==> content(xs).contains(x)

プロパティを定義します。

しかし、このプロパティは適切に定式化されていないため、コンパイルされないことが判明しました (明らかに間違った部分は .contains、&&、!==...)。

では、プロパティを定式化する正しい方法は何ですか? ここでは、コンテンツ関数が次のように定義されていると仮定しています。

証明の部分については、次の関数が与えられていると想像してください。

リストxsからxを削除し、それを証明したいと言うはずです

content(without(x,l)) == content(l) -- セット(x)

それを行う方法のスケッチを教えてもらえますか? SetDifferenceなどの BuiltInNamesを使用する必要がありますか?

楕円曲線の特定のプロパティを証明しています。そのために、フィールド操作を処理するいくつかの関数に依存しています。しかし、私は Inox がこれらの関数の実装について推論するのではなく、関数の特定のプロパティを仮定するだけにしたいと考えています。

たとえば、点の加算p1 = (x1,y1) and p2 = (x2,y2)が交換可能であることを証明しているとします。ポイントの追加を実装するには、そのコンポーネント (つまり、フィールドの要素) の追加を実装する関数が必要です。

追加は次の形になります。

この関数では、次のようなプロパティを指定できます。

whereは、この他の質問^+で示されている add に対応する中置演算子です。

展開中に Inox が何も想定しないようにボディに挿入する適切な式は何ですか?