没有可判定的平等或排除中间的鸽子证明

Question

在软件基础IndProp.v中,要求一个人证明鸽子原则,并且可以使用被排除的中间人,但是提到它并不是绝对必要的.我一直试图在没有EM的情况下证明它,但我的大脑似乎是经典的.

问:如何在不使用排除中间的情况下证明该定理？一般来说,如果没有可判定的平等,人们通常会如何处理类型的证据？

我很高兴看到一个完整的证据,但请避免"明确地"发布它,以免破坏软件基础课程的练习.

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