问题描述
在Software Foundations中一个被要求证明 pigeonhole原理的人，可以使用排除中间的，但是有人提到这并非严格必要。我一直试图在没有EM的情况下证明它，但是我的大脑似乎是经典的连线。
In Software Foundations IndProp.v one is asked to prove the pigeonhole principle, and one may use excluded middle, but it is mentioned that it is not strictly necessary. I've been trying to prove it without EM, but my brain seems to be wired classically.
问：没有定理的情况下，如何证明定理 >使用排除的中间？在没有可判定的相等性的情况下（人们不容易通过案例推理）的类型，人们通常应该如何使用证明？
Q: How would one prove the theorem without using excluded middle? How should one generally approach proofs for types without decidable equality, where one can't easily reason by cases?
我很乐意提供完整的证明，但请避免将其公开发布，以免破坏软件中的练习基础课程。
I'd be very happy for a complete proof to look at, but please avoid posting it "in the clear", so as to not spoil the exercise in the Software Foundations course.
定义使用两个归纳谓词， In 和重复。
The definition uses two inductive predicates, 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'。现在 l1’是 a :: l2’的子集。我的EM训练直觉是以下条件之一：
I'll describe the thought process that led me to a solution, in case it helps. We may apply induction and it is straightforward to reduce to the case l1 = a::l1', l2 = a::l2'. Now l1' is a subset of a::l2'. My EM-trained intuition is that one of the following holds:
- a 是在 l1'中。
- a 不在 l1'。
- a is in l1'.
- a is not in l1'.
在后一种情况下， l1'的每个元素在 a :: l2'中，但与 a 不同，因此必须在 l2'。因此， l1'是 l2'的子集，我们可以应用归纳假设。
In the latter case, each element of l1' is in a::l2' but differs from a, and therefore must be in l2'. Thus l1' is a subset of l2', and we can apply the inductive hypothesis.
不幸的是，如果 In 不可确定，则上述内容不能直接形式化。特别是如果无法确定给定类型的相等性，则很难证明元素不相等，因此很难证明否定性陈述，例如〜（在l1’中）。但是，我们希望使用该否定语句来证明是肯定的，即
Unfortunately if In is not decidable, the above can't be directly formalized. In particular if equality is not decidable for the given type, it's difficult to prove elements are unequal, and therefore difficult to prove a negative statement like ~(In a l1'). However, we wanted to use that negative statement to prove a positive one, namely
forall x, In x l1' -> In x l2'
类推，假设我们想证明
P \/ Q Q -> R ------ P \/ R
上面的直观论证就像从 P \ /〜P 开始，然后使用〜P-> Q-> R 在第二种情况下。我们可以使用直接证明来避免EM。
The above intuitive argument is like starting from P \/ ~P, and using ~P -> Q -> R in the second case. We can use a direct proof to avoid EM.
对列表中的 l1'进行量化会使情况变得更加复杂，但仍然可以使用以下引理构造一个直接证明，可以通过归纳证明。
Quantifying over the list l1' makes this a bit more complicated, but still we can construct a direct proof using the following lemma, which can be proven by induction.
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).
最后请注意，直观的信鸽原理也可以是形式化为以下方式，当类型具有不确定的相等性时无法证明（请注意，结论中包含否定语句）：
Finally note that the intuitive pigeonhole principle could also be formalized as the following way, which cannot be proven when the type has undecidable equality (note that it has a negative statement in the conclusion):
Definition pigeon2 {X} : Prop := forall (l1 l2 : list X),
length l2 < length l1 ->
(exists x, In x l1 /\ ~(In x l2)) \/ repeats l1.
这篇关于没有可判定的相等性或排除中间的鸽子洞证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！