Ошибка «Ошибка Tacti c: отношение (fun xy: BloodType => x <> y) не является объявленным рефлексивным отношением». при доказательстве теоремы о функции - PullRequest
Новая
       3

Ошибка «Ошибка Tacti c: отношение (fun xy: BloodType => x <> y) не является объявленным рефлексивным отношением». при доказательстве теоремы о функции

0 голосов
/ 10 апреля 2020

Я сам изучаю Coq и играю с ним. Я хотел попробовать написать функцию, которая вычисляет группу крови на основе двух аллелей. Тем не менее я получаю сообщение об ошибке «Ошибка Tacti c: отношение (fun xy: BloodType => x <> y) не является объявленным рефлексивным отношением». при попытке доказать, что любая другая пара аллелей, кроме TypeO, не приведет к типу TypeO кровь.

Существует три аллеля: 

Inductive BloodTypeAllele : Type :=
  | BloodTypeA
  | BloodTypeB
  | BloodTypeO.

и четыре типа крови: 

Inductive BloodType : Type :=
  | TypeA
  | TypeB
  | TypeAB
  | TypeO.

Соотношение между ними выглядит следующим образом: 

Fixpoint bloodType (a b : BloodTypeAllele) : BloodType :=
  match a, b with
  | BloodTypeA, BloodTypeA => TypeA
  | BloodTypeA, BloodTypeO => TypeA
  | BloodTypeA, BloodTypeB => TypeAB
  | BloodTypeB, BloodTypeB => TypeB
  | BloodTypeB, BloodTypeA => TypeAB
  | BloodTypeB, BloodTypeO => TypeB
  | BloodTypeO, BloodTypeA => TypeA
  | BloodTypeO, BloodTypeB => TypeB
  | BloodTypeO, BloodTypeO => TypeO
  end.

Я могу доказать, что BloodTypeO и BloodTypeO результаты TypeO кровь. 

Theorem double_O_results_O_type :
  bloodType BloodTypeO BloodTypeO = TypeO.
Proof.
  reflexivity.
  Qed.

Но я не могу доказать, что любая другая комбинация не приведет к TypeO крови. 

Theorem not_double_O_does_not_result_O_type :
  forall (b1 b2 : BloodTypeAllele),
  b1 <> BloodTypeO \/ b2 <> BloodTypeO ->
  bloodType b1 b2 <> TypeO.
Proof.
  intros b1 b2 H.
  destruct b1.
  - destruct b2.
    + simpl. reflexivity.

, потому что я получаю следующую ошибку:

"Tacti c Ошибка: отношение ( fun xy: BloodType => x <> y) не является декларируемым рефлексивным отношением. Может быть, вам потребуется библиотека Coq.Classes.RelationClasses. "

Я попытался импортировать библиотеку, но ошибка осталась прежней , Я очень новичок в Coq, поэтому я, наверное, просматриваю что-то очень очевидное.

1 Ответ

1 голос
/ 10 апреля 2020

Одна часть проблемы заключается в том, что вы не рассуждаете с отрицанным предикатом так же, как вы рассуждаете с прямым предикатом. Вы должны снова подумать с точки зрения логики c, прежде чем ожидать, что Coq будет работать для вас.

Давайте go вернемся к очень основному c логическому выводу "Все люди смертны, Сократ - человек поэтому он смертен ". Если моя кошка смертна, значит ли это, что моя кошка - человек? Нет! Когда вы работаете с отрицанием, проблема очень близка к этому.

Теперь давайте сосредоточимся на вашей проблеме. Существует спецификация c tacti c, чтобы помочь доказать основные c случаи равенства reflexivity. Существует также спецификация c tacti c, чтобы помочь доказать базовые c случаи "неравенства". Эта тактика c называется discriminate, и она будет работать в вашем случае.

Отрицание равенства проявляется в вашем упражнении двумя различными способами. Иногда вам нужно доказать отрицание равенства, которое очевидно невооруженным глазом, и в этом случае discriminate может выполнить эту работу. Иногда вам нужно доказать отрицание равенства, которое явно недоказуемо (я попробую это позже). В этом случае путь к прогрессу состоит в том, чтобы обнаружить, что в вашей цели есть предположение, которое на самом деле содержит внутреннее противоречие, или что две гипотезы противоречат друг другу. В этом случае решение состоит в том, чтобы попытаться destruct H, где H - гипотеза, которая явно неверна.

В случае вашего упражнения вам также необходимо понять, как справиться с or в гипотезе, destruct все еще будет иметь отношение к этому случаю.

Я предлагаю вам прочитать бесплатный документ (coq в спешке) [https://cel.archives-ouvertes.fr/inria-00001173v6/document] в качестве учебного пособия для это. В частности, это объясняет, что для каждой логической конструкции способ обработки этой конструкции различен, независимо от того, появляется ли конструкция в качестве вывода цели или в качестве гипотезы. Существует короткая таблица, которая будет использоваться в качестве первого списка подсказок для большинства базовых c этапов рассуждения.

Еще один совет: не используйте команду Fixpoint, когда вы используете функцию, которую вы sh определить не является рекурсивным. В вашем случае функция bloodType должна быть определена с использованием ключевого слова Definition. Использование Fixpoint делает определение бесполезно сложным, и это может укусить вас позже в ваших экспериментах.

Я рад видеть, что вы учитесь самостоятельно, развлекаетесь и задаете вопросы!

...