Доказательство теоремы в Coq

Я пытаюсь доказать теорему в 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, поэтому я не знаю, что это на самом деле означает. Я провел некоторые исследования в Интернете, но мне не удалось найти решение. У кого-нибудь есть представление о том, из-за чего возникает эта проблема?

Источник

2 ответа

Решение

Вы разрушили гипотезу, поэтому вы уже анализируете каждый случай.

использование left а также right манипулировать дизъюнкцией в заключении, и assumption когда гипотеза и заключение совпадают.

Источник

РЕДАКТИРОВАТЬ: Хм... я мог неправильно понять, что вы пытались сделать здесь на самом деле...

Case То, что вы используете и, вероятно, видели в другом месте, не встроено в Coq, а скорее является библиотекой, которая плавает в экосистеме Coq.

Я могу найти ссылку на это здесь: http://coq.inria.fr/cocorico/Case%20(tactic)

Я также использовал это лично. Чтобы использовать его, вам нужно либо скопировать определение в этой ссылке где-то в вашем файле, либо в другом файле MyCaseModule.v что вы импортируете тогда:

Require Import MyCaseModule.

Как примечание, Coq 8.4, кажется, предлагает другой способ структурирования доказательств с использованием маркеров. Я не знаю точных деталей, так как я застрял, используя 8.3 по другим причинам. Тем не менее, вы все равно можете предпочесть Case/SCase/... за его способность давать имена различным случаям.

Источник
Другие вопросы по тегам