問題タブ [coq]

関数を使用してメジャーを使用して再帰的定義を定義しようとしていますが、エラーが発生します：

ソースコード全体を一番下に投稿していますが、私の関数は

私は問題がforallsに起因することを知っています：それらをTrueに置き換えると、それは機能します。また、右側で含意（->）を使用すると、同じエラーが発生することもわかっています。Fixpointはforallsで機能しますが、メジャーを定義することはできません。

何かアドバイス？

約束通り、私の完全なコードは次のとおりです。

Coq Proof Assistant を使用して、(小さな) プログラミング言語のモデルを実装しています (Bruno De Fraine、Erik Ernst、Mario Südholt による Featherweight Java の実装を拡張しています)。このタクティックを使用する際に常に頭に浮かぶことの 1 つinductionは、型コンストラクターにラップされた情報をどのように保持するかということです。

次のように実装されたサブタイピング Prop があります。

はextendsJava で見られるクラス拡張メカニズムでtypあり、使用可能な 2 種類の型を表します。

型情報を保存したい場所の例は、次のようinductionな仮説で戦術を使用する場合です。

例えば

usingは、 およびinduction H.に関するすべての情報を破棄します。ケースはuvst_refl

ご覧のとおり、 とのコンストラクタに関連する情報、つまり に関連するu情報は失われます。さらに悪いことに、このために Coq はそれを見ることができず、実際にはこの場合は同じでなければなりません。vtypHtuv

Coqinversionでタクティックを使用すると、 とが同じであることがわかります。ただし、およびケースを証明するために生成される誘導仮説が必要なため、この戦術はここでは適用できません。Huvinductionst_transst_extends

コンストラクターにラップされているものに関する情報を破壊することなく、誘導仮説を生成し、等式を導出することの両方を組み合わせた戦術はありinversionますか? inductionまたは、必要な情報を手動で取得する方法はありますか? 両方とも、多くの変換が自動的に適用されることを示しています (特に を使用info inversion H) 。これらにより、私は建設と一緒に戦術を試してみましたが、進歩はありませんでした.info induction Hinversionchangelet ... in

コンストラクターとは何か、およびその仕組みの原則を理解するのに苦労しています。

たとえば、Coq では、自然数を次のように定義するように教えられています。

それはコンストラクターだと言われていますが、それSは正確にはどういう意味ですか?

私なら：

4であり、タイプであることがわかりnatます。

これはどのように機能し、Coq はそれが を(S (S (S (S O))))表していることをどのように認識し4ますか?

これに対する答えは、Coq の非常に巧妙なバックグラウンド マジックだと思います。

パラメータとしてセットがあります：

ここで、Qのサブセットである別のパラメーターを定義したいと思います。次のようなものです。

どうすればそれを定義できますか？後で公理として制限を追加できると思いますが、Fのタイプで直接表現する方が自然なようです。

非常に奇妙な構文を見てきました: (name:type1) type2 in type および [name:type] expr in expression は、Pi と Lambda の代替構文のように見えますが、数時間検索した後、ドキュメントには何も見つかりませんでした。すべて無駄に。

それは何を意味し、どこで定義されていますか? (使用例へのリンクが失われてしまい申し訳ありません)

私はCoqで遊んでいて、ソートされたリストを作成しようとしています。リスト[1,2,3,2,4]を取得して、次のような関数を返す関数が必要Sorted [1,2,3,4]でした。つまり、不良部分を削除しますが、実際にはリスト全体を並べ替えることはありません。

lesseqタイプの関数を定義することから始めようと思ったのですが(m n : nat) -> option (m <= n)、それからパターンマッチングをかなり簡単に行うことができました。多分それは悪い考えです。

私が今抱えている問題の核心はそれです（スニペット、下部の関数全体）

タイプチェックではありません。を期待していると書いてありますoption (m <= n)が、Some (le_n 0)タイプはoption (0 <= 0)です。mその文脈では明らかに両方とnがゼロであるため、私にはわかりませんが、 Coqにそのことを伝える方法がわかりません。

全体の機能は次のとおりです。

おそらく私は自分より進んでいて、これに取り組む前に読み続ける必要があります。

Coqコードが以下のコードで期待することを実行しない理由を理解するのに問題があります。

• 例をできるだけ単純化しようとしましたが、さらに単純化しても問題は発生しなくなりました。
• CompCert1.8ファイルを使用しています。
• これはCoq8.2-pl2の下で私に起こりました。

コードは次のとおりです。

これは動作しません：

失敗rewrite H1する：

ただし、これは機能します。

また、直後のeauto私の目標は次のようになります。

したがって、rewrite H1; discriminate2回は機能しますが、セミコロンを使用した後に「配管」することeautoはできません。

少なくとも問題が理にかなっていることを願っています。ありがとうございました！

完全なコード：

簡単に測定できる引数のない再帰関数を定義する必要があります。使用される引数のリストを保持して、各引数が最大 1 回使用され、入力スペースが有限であることを確認します。

メジャーを使用する(inpspacesize - (length l))とほとんどの場合機能しますが、1 つのケースで行き詰まります。の前のレイヤーが正しく構築されているという情報が欠落しているようですl。つまり、重複はなく、すべてのエントリは実際には入力スペースからのものです。

今、私は必要なことを行うリストの代替品を探しています。

編集これを次のように減らしました。

私はnat与えられたよりも小さい sを持ってmaxおり、関数がすべての数値に対して最大 1 回呼び出されるようにする必要があります。私は次のことを思いつきました：

要素を完全なリストに挿入できないことを帰納的に証明しようとすると、スタックし続けます (IH が使用できなくなるか、必要な情報を見つけることができません)。この挿入不可能性は終了を示すために重要だと思うので、私はまだ有効な解決策を見つけていません。

これを別の方法で証明する方法、または上記を再構築する方法についての提案はありますか?

リスト内のオブジェクトを検索しようとしていますが、見つかった場合はtrueを返します。それ以外の場合はfalse。

しかし、私が思いついたのは間違っています。いくつかのガイダンスを本当にいただければ幸いです。リストの先頭を関連する要素と比較して要素のリストを検索する関数が必要です。一致しない場合は、リストの残りの部分を関数に再帰的に配置し、リストの先頭を照合して繰り返します。

あなたの指導と援助は大歓迎です。

前もって感謝します

これは簡単な質問です。私はCoqが初めてです。

私は排他的な or in Coq を定義したいと思っています（私の知る限り、これは事前定義されていません）。重要な部分は、複数の命題 (Xor ABCD など) を許可することです。

次の 2 つのプロパティも必要です。

現在、定義されていない数の変数に対して関数を定義するのに問題があります。2 つ、3 つ、4 つ、5 つの変数 (必要な数) に対して手動で定義しようとしました。しかし、プロパティを証明するのは苦痛であり、非常に非効率的です。