时间戳

首页 > 解决方案 > 在鸽巢原理的证明中应该如何使用排中？

coq - 在鸽巢原理的证明中应该如何使用排中？

问题描述

Lemma remove {A} (x : A) xs (p : In x xs) :
  exists xs', (forall x', x' <> x -> In x' xs -> In x' xs') /\ (length xs = S (length xs')).
Proof.
induction xs.
- inversion p.
- destruct p.
  + subst x0.
    exists xs.
    split.
    * intros x' neq pin.
      destruct pin.
      -- contradict neq. symmetry. assumption.
      -- assumption.
    * reflexivity.
  + destruct (IHxs H) as [xs' pxs']. clear IHxs.
    destruct pxs' as [p1 plen]. rename x0 into x'.
    exists (x' :: xs').
    split.
    * intros x'' neq pin. 
      destruct pin.
      -- subst x'. left. reflexivity.
      -- right. apply p1. assumption. assumption.
    * simpl.
      rewrite -> plen.
      reflexivity. 
Qed.

Theorem pigeonhole_principle: forall (X:Type) (l1  l2:list X),
  excluded_middle ->
  AllIn l1 l2 ->
  length l2 < length l1 ->
  repeats l1.
Proof.
induction l1; simpl; intros l2 ex_mid Hin Hlen.
- inversion Hlen.
- apply repeats_rest.
  destruct (remove x l2) as [l2' Hl2].
  + apply Hin. left. reflexivity.
  + destruct Hl2 as [Hmap Hlen'].
    rewrite Hlen' in Hlen.
    clear Hlen'.
    apply (IHl1 l2').
    1 : { assumption. }
    2 : { revert Hlen. unfold lt. intros. omega. }
    clear Hlen IHl1.
    revert Hin.
    unfold AllIn.
    intros.
    apply Hmap.
    2 : { apply Hin. right. assumption. }

1 subgoal
X : Type
x : X
l1, l2 : list X
ex_mid : excluded_middle
l2' : list X
Hmap : forall x' : X, x' <> x -> In x' l2 -> In x' l2'
Hin : forall u : X, In u (x :: l1) -> In u l2
u : X
H : In u l1
______________________________________(1/1)
u <> x

我在网上找到了各种关于鸽笼原理的解决方案。以上内容改编自Kovacs的内容，但在他的证明中，他证明了没有重复项，而不是 SF 练习中的重复项。

显着的区别是我无法在u <> x这里证明目标，因为当以这种形式陈述问题时，信息较少。

由于这个问题既困难又可选，并且存在现有的解决方案 - 我已经研究了两天，有人可以向我描述一个我需要做这个证明的高级计划吗？

我不是在寻找解决方案，但我希望具有排除中间的那个结果是优雅的，因为没有排除中间的 Coq 证明只是重写的混乱，并且知道程序的源代码远非了解它的作用。大多数对原理的解释只是描述了它是什么，这不足以让我弥合直觉鸿沟。

我从来没有见过经典的法则在起作用——知道某事是可判定的似乎不会让我受益匪浅，而且我发现很难看出它们的意义是什么。在这种情况下尤其如此，所以我更有兴趣看看他们的目的是什么。

标签： coq

解决方案

我在通过 SF（软件基础）工作时寻找答案时遇到了这个问题，但我自己设法证明了这一点。我将使用excluded_middle 为SF 版本的鸽笼原理提供一个草图。要证明的语句是，如果列表中的所有元素l1都在l2并且length l2小于length l1，则l1包含重复的元素。

SF 建议的证明始于对 的归纳l1。我将省略简单的空案例。在归纳的情况下， destruct l2。为空的情况l2很简单；我们考虑另一种情况。

现在，由于 on 的归纳l1和解构l2，您要证明的陈述是关于具有第一个成员的列表，我们称它们为x1::l1and x2::l2。您的成员资格假设现在看起来像： 中的所有元素x1::l1都在x2::l2.

但首先，让我们使用排中来表示x1inl1或x1not in l1。如果x1在l1，那么我们可以简单地证明x1::l1有重复。所以向前看，我们可以假设它x1不在l1.

它足以匹配存在一个l2'长度相同的归纳情况，使得 的l2所有元素l1都在 中l2'。

现在考虑关于 的隶属度假设x1::l1，其中引入的 forall 变量为x：

通过假设，我们知道x1在x2::l2. 现在考虑l2', wherel2'是一个已移除x2::l2实例(use )。现在因为not in ，我们可以得出结论 的所有成员也在 in而不是被移除的元素。那么这就满足了归纳中的隶属度假设，一些与长度的争论给了我们，从而满足了长度假设。因此，我们得出结论包含重复，因此也包含。x1in_splitx1l1l1l2'length l2 = length l2'l1x1::l1

编辑：之前我也对是否x1=x2或x1inl2以及是否x=x2或xin进行了案例分析l2，并以更直接的方式解决了特殊情况。它不是必需的，一般情况下也包括它们。

推荐阅读