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

Question

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

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

我很乐意看到完整的证明，但请避免“公开”发布，以免破坏软件基础类(class)中的练习。

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