Lean 4 із підручником з математики - Частина 2 - Підмножини
Це переклад другої статті від Филип Уайшчак (Filip Łajszczak) - https://filip.lajszczak.dev/lean-4-with-a-math-textbook—part-2—subsets.html про формалізацію класичної теорії множин від Хелени Расьової у Lean4
Ми продовжуємо систематичне дослідження книги Гелени Расьової «Вступ до сучасної математики» за допомогою формалізації в Lean 4 Дивіться вступ. Визначивши в Частині 1, як працюють множини та належність через кодування предикатами, тепер переходимо до відношень підмножин.
Відношення підмножин: Формула (5)
Визначення Расьови:
Якщо кожен елемент множини $A$ є елементом множини $B$, тоді ми говоримо, що $𝐴$ є підмножиною $B$. Також кажуть, що множина $A$ міститься в множині $B$, або що $B$ містить $A$. Це записується як $A \subseteq B$ або $B \supset A$.
Потім вона ставить формальну умову:
За означенням, $A \subseteq B$ тоді й тільки тоді, коли для кожного $x$ виконується така умова: якщо $x \in A$, то $x \in B$.
У її символічному записі:
\[(A \subseteq B) \leftrightarrow (\textit{for every } x : x \in A \Rightarrow x \in B) \tag{5}\]Це безпосередньо перекладається як Lean:
def subset (A B : RasiowaSet α) : Prop := ∀ x, x ∈ A → x ∈ B
infixr:50 " ⊆ " => subset
infixr:50 " ⊇ " => fun A B => B ⊆ A -- позначення надмножини:
-- A ⊇ B означає B ⊆ A
Справжні (власні) підмножини: Расьова зазначає у примітці, що коли множини $A$ і $B$ не є тотожними, «кажуть, що $A$ є власною підмножиною $B$». Відношення власної підмножини означає, що $A$ міститься в $B$, але множини $A$ і $B$ не рівні - існує принаймні один елемент у $B$, якого немає в $A$.
-- Власна підмножина: A ⊂ B означає A ⊆ B та A ≠ B (примітка Расьової)
def proper_subset (A B : RasiowaSet α) : Prop := A ⊆ B ∧ A ≠ B
infixr:50 " ⊂ " => proper_subset
Повна відповідність: і Расьова, і Lean виражають підмножину через універсальну квантифікацію (∀ - «для всіх») над імплікацією (→ - «якщо… то»). Математичний зміст є тотожним.
Зв’язок у явному вигляді: хоча Lean автоматично розуміє, що наша інфіксна нотація 𝐴 ⊆ 𝐵 означає те саме, що й логічна формула ∀𝑥, 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵, з навчальною метою корисно сформулювати цю еквівалентність явно:
theorem subset_def (A B : RasiowaSet α) :
A ⊆ B ↔ ∀ x, x ∈ A → x ∈ B := by rfl
Ця теорема доводить еквівалентність за допомогою rfl (рефлексивності), оскільки обидві сторони є визначально рівними - інфіксна нотація ⊆ є лише синтаксичним цукром, що розгортається в логічну формулу. Це явне твердження допомагає з’єднати математичну нотацію з формальною логікою, показуючи, що означення з підручника Расьової та наше кодування в Lean виражають ідентичний математичний зміст.
Расьова наводить кілька конкретних прикладів:
Множина всіх цілих чисел міститься в множині всіх раціональних чисел, оскільки кожне ціле число є раціональним. Множина $A = \lbrace 1, 2 \rbrace$ міститься в множині $B = \lbrace 1, 2, 3 \rbrace $, оскільки $ 1 \in B $ і $2 \in B$. […] Множина всіх ірраціональних чисел міститься в множині всіх дійсних чисел, оскільки кожне ірраціональне число є дійсним.
Коли множини не є підмножинами: Формула (6)
Расіова також пояснює, коли множини не є підмножинами:
\[\sim(A \subseteq B) \Leftrightarrow (\textit{there is an } x \textit{ such that: } x \in A \textit{ and } \sim(x \in B)) \tag{6}\]Твердження про те, що $A$ не є підмножиною $B$, записується як $A \nsubseteq B$ або $B \nsupseteq A$. […] Із означення підмножини випливає, що $A \nsubseteq $B$ тоді й тільки тоді, коли не кожен елемент множини $A$ є елементом множини $B$, тобто в множині $A$ існує такий елемент, який не належить множині $B$. У символічній нотації:
Вона наводить такий приклад: «Множина всіх цілих чисел, кратних 3, не міститься в множині всіх цілих чисел, кратних 6, оскільки існує ціле число, кратне 3, але не кратне 6, наприклад число 9».
Тактики Lean Proof, які ми використовуватимемо:
Тактика constructor (див.) розділяє двосторонні твердження (якщо й тільки якщо, ↔) на дві окремі цілі: пряму імплікацію (→) та обернену (←).
Тактика intro (див.) працює із припущеннями: для універсальних кванторів (∀) вона вводить змінні, а для імплікацій (→) приймає гіпотезу.
Тактика rewrite (див.) замінює вирази, використовуючи рівність або еквівалентність. Синтаксис rewrite [theorem_name] at hypothesis застосовує переписування до конкретної гіпотези.
Тактика cases (див.) виконує розбір випадків для індуктивних типів, таких як диз’юнкції (∨), існування (∃) та кон’юнкції (∧).
Тактика have вводить проміжні результати. Синтаксис have name : type := proof створює нову гіпотезу, яку можна використовувати на наступних кроках.
Тактика exact (див.) надає довідковий терм, що точно збігається з поточною ціллю. Її застосовують тоді, коли ми маємо саме той доказ, який потрібен для завершення кроку.
Крапки (·) - це маркери Lean, які допомагають структурувати доведення, чітко розділяючи різні випадки чи підцілі.
Ключове слово theorem створює іменований доказ, який можна використовувати пізніше. На відміну від example (яке є анонімним), теореми стають частиною нашої математичної бібліотеки і можуть застосовуватися в інших доведеннях.
theorem not_subset_iff (A B : RasiowaSet α) :
¬(A ⊆ B) ↔ ∃ x, (x ∈ A ∧ x ∉ B) := by
constructor -- Розділити двонаправлений доказ
-- на прямий та зворотний напрямки
· -- Прямий напрямок: ¬(A ⊆ B) → ∃ x, (x ∈ A ∧ x ∉ B)
intro h -- Припустимо h : ¬(A ⊆ B)
rewrite [subset_def] at h -- Використайте нашу явну теорему для розкриття:
-- h : ¬(∀ x, x ∈ A → x ∈ B)
rewrite [not_forall] at h -- Застосуємо логічну еквівалентність:
-- h : ∃ x, ¬(x ∈ A → x ∈ B)
cases h with -- Витягуємо свідка з екзистенціала
| intro x hx => -- hx : ¬(x ∈ A → x ∈ B)
rewrite [not_imp] at hx -- Застосуємо ¬(P → Q) ↔ (P ∧ ¬Q):
-- hx : x ∈ A ∧ x ∉ B
exact ⟨x, hx⟩ -- Надає свідоцтво x із доказом hx
· -- Зворотній напрямок: ∃ x, (x ∈ A ∧ x ∉ B) → ¬(A ⊆ B)
intro h -- Припустимо h : ∃ x, (x ∈ A ∧ x ∉ B)
cases h with -- Витягуємо свідка з екзистенціала
| intro x hx => -- hx : x ∈ A ∧ x ∉ B
cases hx with -- Деструктуризовуємо кон'юнкцію
| intro hx_in_A hx_not_in_B => -- hx_in_A : x ∈ A,
-- hx_not_in_B : x ∉ B
intro h_subset -- Припустимо h_subset : A ⊆ B (для суперечності)
have hx_in_B : x ∈ B := h_subset x hx_in_A -- Застосуємо підмножину
-- щоб отримати x ∈ B
exact hx_not_in_B hx_in_B -- Суперечність: x ∉ B але x ∈ B
Цей доказ встановлює логічну еквівалентність, яку описує Расьова: $A$ не є підмножиною $B$ тоді й лише тоді, коли існує деякий елемент у $A$, який не належить $B$.
Пройдемо цей доказ крок за кроком звичайною математичною мовою, щоб показати відповідність між формальним і неформальним міркуванням:
Прямий напрямок: ми хочемо показати, що якщо $A$ не є підмножиною $B$, тоді існує деякий елемент у $A$, який не належить $B$.
Припустимо, що $A$ не є підмножиною $B$. За означенням це означає, що неправда, ніби кожен елемент $A$ належить $B$. У класичній логіці «не кожен» еквівалентно «існує такий, що … не», отже, повинен існувати деякий елемент $x$, для якого $x \in A$, але $x \in B$. Це саме те, що ми хотіли довести.
Зворотній напрямок: ми хочемо показати, що якщо існує деякий елемент у $A$, який не належить $B$, тоді $A$ не є підмножиною $B$.
Припустимо, що існує конкретний елемент $x$ такий, що $x \in A$ і $x \notin B$. Тепер, для доведення від супротивного, вважатимемо, що $A \subseteq B$. Тоді за означенням підмножини кожен елемент $A$ повинен належати $B$. Зокрема, оскільки $x \in A$, мусить виконуватися й $x \in B$. Але ми вже знаємо, що $x \notin B$ - суперечність! Отже, наше припущення було хибним, і маємо $A \nsubseteq B$.
Рівність множин: Формула (7)
Расіова визначає, коли два множини рівні:
\[(A = B) \Leftrightarrow (\textit{for every } x : x \in A \Leftrightarrow x \in B) \tag{7}\]Множини $A$ та $B$ є ідентичними тоді і тільки тоді, коли вони мають однакові елементи. Це записується так:
У Lean це теорема про екстенсивність множин:
theorem set_extensionality (A B : RasiowaSet α) :
A = B ↔ ∀ x, (x ∈ A ↔ x ∈ B) := by
constructor -- Розділити двонаправлений доказ на прямий та зворотний
· -- Прямий напрямок: якщо A = B, тоді однакова належність
intro h x -- Припустимо h : A = B, нехай x буде довільним
rw [h] -- Перепишемо мету, використовуючи A = B:
-- x ∈ A ↔ x ∈ B стає x ∈ B ↔ x ∈ B
-- що тривіально істинно згідно з рефлексивністю
· -- Зворотній напрямок: якщо однакова належність, тоді A = B
intro h -- Припустимо h : ∀ x, (x ∈ A ↔ x ∈ B)
funext x -- Екстенсивність функції:
-- щоб довести, що A = B (функції рівні),
-- покажемо A x = B x для усіх x
exact propext (h x) -- Пропозиційна екстенсіональність:
-- оскільки h x доводить
-- x ∈ A ↔ x ∈ B,
-- твердження A x та B x рівні
Ця теорема встановлює те, про що говорить Расьова: дві множини є рівними тоді й лише тоді, коли вони мають ті самі елементи - базовий принцип екстенсіональності множин.
Маючи формалізованими відношення підмножин і рівність множин, ми готові досліджувати глибші математичні властивості, що випливають із цих означень. Наступний крок у Расьової - показати основні властивості, яким має задовольняти кожна математична структура, побудована на підмножинах, - такі властивості, як рефлексивність, транзитивність і антисиметричність, що розкривають внутрішню логічну архітектуру теорії множин.