問題タブ [coq]

私はCoqが初めてです。単位、積、合計を使用してリスト、マップ、ツリーを定義するのに問題があります。タイトルのエラーメッセージが表示されます。コメントの上のコードは正常に機能しますが、その下のコードは機能しません。

編集 4 : これは、実際には一般的な TTY 入力の制限にすぎないことがわかりました。問題の原因となっている OCaml、Coq、または Emacs については特に何もありません。

Emacs で Proof General を使用して Coq プログラムに取り組んでいますが、入力が長すぎるバグを発見しました。Proof Generalを介して送信する領域にcoqtop1023 文字を超える文字が含まれている場合、Proof General (Emacs ではありません) は応答を待っている間にハングし、*coq*バッファーには^G1023 文字を超える文字ごとに 1 つの余分な文字が含まれます。たとえば、1025 文字の場合region が に送信されたcoqtop場合、*coq*バッファは 2 つの余分な文字で終了し^G^Gます。ファイルのこのポイントを超えて先に進むことができず、coqtopプロセスを強制終了する必要があります (C-c C-xまたはターミナルからkill/を使用killall)。

この制限に関する何かは、coqtopそれ自体から生じます。1024文字以上の文字列を生成し、それをパイプする場合

その後、すべて正常に動作します。(同様に、正常にcoqc動作します。) しかし、ターミナルで実行するcoqtopと、1 行に 1024 文字を超える文字を入力できません。これには、最後の改行文字が含まれます。したがって、1023 文字の行を入力してから改行を押すと機能します。しかし、1024 文字を入力した後、return を含む (delete などは含まない) 任意のキーを押しても、ビープ音が鳴るだけです。そして、ocaml(OCaml トップレベル) が同じ動作をすることがわかりました:

ocaml正常に動作しますが、端末から実行している場合、1 行に 1024 文字を超える文字を入力できません。私の理解ではcoqtop、OCaml のトップレベルに依存しているため (より明らかに as として実行した場合coqtop -byte)、これは関連する制限であると思います。

関連するソフトウェア バージョンは次のとおりです。

• HomebrewのOCaml 3.12.1 ;
• HomebrewのCoq 8.3pl3 (および 8.3pl2) ;
• 証明 一般4.1;
• Emacs for Mac OS XからのGNU Emacs 24.1.1のビルド。と
• Mac OS X 10.6.7。

そして私の質問は次のとおりです。

• この文字数制限の実施ocamlについてはどうですか? coqtopそして、なぜパイプやファイルからの入力ではなく、端末や Emacs からの入力だけなのですか?
• Proof General がこの制限を (明らかに) 無知であるために、エラーがハングしたり、謎^Gの s が発生したりするのはなぜですか?
• この制限を回避するにはどうすればよいですか? 私の最終目標は、Proof General/Emacs 内で Coq を使用することなので、根本的な問題を回避する回避策は問題ありません。

編集 3: 1024 文字の入力制限が Ocaml トップレベルにも存在することを発見した後 (関連していると思われるもの)、その情報を追加し、元の問題の説明を削除しました。(必要に応じて編集履歴を参照してください)。

したがって、サブゴールに誤った仮説があります。これは、異なるコンストラクター間の同等性です。サブゴールを終了するにはどうすればよいですか？

文字列の「再帰性」プロパティを証明したいと思います。証明の進め方を教えていただけませんか。これが私のコードです：

私は定理 T とその証明、そしてそれを証明するために使用される無数の補題を持っています。

補題を非表示にして、定理だけを利用できるようにしたいと思います。主な理由は、補題の適切でグローバルな名前を考える必要がないからです。

定理、その証明、および補題を、モジュール タイプで制限されたモジュールに配置して、定理のみを使用可能にすることはできますか?

何かのようなもの：

もしそうなら、誰かが投稿したり、簡単な例を教えてもらえますか?

Coqを使用して、自由変数、たとえばn:Uが項/式eに存在するかどうかを取得/チェックする関数/コマンドはありますか? 共有してください。

たとえば、この「n は e の自由名には現れない」と Coq で述べたいと思います。

ありがとう、

ウィラヤット

Coqのドキュメントには、組み込みの命名メカニズムに依存しないように一般的な警告が記載されていますが、命名メカニズムの変更によって過去の証明が無効にならないように、自分の名前を選択してください。

フォームの式を検討するときはremember Expr as v、変数vを式に設定しますExpr。しかし、仮定の名前は自動的に選択され、のようなものなので、次Heqvのようになります。

Heqv: v = Expr

代わりに自分の名前を選択するにはどうすればよいHeqvですか？コマンドを使用していつでも好きな名前に変更できますがrename、Coqに組み込まれている名前付けメカニズムの将来の変更に関係なく証明を維持することはできません。

誰かがZ3とcoqの違いを教えてくれるかどうか疑問に思っていますか？coqは、ユーザーが証明手順を入力する必要があるという点で証明アシスタントであるように思われますが、Z3にはその要件がありません。しかし、coqにもZ3と同様の自動戦術があるようです。それとも、coqの証明検索機能はZ3ほど強力ではありませんか？

coq命題（またはそのようなもの...）から証人を抽出しようとしています。

私は次のようなものを持っています

(これは後で証明され、明示的な型でatom:

そのようなものを抽出するにはどうすればよいxですか? ドキュメンテーションによると

そのような (exist xp) から、その証人 x:A を抽出することができます (match などの消去構造を使用)。

しかし、私はこれがどのように機能するのかわかりません....

それはまた言います

A:Type と P:A->Prop を指定すると、構造 {x:A | P x} はタイプです

Parameter C : {x : atom | x \notin xs}しかし、次のようなことを試してみると、

と と の 2 つの関数があるfとgしf = gます。共通のドメイン内f a = g aの一部のコンテキストに追加できる、前方推論の「関数適用」戦術はありますか? aこの不自然な例ではassert (f a = g a)、f_equal. しかし、私はもっと複雑な状況でこのようなことをしたいと思っています。例えば、