coq

2熱

2答えて

私はCoqを試していますが、私は何をしているのか完全にはわかりません。です： Theorem new_theorem : forall x, P:Prop /\ Q:Prop 相当： ∀x (P(x) and Q(x)) 編集：私は、彼らがいると思います。

10熱

1答えて

coqでの紹介は？

私はCoqの中 ~ (forall t : U, phi) -> exists t: U, ~phi を証明する（古典的）にしようとしています。私がしようとしているのは、反抗的にそれを証明することです： 1. Assume there is no such t (so ~(exists t: U, ~phi)) 2. Choose arbitrary t0:U 3. If ~phi[t

1熱

1答えて

可能な入力の集合に対する制限付きのcoqにおける再帰関数定義

簡単に測定可能な引数を持たない再帰関数を定義する必要があります。私は使用された引数のリストを保持して、各引数が最大で1回使用され、入力スペースが有限であることを保証します。小節を使用すると、ほとんどが動作しますが、私は1つのケースで立ち往生します。 lの以前のレイヤーが正しく構築されているという情報が失われているようです。 e。重複はなく、すべてのエントリは実際に入力スペースからのものです。今

2熱

2答えて

Coqでリストを再帰的に検索する

リスト内のオブジェクトを検索しようとして、それが見つかった場合はtrueを返します。そうでなければfalse。しかし、私が思いついたのは間違っています。私は本当にいくつかの指導を感謝します。リストの先頭を要素と比較することで要素のリストを検索する機能が必要です。一致しない場合は、リストの残りの部分を再帰的に関数に渡して繰り返します。 Fixpoint find (li:list Interfac

4熱

4答えて

証明方法（forall x、P x） - （forall x、P x）

どのようにして証明するか（forall x、P x/\ Q x） - >（forall x 、P x）何時間も試していて、Coqが消化できるものに前例を分解する方法を理解することはできません。（私は明らかに、初心者くさいよ:)