在证明存在性陈述之后，为该定理的某些见证者引入一个常数符号通常在符号上很方便。
作为一个简单的例子，编写起来要简单得多（以典型的数学符号表示）
?x. ? ? x.
比写
?x. ?y. empty(y) and y ? x.
我希望在Coq中复制这种效果。这是我遇到的基本情况以及导致错误的尝试（现在在真实的Coq代码中）：
Variable A:Type.
Hypothesis inhabited: exists x:A, x=x.
Definition inhabitant:A.
destruct inhabited.
(*Error: Case analysis on sort Type is not allowed for inductive definition ex.*)
我想知道此错误消息的含义，以及是否有任何方法可以解决此问题。谢谢！
在Coq标准库中我可以找到一个说明inl并inr注射的引理吗？也就是说forall (A B : Type)(x y : A), inl B x = inl B y -> x = y,并且类似于右手情况.我自己没有问题证明这一点,但这些似乎是非常有用和重要的引理,我必须想象它们已经在某个地方的标准库中了.
假设我有一个包含10个元素的简单枚举类型:
data Test = A | B | C | D | E | F | G | H | I | J
deriving Eq
GHC Eq按照您的预期派生实例:
==================== Derived instances ====================
Derived class instances:
instance GHC.Classes.Eq Test.Test where
(GHC.Classes.==) (Test.A) (Test.A) = GHC.Types.True
(GHC.Classes.==) (Test.B) (Test.B) = GHC.Types.True
(GHC.Classes.==) (Test.C) (Test.C) = GHC.Types.True
(GHC.Classes.==) (Test.D) (Test.D) = GHC.Types.True
(GHC.Classes.==) (Test.E) (Test.E) = GHC.Types.True
(GHC.Classes.==) (Test.F) (Test.F) = GHC.Types.True
(GHC.Classes.==) (Test.G) (Test.G) = GHC.Types.True
(GHC.Classes.==) (Test.H) (Test.H) = GHC.Types.True
(GHC.Classes.==) …