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

Question

我很高兴向 Coq 介绍自己。现在我一直在做关于枚举的证明:

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

EQUAL、GREATER 和 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 模式魔法。

最好的，五、