Как следует использовать исключенное третье в доказательстве принципа сортировки?

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 без исключенного третьего — это просто беспорядок переписывания, и знание исходного кода программы далеко от понимания того, что это такое. делает. Большинство объяснений принципа просто описывают, что это такое, чего мне недостаточно, чтобы преодолеть пробел в интуиции.

Я никогда не видел классические законы в действии - не похоже, что знание того, что что-то разрешимо, принесло бы мне много пользы, и мне трудно понять, в чем их смысл. Это особенно актуально в этой ситуации, поэтому мне гораздо больше интересно посмотреть, какой окажется их цель.

IIRC вам не нужен EM. См. это решение в Агде для аналогичного состава с использованием repeats.

gallais 15.05.2019 12:17

Действительно, он не нужен, но определение гораздо проще при его использовании.

eponier 15.05.2019 13:52
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
0
2
333
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Я столкнулся с этим вопросом при поиске ответов при работе через 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 месяцев назад, когда я задал этот вопрос, каким-то образом классическое доказательство полностью ошеломило меня, и я совершенно потерялся в том, что происходит. В конце концов, с большими усилиями и в течение определенного периода времени, я вычислил доказательство Агды и забыл неконструктивную версию, но все же хорошо иметь ее где-то.

Marko Grdinić 29.10.2019 15:30

Вам не нужен такой разбор случая. Вы знаете, что x1 находится в x2::l2. Случаи x1 = x2 и x1 находится в l2 отдельно рассматривать не нужно. Вы можете использовать in_split напрямую с x2::l2.

eponier 30.10.2019 12:11

Другие вопросы по теме