coq

1熱

1答えて

私はBenjamin Pierceの第1巻、Software Foundationsを使って作業していますが、IndPropの章のいくつかの問題を抱えています。残念ながら、私はより良い場所を知りません：誰もヒントはありますか？ Theorem leb_complete : forall n m, leb n m = true -> n <= m. Proof. (* FILL IN

2熱

1答えて

単純型のラムダ計算の閉じた項の自由変数の帰納仮説

単純な型のラムダ計算をCoqで形式化しようとしています。空のコンテキストは空です。これは正式化の関連部分です。 Require Import Coq.Arith.Arith. Require Import Coq.MSets.MSets. Require Import Coq.FSets.FMaps. Inductive type : Set := | tunit : type |

1熱

2答えて

簡体字中国人剰余定理をどのように証明できますか？

私は Theorem modulo_inv : forall m n : Z, rel_prime m n -> exists x : Z, (m * x == 1 [n]). Admitted. 私の質問は、（多分modulo_inv定理を使用して？）以下の証明を完了する方法であることを証明するために管理してきました。ここで Variables m n : Z. Hypothesis co

2熱

3答えて

機能マップの「折りたたみ」状態？

この質問は、ソフトウェアファンデーション、からインスピレーションを受けましたが、練習問題ではありません。私が知っていることは、これまでのところ。 Impの章（「簡単な命令プログラム」）では、シンプルな環境のための機能マップ（マップの章（「トータルマップとパーシャルマップ」）プログラミング言語。状態は、すべての割り当てで成長するので、インプの章のプログラムについて Inductive id : Ty

0熱

2答えて

CoqのXMLプロトコル文書の「editId」とは何ですか？

Coq's XML Protocol document (for the Add operation)には、<int>${editId}</int>と表示されています。ここでeditIDは何ですか？私はサイドバイトモードでcoqtopと対話できなかったため、これを尋ねました。例としてcoq-8.6.1/theories/FSets/FSetCompat.vを使用して、私は <call val="

2熱

1答えて

可変アリティを持つ戦術

と言っていいでしょう。clear_multiple H1, H2, H3.のようなことをするために、一度に複数の仮説をクリアするための戦術を持ちたいとします。私は、次のように、ペアを使用していることを実行しようとしました： Ltac clear_multiple arg := match arg with | (?f, ?s) => clear s; clear_multiple f | ?

0熱

1答えて

コック：不等式テスト

条件分岐のための簡単な構築物は、Coqの中平等テスト/ wがあります： Check ltac:(tryif unify 1 (S 0) then idtac "success" else idtac "fail"). (*success...*) は<および/または<=をテストするための同様の方法はありますか？

0熱

1答えて

疑問符のついたオペレータの仮説

私は過去数週間、Coq証拠アシスタントと協力してきましたが、今日は特別なことに遭遇しました。私はBenjamin Pierceの "Types and programming languages"の練習を通して練習中です。これらの演習のうちの1つでは、特定のホアレの3つ組が有効であるという自己製作プログラミング言語（Pier inの演習ではImp）を証明する必要があります。私はこの証拠をほぼ完成さ

1熱

2答えて

一意性述語の可否判定リスト

リストの一意性とその決定性機能の述語をCoqで定義したいと思います。私の最初の試みでした：ここ Section UNIQUE. Variable A : Type. Variable P : A -> Prop. Variable PDec : forall (x : A), {P x} + {~ P x}. Definition Unique (xs

1熱

1答えて

引数を減らす（とどのようなプログラム不動点である）

には、次の固定点を考えてみましょう：それは減少不動点を推測することはできませんので Require Import Coq.Lists.List. Import ListNotations. Inductive my_type: Type:= | Left: my_type | Right: my_type . Fixpoint decrease (which: my_type) (