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
Я нашел в сети различные решения для принципа сортировки. Вышеупомянутое адаптировано из того, что сделал Ковач, но в своем доказательстве он доказывает, что нет дубликатов, а есть повторения, как в упражнении SF.
Заметная разница в том, что я не могу доказать цель u <> x
здесь, потому что при формулировке проблемы в этой форме информации меньше.
Поскольку эта проблема является одновременно сложной и необязательной, и существуют существующие решения - и я уже работаю над ней в течение двух дней, может ли кто-нибудь описать мне высокоуровневый план того, что именно мне нужно, чтобы сделать это доказательство.
Я не ищу решения, но я надеюсь, что вариант с исключенной серединой окажется элегантным, потому что доказательство Coq без исключенного третьего — это просто беспорядок переписывания, и знание исходного кода программы далеко от понимания того, что это такое. делает. Большинство объяснений принципа просто описывают, что это такое, чего мне недостаточно, чтобы преодолеть пробел в интуиции.
Я никогда не видел классические законы в действии - не похоже, что знание того, что что-то разрешимо, принесло бы мне много пользы, и мне трудно понять, в чем их смысл. Это особенно актуально в этой ситуации, поэтому мне гораздо больше интересно посмотреть, какой окажется их цель.
Действительно, он не нужен, но определение гораздо проще при его использовании.
Я столкнулся с этим вопросом при поиске ответов при работе через SF (Software Foundations), но сумел доказать это сам. Я предоставлю набросок для SF-версии принципа сортировки с использованием exclude_middle. Утверждение, которое нужно доказать, состоит в том, что если все элементы в списке l1
находятся в l2
, а length l2
меньше, чем length l1
, то l1
содержит повторяющиеся элементы.
Доказательство, как предлагает SF, начинается индукцией по l1
. Я опущу простой пустой случай. В индуктивном случае уничтожить l2
. Случай, когда l2
пуст, прост; мы рассматриваем другой случай.
Теперь, из-за индукции по l1
и деструктурирования по l2
, ваше утверждение для доказательства касается списков с первым членом, назовем их x1::l1
и x2::l2
. Ваша гипотеза членства теперь выглядит так: все элементы в x1::l1
находятся в x2::l2
.
Но сначала давайте воспользуемся исключенным средним, чтобы указать, что либо x1
в l1
, либо x1
не в l1
. Если x1
в l1
, то мы можем тривиально доказать, что x1::l1
имеет повторы. Итак, продвигаясь вперед, мы можем предположить, что x1
не находится в l1
.
Достаточно сопоставить индуктивный случай, что существует l2'
той же длины, что и l2
, такой, что все элементы l1
находятся в l2'
.
Теперь рассмотрим гипотезу принадлежности для x1::l1
с переменной forall, введенной как x
:
По гипотезе мы знаем, что x1
в x2::l2
. Теперь рассмотрим l2'
, где l2'
— это x2::l2
с удаленным одним экземпляром x1
(используйте in_split
). Теперь, поскольку x1
не входит в l1
, мы можем заключить, что все члены l1
также находятся в l2'
, а не в удаленном элементе. Тогда это удовлетворяет гипотезе о принадлежности в индукции, и некоторые споры с длинами дают нам length l2 = length l2'
, так что гипотеза о длинах выполняется. Таким образом, мы заключаем, что l1
содержит повторы, а значит, и x1::l1
.
Редактировать: ранее я также проводил анализ случаев на предмет того, является ли x1
= x2
или x1
в l2
, и является ли x
= x2
или x
в l2
, и решал особые случаи более простым способом. Это не нужно, и общий случай их также охватывает.
Я не буду проверять, правильно ли ваше решение формально, а вместо этого поверю вам на слово. 5,5 месяцев назад, когда я задал этот вопрос, каким-то образом классическое доказательство полностью ошеломило меня, и я совершенно потерялся в том, что происходит. В конце концов, с большими усилиями и в течение определенного периода времени, я вычислил доказательство Агды и забыл неконструктивную версию, но все же хорошо иметь ее где-то.
Вам не нужен такой разбор случая. Вы знаете, что x1
находится в x2::l2
. Случаи x1 = x2
и x1
находится в l2
отдельно рассматривать не нужно. Вы можете использовать in_split
напрямую с x2::l2
.
IIRC вам не нужен EM. См. это решение в Агде для аналогичного состава с использованием
repeats
.