在 coq 中，如何声明/证明枚举元素是不同的

Question

我很乐意向Coq介绍自己。现在我被困在做关于枚举的证明：

Inductive Comparison : Type :=
  | EQUAL
  | GREATER
  | LESSER.

EQUAL和MORE和LESSER是不同的（这似乎是文档所暗示的），还是仅通过上述代码无法确定？我不知道如何证明这一点。

Proposition comp_sanity: forall x : Comparison,
  x = EQUAL / x = GREATER -> False.
Proof.
intros x H_eqgr.

给我：

H_eqgr : x = EQUAL / x = GREATER
--------------------------------------------------
False

但后来我卡住了：

Coq> contradiction H_eqgr.
Error: Not a contradiction.

我应该在这里做什么才能拥有一个完全（明显）枚举的类型？

Answer 1

在你的情况下，我会选择discriminate战术而不是contradiction.简短的版本是：

Proposition comp_sanity: forall x : Comparison,
  x = EQUAL / x = GREATER -> False.
Proof.
now intros x [h1 h2]; subst; discriminate.
Qed.

翻译成

Proposition comp_sanity: forall x : Comparison,
  x = EQUAL / x = GREATER -> False.
Proof.
intros x hx.
destruct hx as [h1 h2].
rewrite h1 in h2.
now discriminate h2.
Qed.

没有intros图案魔法。

最好五.

Answer 2

contradiction策略除了尝试在您的上下文中查找类型为 False 的内容外，并没有做更多的工作。不幸的是，虽然您的上下文存在矛盾，但尚不清楚contradiction.

congruence策略执行更多的工作，并且理解，事实上，两个不同的构造函数是不相等的（我们说构造函数是不相交的）。

在这种情况下，这或多或少与调用subst传播关于x的等式相同，这导致一个假设EQUAL = GREATER，然后调用discriminate，这是一种在不同构造函数的相等中发现荒谬的策略。