問題タブ [coq]

数式を入力して操作を実行できるが、数学的に有効な操作のみに制限するツール (GUI が推奨されますが、CLI が機能します) を探しています。また、ツールはセッションを保存し、保存された特定の一連の操作が有効であることを後で証明できる必要があります。

注:証明を生成するシステムを探しているのではなく、手動で指定した手順が有効であることを確認するだけです。

同様の操作にACL2を使用したことがありますが、一部のケースではうまく機能しますが、それ以外の場合は非常に使いにくいです。

この小さなプロジェクトが私のモチベーションです。方程式を解くことができる D テンプレート タイプです。この方程式を考えると：

シンボルのいずれかを不明として設定でき、その式を評価すると、その変数に割り当てられます。これは、式ツリーを型に組み込み、書き換え規則を使用してそれを未知の型に対応できるものに変換することによって機能します。

必要なのは、書き換えルールを検証する方法です。それらは、ある関係が真であり、別の関係も真であるというアサーションをテストすることによって検証できます。

Coq を試していますが、何をしているのか完全にはわかりません。は：

に相当：

編集：そうだと思います。

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

次の例を知っている人はいますか？

1. 証明アシスタント ( Coqなど) における正規表現(後方参照で拡張される可能性があります)に関する証明の開発。
2. 正規表現に関する従属型言語 ( Agdaなど) のプログラム。

coqでf、boolを受け入れてbooltrue|falseを返す関数true|false（以下に表示）を1つのboolに2回適用すると、true|false常に同じ値が返されることを証明するにはどうすればよいですかtrue|false。

たとえば、関数fは4つのことしか実行できません。関数の入力を呼び出しましょうb：

• 常に戻るtrue
• 常に戻るfalse
• Return b（つまり、bがtrueの場合はtrueを返し、その逆の場合）
• Return not b（つまり、bがtrueの場合はfalseを返し、その逆の場合はfalseを返します）

したがって、関数が常にtrueを返す場合：

関数が常にfalseを返す場合、次のようになります。

その他の場合は、関数がnot b

両方の可能な入力の場合、私たちは常に元の入力で終わります。関数がを返すと仮定した場合も同じことが言えますb。

では、これをcoqでどのように証明しますか？

Coqで次のことを証明しようとしています:

目標 (forall x:X, P(x) /\ Q(x)) -> ((forall x:X, P (x)) /\ (forall x:X, Q (x)))。

誰か助けてくれませんか？分割するかどうか、仮定などを行うかどうかはわかりません。

完全な初心者で申し訳ありません

私は定義された誘導型を持っています：

今、私はその誘導型の一連の特性を証明する必要がありますが、私は立ち往生し続けています。

誰かが私が前進するのを手伝ってもらえますか？

チューリング完全でない言語が世の中にあり、私が大学でComp Sciを勉強していなかったとすると、チューリング不完全言語（Coqなど）ではできないことを誰かが説明できますか？

それとも、実際の利害関係がない（つまり、実際にはあまり違いがない）完全性/不完全性ですか？

編集-私はあなたの線に沿って答えを探していますX、またはそのようなもののために非チューリング完全言語でハッシュテーブルを構築することはできません！

Coqで定義された次の Inductive 型があります。

natlist は基本的に自然数のリストです (Python のリストに似ています)。以下の定義を使用して、2 つの natlist の結合を見つけようとしています。

Definition union_of_lists : natlist -> natlist -> natlist

つまり Eval simpl in (union_of_lists [1,2,3] [1,4,1]) 、[1,2,3,1,4,1] を返す必要があります。

以下の疑問があります。

• この定義には引数がないため、実際に入力を取得して処理するにはどうすればよいでしょうか?
• 定義 union_of_lists は正確に何を返しますか? それはただのnatlistですか？

ヘルプやヒントは大歓迎です。

私は（古典的に）証明しようとしています

Coqで。私がやろうとしていることは、それを反対に証明することです。

私の問題は（2）行と（5）行にあります。Uの任意の要素を選択し、それについて何かを証明し、すべてを結論付ける方法を理解することはできません。

何か提案はありますか（私は対偶を使用することを約束していません）？