没有可判定的相等性或排除中间值的鸽巢证明

在软件基础中IndProp.v https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab244一个人被要求证明鸽巢原理，并且可以使用排除中间，但有人提到这并不是绝对必要的。我一直试图在没有电磁场的情况下证明这一点，但我的大脑似乎是经典的。

问：如何证明该定理without使用排除中间？在无法轻易通过案例进行推理的情况下，人们通常应该如何处理没有可判定相等性的类型的证明？

我很乐意看到完整的证明，但请避免“以明确的方式”发布它，以免破坏软件基础课程中的练习。

该定义使用两个归纳谓词，In and 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.

    (* ??? *)     

我将描述引导我找到解决方案的思维过程，以防有帮助。我们可以应用归纳法，很容易简化到案例l1 = a::l1', l2 = a::l2'. Now l1'是一个子集a::l2'。我受过 EM 训练的直觉是以下之一成立：

• a is in l1'.
• a不在l1'.

在后一种情况下，每个元素l1' is in a::l2'但不同于a，因此必须在l2'. Thus 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.