错误“战术失败：关系（fun x y：BloodType => x <> y）不是声明的自反关系。”证明关于函数的定理

Question

我正在自学Coq并玩它。我想尝试编写一个基于两个等位基因计算血型的函数。但是，我收到一个错误“战术失败：该关系（fun x y：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.

因为我遇到以下错误：

“战术失败：关系（fun x y：BloodType => x <> y）不是声明的自反关系。也许您需要Coq.Classes.RelationClasses库。”

我尝试导入库，但是错误仍然相同。我对Coq并不陌生，所以我可能正在寻找一些很明显的东西。

Answer 1

问题的一部分是，您对推定谓词的推论与对直接谓词的推论不同。您必须在逻辑上重新考虑，然后才能期望Coq为您工作。

让我们回到一个非常基本的逻辑推论：“所有人都是凡人，苏格拉底是人，因此他是凡人”。如果我的猫是凡人，这是否意味着我的猫是人类？没有！当您进行否定运算时，问题就非常接近此。

现在，让我们集中解决您的问题。有一种特定的策略可以帮助证明相等性的基本实例reflexivity。还有一种特殊的策略可以帮助证明“不平等”的基本情况。此策略称为discriminate，它将在您的情况下起作用。

否定平等在您的锻炼中以两种不同的方式出现。有时，您需要证明肉眼可以看到的否定的等式，在这种情况下，discriminate可能会起作用。有时，您需要证明显然无法证明的否定的相等性（我尝试过以后会在练习中发生）。在那种情况下，进步的方法是发现目标中确实存在一个内在矛盾的假设，或者两个假设相互矛盾。在这种情况下，解决方案是尝试destruct H，其中H是明显错误的假设。

在锻炼时，您还需要了解如何应对假设中的or，destruct仍与该情况相关。

我建议您阅读免费文档（急着求助）[https://cel.archives-ouvertes.fr/inria-00001173v6/document]作为此教程。特别是，它解释说，对于每个逻辑结构，处理该结构的方式都不同，无论该结构是作为目标的结论还是作为假设出现的。对于最基本的推理步骤，有一个简短的表可以用作第一个提示列表。

[另一条建议：当您要定义的函数不是递归时，请不要使用Fixpoint命令。在这种情况下，应使用bloodType关键字定义功能Definition。使用Fixpoint会使定义变得毫无用处，这可能在以后的实验中给您带来困扰。

我很高兴看到您自己学习，玩得开心，并提出问题！