この戦術を使用してdestruct、場合によってステートメントを証明したいと思います。オンラインでいくつかの例を読みましたが、混乱しています。誰かがそれをよりよく説明できますか？

以下に小さな例を示します (解決する方法は他にもありますが、 を使用してみてくださいdestruct)。

現在、オンラインのいくつかの例では、次のことを提案しています。

その場合、次のようになります。

そこで、最初の 2 つのケースが不可能であることを証明したいと思います。しかし、マシンはそれらをサブゴールとしてリストし、私にそれらを証明することを望んでいます... これは不可能です.

まとめ: 不可能なケースを正確に破棄するには?

使用例をいくつか見inversionましたが、手順がわかりません。

最後に、補題がいくつかの帰納型に依存していて、それでもすべてのケースをカバーしたい場合はどうなりますか?

H私はローカルコンテキストで仮説を立てています。それをの形式と呼びましょうtrue=true -> conclusion。前提を破棄して結論のみを保持するために使用できる戦術はどれですか？

私はCoqでコードを記述し、このコードを抽出して大規模なHaskellプロジェクトで使用することを検討しています。Coqで単一のモジュールを構築し、プロパティを証明してから、Haskellのモジュールシステムを使用して、これらのプロパティの違反を（スマートコンストラクターを介して）防止したいと思います。

明示的なエクスポートリストを使用してCoqコードをHaskellモジュールに抽出できるという兆候は見つかりません。抽出されたCoqコードを手動で変更する必要があるようです。これは大したことではありませんが、この権利があるかどうかを知りたいと思います。誰か別の提案がありますか？

Coqのモジュールから定義をインポートするのに問題があります。Coqは初めてですが、言語のリファレンスマニュアルまたはオンラインチュートリアルを使用して問題を解決できませんでした。有限集合の署名と公理を定義するモジュールがあり、これを別のモジュールに実装する予定です。それだけではありませんが、次のようになります（参考までに、有限オートマトンに関するFilliatreの論文を厳密にフォローしています）。

を使用してモジュールをコンパイルし、コマンドを使用して、またはなどcoqcの別のモジュールにロードしようとします。モジュールをインポートしようとすると、Coq（Proof General経由）が警告を発行します。FinSetListFinSetRBTRequire Import FinSet

さらに、で定義されているものが表示されませんFinSet。あるモジュールから別のモジュールに定義（この場合は公理）をインポートするにはどうすればよいですか？私は基本的に、Pierceの「SoftwareFoundations」講義で概説されている手順に従いました。しかし、彼らは私のために働いていません。

ListSetCoq標準ライブラリのモジュールを使用しています。証明の条件について推論する方法がわかりません。たとえば、次の証明に問題があります。コンテキストの定義が提供されています。

現在の証明状態にはinr、Aeq_dec仮説としてのが含まれています。inl帰納の基本ケースとのAeq_decが真である帰納ケースを破棄しました。

真であるための唯一の方法はH、真であるa <> x場合set_mem xsです。を取得するためにH、に条件を適用できるはずです。しかし、私はこれを行う方法を理解していません。条件を処理、分解、または適用するにはどうすればよいですか？a <> xset_mem xs

.v検証用ですか？検証？vamanos？

.coq拡張機能を使用してみませんか？

[これがスタック オーバーフローに適しているかどうかはわかりませんが、ここには他にも多くの Coq に関する質問があるので、誰かが助けてくれるかもしれません。]

私はhttp://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28 (Case が導入されている場所のすぐ下) から次の作業を行っています。私はこれの完全な初心者であり、自宅で作業していることに注意してください-私は学生ではありません.

そして、私は書き換えが何をするかを見ています:

次にrewrite <- H.適用されます。

そして、証明がどのように成功するかは明らかです。

機械的な方法でシンボルを操作するという観点から、どのように証明に到達しているのかがわかります。それはいいです。しかし、私は「意味」に悩まされています。false = true特に、証明の途中でどうやって持つことができますか?

何か矛盾した議論をしているようですが、よくわかりません。やみくもにルールに従っていて、どういうわけかナンセンスなタイピングをしているように感じます。

私は上で何をしていますか？

質問が明確であることを願っています。

型クラスを使用して、代数構造の階層を Coq で簡単に構築できます。型クラスの Coq の構文とセマンティクスに関するリソースを見つけるのに苦労しています。しかし、私は以下が半群、モノイド、可換モノイドの正しい実装であると信じています:

Monoid私の理解が正しければ、最初に のインスタンスを宣言しSemigroup、次に をパラメータ化することで、追加のパラメータ (モノイドの恒等要素など) を追加できますid : A。しかし、 のために構築されたレコードで奇妙なことが起こっていAbelianMonoidます。

これは、セミグループのクラスを作成しようとしたときに発生しました。次の構文が正しいと思いました。

ただし、正しい演算子と ID 要素を明確にすることはできませんでした。レコードを印刷すると、上記の問題が明らかになりました。したがって、2 つの質問があります。まず、クラスを正しく宣言するにはどうすればよいですかMonoid。第二に、スーパークラスの関数をどのように明確にしますか?

私が本当に欲しいのは、時代遅れの構文なしで Coq の型クラスを明確に説明する優れたリソースです。たとえば、Hatton の本では、Haskell の型クラスが明確に説明されていると思いました。