問題タブ [coq]

Coqがこれを受け入れないのはなぜですか？

ID と構成を提供するクラスを定義しようとしています。他の便利なインスタンス (nil と連結を含むリスト; ID と合成との関係 ;-) ) に加えて、関数のインスタンスが必要です。

与えられた

のようなものを定義できるようにしたい

しかし、Coq の演算子はそのようには機能しません。最初->は表記だと思いLocate "_ -> _".ましたが、これはUnknown notation. ちょっとうまくいきfun a b => a -> bますが、後で型がおかしく見えます。

(同じことが にEval compute inも当てはまります。型を単純化していないようです。)より読みやすいidentity nat : nat -> nat. （現在、私がやっていることの型は読めなくなります。）

「生」を取得する方法、->または少なくともCoqにもっと良い型を与えるよう説得する方法はありますか?

補足: 私はInductive評価セマンティクスを表す多くの を構築しています。私の目標は、「通常の」プログラミング言語のサブセットを Coq にマッピングして戻し、セキュリティ制約を転送し、魔法をかけることです。私は同じことを異なるコンストラクターで何度も何度も証明することを余儀なくされています。これにより、一度だけ証明できるようになることを願っています。カテゴリはこれを抽象化する正しい方法だと思います。私が間違っている場合に備えて、このメモをここに含めます->。問題全体を回避するより良い方法があるかもしれません。

私の現在のプロジェクトでは、Java と Coq を使用しています。Mavenを使用して、継続的インテグレーションをセットアップしました。その一部としてcoqファイルをチェックしたい。つまり、次のものが必要です。

• インストールされていない場合は、coq をダウンロードしてローカルにインストールします (maven が gwt などのフレームワークで行うように)。
• coq ファイルが正しいことを確認する

誰かがこれを設定しようとしましたか？これはどのように行うことができますか？

を証明しようとしていますがP ?x、ここでP : A -> Propと?x : Aは存在変数です。を証明できるので、 に一般化するforall a:A, P a必要があります。P ?xforall a:A, P a

?x がインスタンス化された変数 x である場合、単純に を使用generalize xして を生成できforall x:A, P xます。しかし、試してみるとgeneralize ?x、Coq は構文エラーを返します。

これは可能ですか？私が調べたところ、Coq は、存在変数に関するステートメントを一般化する直感的な方法を提供していないようです。

どんな助けでも大歓迎です。

ここで問題が発生します。p（a、a、a）-> p（fa、a、fa）が必要です。これは、すべてのx、すべてのy、すべてのz、p（x、y、z）から明らかです。 > p（fx、y、fz）x、yおよびz = aをインスタンス化する必要がありますが、できません。私がすることはここでは受け入れられません。

エラーが発生します：戦術的な失敗:(引数は全称記号ではないか、目標に適合しません）。

all_e（all x、all y、all z、p（x、y、z）-> p（fx、y、fz））を試してみると。エラー：戦術的失敗:(議論は全称記号ではありません）。

手伝ってもらえますか？私はCoqの情報をあちこちで掘り起こし、PDFを印刷し、試しましたが、それでもCoqの構文とロジックの流れを理解することができず、まだかなり迷っています。

ポインタを事前に感謝します！

見つかった解決策：

Coq には次の定理がありますTheorem T : exists x:A, P x.。この値を後続の証明で使用できるようにしたいです。IE私は次のようoなことを言いたいです:P ooT

どうすればいいですか？前もって感謝します！

私の証明スクリプトは、矛盾する目標を解決するために使用する必要がある、nat = boolまたは のようなばかげた型の等価性を与えてくれます。nat = list unit

通常の数学では、これは些細なことです。与えられたセットbool := { true, false }と nat := { 0, 1, 2, ... }私はそれを知っていますtrue ∈ boolがtrue ∉ nat、したがってbool ≠ nat. Coqでは、それをどのように述べればよいかさえわかりませんtrue :̸ nat。

質問

これらの等式が偽であることを示す方法はありますか? それとも、それは不可能ですか？

(編集: 失敗した試行の長いリストを削除しましたが、履歴で引き続き表示できます。)

単純型付きラムダ計算で型付きラムダ計算が一意であるという証明は、紙の上では簡単です。私が精通しているという証拠は、タイピングの派生に関する完全な帰納法によって進められます。ただし、タイピング派生のタイプで表されるタイピング派生が一意であることを証明するのに苦労しています。dec Γ x τここで、変数のxタイプτがenvironmentの場合、述語はtrueですΓ。型付き述語Jは通常どおりに定義され、単純型付きラムダ計算の型付き規則を読み取るだけです。

Jタイピングの派生が一意であることを証明するときに、タイプの用語の構造を公開するのに問題があります。たとえば、私は次の補題のいずれd1かで誘導することはできますが、その後破壊して逆に誘導することはできません。Coqによって表示されるエラーメッセージ（用語を抽象化すると、タイプが正しくない用語になります）は少しわかりにくく、Coqwikiは何の助けにもなりません。参考までに、これは私が証明しようとしている見出語です。d2d1d2

タイプがユニークであることを証明するときなど、用語を導入するときに問題はありません。

編集：問題が発生した結果を示すために必要な最小限の定義を追加しました。huitseekerのコメントに応えて、J抽出などの操作を実行し、Coqでこれまで行ったことのない一意性などの結果を証明するために、派生を構造化オブジェクトとして入力することについて推論したかったので、この種が選択されました。

コメントの最初の部分に応じて、またはのinductionいずれd1かd2で実行できますが、実行後は、、、または残りの用語をinduction使用できません。これは、両方の構造を公開することはできず、両方のプルーフツリーについて推論することはできないことを意味します。私がそうしようとしたときに私が受け取るエラーは、残りの用語を抽象化すると、タイプが正しくない用語につながることを示しています。destructcaseinductiond1d2

ライブラリdependent inductionからいくつかの結果を試してみましたが、成功しませんでした。Coq.Logic派生がユニークであるということは、証明するのが簡単な命題であるように思われます。

私は関数" HF"を持っていますセクション内にタイプがありますS

補題を書きたい：

どこ

セクション内にこの関数があればOKSです。

incl_flしかし、セクションの外に関数を書きたいと思いSます。HFこれが外側のセクションのタイプですS。

""でエラーが発生しましたHF：

arityこの関数" "にを追加する場所を見つけようとしましたが、HF成功しません。incl_flセクションの外に見出語""を書くのを手伝ってくれませんSか。どうもありがとうございます。

ある意味で「互換性がある」必要があるリストのタイプがあります。

ただし、次の理由から、このコードはあまり好きではありません。

1. モジュラーではありません: アドホック リスト データ コンストラクターは、本質的に、先頭と末尾が互換性があるという証明 (タグ) と結合されています。
2. コードの再利用を好まない: 通常のリスト関数 (リスト連結など) を再定義し、通常のリスト定理 (リスト連結の結合性など) を再証明する必要があります。

私は、次の 3 つのステップからなる別のアプローチを念頭に置いています。

1. タグ付けされた要素の単一のタイプを定義する (タグ付けされたタイプの要素のファミリとは対照的に):

   /li>

2. タグ付けされた要素の任意の (つまり、有効または無効な) リストのタイプを定義します。

   /li>

3. タグ付けされた要素の有効なリストを、要素がタグ付けされた要素の任意のリストであり、要素が隣接する要素と互換性があることの証明であるタプルとして定義します。

   /li>

Coq で 3 番目のステップを実行するにはどうすればよいですか?