0

Coqで定理を証明しようとしていますが、発生した問題を解決できません。私は解決しようとしています：

 forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
Proof.
intros.
destruct H as [H1 | [H2 | H3 ]].
Case H1.
and in this last line I get the following error "Error: The reference Case was not found in the current environment."

私はCoqを初めて使用するので、それが実際に何を意味するのかわかりません。私はインターネットでいくつかの調査をしましたが、解決策を見つけることができませんでした。この問題が何から来ているのか誰かが知っていますか？

4

2 に答える 2

2

仮説を破棄したので、すでに各ケースを分析しています。

leftとを使用rightして、結論の論理和を操作しassumptionます。仮説と結論が同じ場合。

于 2012-11-25T15:23:48.373 に答える
1

編集:うーん...私はあなたがここで実際にやろうとしていたことを誤解したかもしれません...

あなたが使用していて、おそらく他の場所で使用されているのを見たことのCaseある は、Coq でビルドされたものではなく、Coq エコシステム内に出回っているライブラリです。

ここで参照できます：http://coq.inria.fr/cocorico/Case%20(tactic )

私も個人的に利用させていただきました。それを使用するには、そのリンクの定義をファイルのどこかにコピーするか、MyCaseModule.v次にインポートする別のファイルにコピーする必要があります。

Require Import MyCaseModule.

補足として、Coq 8.4 では、箇条書きを使用して証明を構造化する別の方法が提供されているようです。他の理由で 8.3 を使っているので、詳細は正確にはわかりません。ただし、さまざまなケースに名前を付ける機能があるため、Case/SCase/... を好む場合もあります。

于 2012-11-26T03:01:14.940 に答える