没有可判定相等或排中的鸽巢证明

Question

在软件基础IndProp.v中，要求证明鸽巢原理，并且可以使用排除中线，但是有人提到这不是绝对必要的。我一直试图在没有 EM 的情况下证明这一点，但我的大脑似乎是经典的。

问：不使用如何使用排中来证明定理？人们通常应该如何处理没有可判定相等性的类型的证明，在这种情况下人们不能轻易地通过案例进行推理？

我很乐意查看完整的证明，但请避免发布它 "in the clear"，以免破坏软件基础课程中的练习。

该定义使用了两个归纳谓词，In 和 repeats。

Require Import Lists.List. Import ListNotations. Section Pigeon. Variable (X:Type). Implicit Type (x:X). Fixpoint In x l : Prop := (*** In ***) match l with | nil => False | (x'::l') => x' = x \/ In x l' end. Hypothesis in_split : forall x l, In x l -> exists l1 l2, l = l1 ++ x :: l2. Hypothesis in_app: forall x l1 l2, In x (l1++l2) <-> In x l1 \/ In x l2. Inductive repeats : list X -> Prop := (*** repeats ***) repeats_hd l x : In x l -> repeats (x::l) | repeats_tl l x : repeats l -> repeats (x::l). Theorem pigeonhole_principle_NO_EM: (*** pigeonhole ***) forall l1 l2, length l2 < length l1 -> (* There are more pigeons than nests *) (forall x, In x l1 -> In x l2) -> (* All pigeons are in some nest *) repeats l1. (* Thus, some pigeons share nest *) Proof. (* ??? *)

Answer 1

一个可能的建设性证明是这样的：

我们通过对 l1 的归纳证明 pigeonhole_principle_NO_EM。由于长度限制，只有非空的情况是可能的。因此，假设 l1 = x :: l1'。现在，检查 l1' 中是否有某个元素被 f : (forall x, In x l1 -> In x l2) 映射到与 x 相同的成员证明。如果存在这样的 x' 元素，则紧随其后的是 x = x'，因此 l1 会重复。如果没有这样的元素，那么我们可以通过从l2中删除x映射到的元素得到l2'，并将归纳假设应用于l2'和适当的f' : forall x, In x l1' -> In x l2' 函数。

就是这样，但我注意到，根据给定的定义，实际上形式化此证明并不容易，因为我们需要证明异构或依赖等式，因为我们必须比较可能不同元素的成员资格证明。

关于掌握一般的构造性证据的窍门，一项重要的技能或习惯总是检查我们拥有什么样的数据，而不仅仅是我们知道什么样的逻辑事实。在这种情况下，成员资格证明实际上是指向列表的索引，与指向元素等于特定值的证明捆绑在一起。如果成员资格证明没有说明元素的确切位置，那么这个证明将无法建设性地实现。

Answer 2

我将描述引导我找到解决方案的思考过程，以防有帮助。我们可以应用归纳法，直接归结为 l1 = a::l1'、l2 = a::l2' 的情况。现在 l1' 是 a::l2' 的子集。我受过 EM 训练的直觉是以下之一成立：

a 在 l1'.
a 不在 l1'.

在后一种情况下，l1' 的每个元素都在 a::l2' 中，但不同于 a，因此必须在 l2' 中。因此 l1' 是 l2' 的子集，我们可以应用归纳假设。

不幸的是，如果 In 是不可判定的，则上面不能直接形式化。特别是如果给定类型的相等性不可判定，则很难证明元素不相等，因此很难证明像 ~(In a l1') 这样的否定陈述。但是，我们想用那个否定的陈述来证明一个肯定的陈述，即

forall x, In x l1' -> In x l2'

以此类推，假设我们要证明

P \/ Q
Q -> R
------
P \/ R

上面直观的说法就像是从P \/ ~P开始，在第二种情况下使用~P -> Q -> R。我们可以使用直接证明来避免 EM。

对列表进行量化 l1' 使这有点复杂，但我们仍然可以使用以下引理构建直接证明，这可以通过归纳法证明。

Lemma split_or {X} (l : list X) (P Q : X -> Prop) :
  (forall x, In x l -> (P x \/ Q x)) ->
  (exists x, In x l /\ P x) \/ (forall x, In x l -> Q x).

最后请注意，直观的鸽巢原理也可以形式化为以下方式，当类型具有不可判定的相等性时无法证明（注意它在结论中有否定陈述）：

Definition pigeon2 {X} : Prop := forall (l1 l2 : list X),
  length l2 < length l1 ->
  (exists x, In x l1 /\ ~(In x l2)) \/ repeats l1.

没有可判定相等或排中的鸽巢证明

Pigeonhole proof without decidable equality or excluded middle

coq