coq

1熱

1答えて

私はcoqの関数型プログラミングにはまったく新しいので、coqの連続性のトポロジカルな定義を表現しようとしています。私はcoqのトポロジを定義するために codeを使用しています。特定の関数である特定の継続性を表現するのが私の最高の試み、 Definition Continuous (X:Type)(TX:Topology X)(Y:Type)(TY:Topology Y)(f:X->Y):=

0熱

1答えて

Coqで例外を発生させるにはどうすればいいですか？一致する場合は...

再帰的な定義を定義する必要がありますが、正しく行う方法はまだありません。したがって、私は、書かれたレベルの再帰レベルが必要な場合には、部分的に定義された関数を定義したいと考えています。 Context (qsigT: forall (A : Type) (P : forall a : A, Type), Type). Context (qpr1: forall (A : Type) (P :

1熱

1答えて

タイプのファミリーのための帰納的定義

私はしばらくの間これを苦労してきました。正規表現r:Exp私はrに関連付けられた言語を表現しようとしていますが与えられ、ここで Inductive Language : Exp -> Set := | LangLit : forall c:char, Language (Lit c) | LangAnd :

1熱

1答えて

は、タイプレベル

で書き換え私は、次の証明状態を持っている： 1 subgoals U : Type X : Ensemble U Y : Ensemble U f : U -> U g : U -> U pF : proof_dom_cod U X Y f pG : proof_dom_cod U X Y g fg : f = g H : proof_dom_cod U X Y g = proo

3熱

1答えて

Coqの製品タイプ

coqの製品タイプにパラメータを渡す際に問題があります。私はのように見えるの定義、 Definition bar (a:Type) := a->Type. が、私は彼らの製品/順序対を出力「A」と「バーA」とによって作られたもので受け取る関数を定義する必要があります。だから私は次のことを試みた。用語「b」は、それが型を持つことが予想される一方で、「タイプ」「バー」型を持つ私にエラーを与える

5熱

3答えて

をリストする - >リストA - > BOOL

私は自然に宣言リストの誘導述語に再利用可能なコードを記述しようとしているとき： Parameter A:Type. は、その後、私はバイナリ述語を定義するために進めた（用例： Inductive prefix : list A -> list A -> Prop := | prefixNil: forall (l: list A), prefix nil l | prefi

2熱

1答えて

私の機能が実際に再帰的であることをCoqにどのように納得させることができますか？

私は比較的シンプルな文脈自由文法（括弧の1つのタイプ）を解析するためにCoqにプログラムを書こうとしています。私の一般的なアルゴリズムはパーザが潜在的に残りの文字列を返すことです。たとえば、"++]>><<"を解析すると、CBTerminated [Incr Incr] ">><<"が返され、 "[++] >> < <"を解析するパーサーは、 ">> < <"を取得してそれを続行できます。明らか

3熱

1答えて

すべての公理を表示するCoq

私は私の証明で使われたすべての公理を見たいと思っています。このような情報を取得する最も簡単な方法は何ですか？使用するコマンドまたはスクリプトまたはツールはどれですか？私はすべての公理またはすべての使用された公理に興味があります。

1熱

1答えて

Coqの定理の高速計算

非常に単純な場合でもCoqが計算を終了するまで待たなければなりません。「非同期および並列プルーフ処理」については知っていますが、私のコードには固有の悪意があると思われますので、ガイドライン/プルーフのスタイリングのベストプラクティスに参考にしてください。例えば：は、代わりに定理の定義を使用するように使用コンパイラを試してみてください。 parrallel処理を使用します。より良いハードウ

2熱

1答えて

`{x：nat | '}という形式の（サブ）型を扱う最良の方法です。 x> = 13/\ x <= 19} `？

コックは私がこの定義できます： Definition teenagers : Set := { x : nat | x >= 13 /\ x <= 19 }. とも： Variable Julia:teenagers. ではなく： Example minus_20 : forall x:teenagers, x<20. か： Example Julia_fact1 : Julia >