Как доказать существование обратных функций в Isabelle / HOL?

Я согласен с проницательными замечаниями Доминика Унру. Однако я хотел бы упомянуть, что теорема, которая отражает идею, лежащую в основе теоремы, которую вы пытаетесь доказать, уже существует в исходном коде основной библиотеки Isabelle / HOL. Фактически, он существует как минимум в двух разных форматах: позвольте мне назвать их традиционным форматом Isabelle / HOL и каноническим форматом FuncSet. Относительно первого см. Теорему bij_betw_iff_bijections:

"bij_betw f A B ⟷ (∃g. (∀x ∈ A. f x ∈ B ∧ g(f x) = x) ∧ (∀y ∈ B. g y ∈ A ∧ f(g y) = y))"

С FuncSet дело обстоит немного сложнее. Похоже, что не существует ни одной теоремы, отражающей эту идею. Однако вместе теоремы bij_betwI, bij_betw_imp_funcset и inv_into_funcset почти эквивалентны теореме, которую вы пытаетесь сформулировать. Позвольте мне представить набросок того, как можно выразить эту теорему способом, который можно было бы считать вполне каноническим в FuncSet смысле (попробуйте доказать это сами):

lemma bij_betw_iff:
  shows "bij_betw f A B ⟷
    (
      ∃g.
        (∀x. x∈A ⟶ g (f x) = x) ∧
        (∀y. y∈B ⟶ f (g y) = y) ∧
        f ∈ A → B ∧
        g ∈ B → A
    )"
sorry

Я также хотел бы повторить совет Доминика Унру и сделать несколько дополнительных замечаний:

Моя рекомендация: сначала попробуйте доказательство с помощью bij вместо bij_betw.

Действительно, это очень хорошая идея. В общем, пытаясь ограничить проблему явно определенными наборами A и B, вместо того, чтобы работать напрямую с типами, вы затронули тему, которая в логике известна как релятивизация. Для мягкого введения непрофессионала см, например, https://leanprover.github.io/logic_and_proof/first_order_logic.html [1], более подробное введение в контексте теории множеств см. в [2, глава 12]. Как вы, наверное, уже заметили, релятивизировать теоремы в Isabelle / HOL не так просто, и это требует дополнительных усилий по доказательству. Однако существует расширение Isabelle / HOL, которое позволяет автоматизировать процесс релятивизации теорем. Для получения дополнительной информации об этом расширении см. Статью Ондржея Кунчара и Андрея Попеску От типов к множествам по определению локального типа в логике высокого порядка [3]. Также существует крупномасштабный пример применения фреймворка [4]. Независимо от этого, я работаю над тем, чтобы сделать это расширение более удобным для пользователя и очень медленно приближаюсь к завершающим этапам в своих усилиях: см. https://gitlab.com/user9716869/tts_extension. Таким образом, в принципе, если вы знаете, как использовать типы-множества и принимаете его аксиомы, то достаточно доказать теорему с помощью bij, например,

"bij f ⟷ (∃g. (∀x. g (f x) = x) ∧ (∀y. f (g y) = y))",

Затем теоремы, подобные bij_betw_iff_bijections и bij_betw_iff, могут быть синтезированы автоматически бесплатно одним нажатием кнопки (почти ...).

Наконец, для полноты, позвольте мне предложить свой собственный совет относительно ваших вопросов (хотя, как я уже упоминал, я согласен со всем, что сказал Доминик Унру)

как расширить соответствующие определения, а затем упростить их с помощью функциональных приложений. Я следил за некоторыми примерами / учебными пособиями Isabelle (2021) как о применении simp-стиля, так и о доказательстве Isar в структурированном стиле, но не мог свободно использовать доказательство Isar. Как только я запустил команду доказательства, я не знаю, как упростить или продвинуться дальше.

Я считаю, что лучший способ узнать то, что вы пытаетесь изучить, - это выполнять упражнения из книги Конкретная семантика Тобиаса Нипкова и Гервина Кляйна [5]. Кроме того, я бы также просмотрел Помощник по проверке логики высшего порядка Тобиаса Нипкоу и др. [6] (он немного устарел, но я нашел его полезным специально для изучения сценариев в стиле apply / прямое применение правил). Между прочим, я в основном самоучился Изабель из этих книг без какого-либо предшествующего опыта в формальных методах.

Исар использует новый способ предполагает ... показывает ... для формулировки теоремы. Есть ли аналогичная поддержка для доказательства iff (⟷), как в примере выше? Без него нет доступа к assms и т. Д., И нужно ли во время доказательства предполагать все, кроме заключения.

Я сделаю совет Доминика Унру более ясным: используйте для этого rule iffI или intro iffI.

Изменить. Когда вы используете rule iffI (или аналогичный) для запуска структурированного доказательства Isar, вам необходимо явно указать свои предположения для каждой подцели (используя парадигму assume ... show ...). Однако есть инструмент, который может автоматически сгенерировать такой шаблонный код Isar. Он называется Sketch-and-Explore, и вы можете найти его в каталоге HOL/ex основной библиотеки Isabelle / HOL. В этом случае все, что вам нужно сделать, это ввести sketch(rule iffI), и парадигма _23 _ / _ 24_ будет сгенерирована автоматически для каждой подцели.

Ссылки

1. Авигад Дж., Льюис Р. Я. и ван Дорн Ф. Логика и доказательство.
2. Jech T. Теория множеств. 3-е изд. Гейдельберг: Спрингер; 2006. (Чистая и прикладная математика, серия монографий и учебников).
3. Кунчар О., Попеску А. От типов к множествам с помощью определения локального типа в логике высокого порядка. Журнал автоматизированных рассуждений. 2019; 62 (2): 237–60.
4. Иммлер Ф., Жан Б. Гладкие многообразия и типы множеств для линейной алгебры в Изабель / HOL. В: 8-я Международная конференция ACM SIGPLAN по сертифицированным программам и доказательствам. Нью-Йорк: ACM; 2019. стр. 65–77. (CPP 2019).
5. Нипков Т., Кляйн Г. Конкретная семантика с Изабель / HOL. Гейдельберг: Springer-Verlag; 2017 г. (http://concrete-semantics.org/)
6. Нипкоу Т., Полсон Л.К., Венцель М. Помощник по доказательству логики высокого порядка. Гейдельберг: Springer-Verlag; 2017 г.

lemma bij_iff_ex_identity : "bij_betw f A B ⟷ (∃ g. g∘f = restrict id B ∧ f∘g = restrict id A)"

Я думаю, что это не совсем то, что вам нужно, и я сомневаюсь, что это правда. g∘f = restrict id B не означает, что g∘f и id равны на B. Это означает, что итоговая функция g∘f (а в HOL есть только итоговые функции) равна итоговой функции restrict id B. Последний возвращает id x на x∈B и undefined в противном случае. Таким образом, чтобы сделать это равенство истинным, g необходимо вывести undefined всякий раз, когда вход f не находится в B. Но откуда g это знать!

Если вы хотите использовать restrict, вы можете написать restrict (g∘f) B = restrict id B. Но лично я бы предпочел более простой (∀x∈B. (g∘f) x = x).

Итак, исправленная теорема будет такой:

lemma bij_iff_ex_identity : "bij_betw f A B ⟷ (∃ g. (∀x∈A. (g∘f) x = x) ∧ (∀y∈B. (f∘g) y = y))"

(Что, кстати, все еще неверно, как сообщает мне quickcheck в Isabelle / jEdit, см. Окно вывода. Если A имеет один элемент, а B пусто, f не может быть взаимно однозначным. Таким образом, теорема, которую вы пытаетесь использовать, на самом деле математически не правда. Я не буду пытаться это исправить, а просто отвечу на оставшиеся строки.

unfolding bij_betw_def inj_on_def restrict_def iffI

iffI здесь не действует. При развертывании можно применять только теоремы вида A = B (правила безусловной перезаписи). iffI не такой формы. (Используйте thm iffI, чтобы увидеть.)

proof

Лично я не использую голую форму proof, но всегда proof - или proof (some method). Потому что proof просто применяет какой-то метод по умолчанию (в данном случае эквивалент (rule iffI), поэтому я думаю, что лучше сделать его явным. proof - просто запускает доказательство без применения дополнительного метода.

let ?g = "restrict (λ y. (if f x = y then x else undefined)) B"

У вас есть несвязанная переменная x. (Обратите внимание на цвет фона в среде IDE.) Скорее всего, это не то, что вам нужно. Формально это разрешено, но x будет рассматриваться как некоторая произвольная константа.

В общем, я не думаю, что есть какой-либо способ определить g простым способом (то есть только с помощью квантификаторов и приложений-функций и if-then-else). Я думаю, что единственный способ определить инверсию (даже если вы знаете, что она существует) - это использовать оператор THE, потому что вам нужно сказать что-то вроде g y - это x такой, что f x = y. (А потом в доказательстве вы столкнетесь с обязательством доказательства того, что он действительно существует и уникален.) См. Определение inv_into в Hilbert_Choice.thy (за исключением того, что здесь используется SOME, а не THE). Может быть, для начала попробуйте провести доказательство, просто используя существующую константу inv_into.

assume "(∀x∈A. ∀y∈A. f x = f y ⟶ x = y)"

Все assume команды должны иметь предположения, точно такие же, как в цели доказательства. Вы можете проверить, правильно ли вы написали, просто временно написав команду show A for A (это недоказуемая цель, которая, однако, завершит доказательство, поэтому она обманом заставляет Изабель проверить, будет ли это). Если эта команда не выдает ошибки, вы правильно поняли assumes. В ваших случаях вы этого не сделали, это должно быть (∀x∈A. ∀y∈A. f x = f y ⟶ x = y) ∧ f ' A = B. ('здесь является обратным апострофом. Разметка не позволяет мне его писать.)

Моя рекомендация: сначала попробуйте испытать доказательство с bij вместо bij_betw. (Одно направление находится в BNF_Fixpoint_Base.o_bij, если вы хотите обмануть.) Когда закончите, вы можете попытаться обобщить.