Це переклад третьої статті від Филип Уайшчак (Filip Łajszczak) - https://filip.lajszczak.dev/lean-4-with-a-math-textbook—part-3—properties-of-subsets.html про формалізацію класичної теорії множин від Хелени Расьової у Lean4

Ми завершуємо нашу формалізацію базового розділу Гелени Расьової про множини (вступ), доводячи основні властивості, що випливають із наших означень. Спираючись на кодування множин і відношення належності (Частина 1) та на відношення підмножини (Частина 2,), тепер ми переходимо до Пропозиції 1.1 Расьової.

Расьова визначає властивості, що випливають з визначення підмножини:

З визначення підмножини випливає, що

1.1. Для будь-яких множин $A$, $B$, $C$:

\[\varnothing \subseteq A \tag{8}\] \[A \subseteq A \tag{9}\] \[\textit{if } A \subseteq B \textit{ and } B \subseteq C, \textit{ then } A \subseteq C \tag{10}\] \[\textit{if } A \subseteq B \textit{ and } B \subseteq A, \textit{ then } A = B \tag{11}\] \[\textit{if } A \ne B, \textit{ then } A \nsubseteq B \textit{ or } B \nsubseteq A \tag{12}\]

Давайте доведемо кожну з цих властивостей у Lean:

Властивість (8): Порожня множина є підмножиною будь-якої множини

Расьова пояснює: «Формула (8) стверджує, що порожня множина міститься в кожній множині. Оскільки порожня множина не має жодних елементів, умова, що кожен елемент множини ∅ є елементом множини 𝐴, виконується».

theorem empty_subset (A : RasiowaSet α) : ∅ ⊆ A := by
  intro x h  -- Припустимо, що x довільне, а h : x ∈ ∅
             -- Мета стає: x ∈ A
  exact False.elim h  -- Оскільки x ∈ ∅ означає False,
                      -- використовуючи принцип вибуху
                      -- (із False, може випливати будь-що)

Покрокове пояснення доведення:

Що ми доводимо: твердження $\varnothing \subseteq A$ означає «порожня множина є підмножиною довільної множини $A$». За нашим означенням підмножини це розгортається в $\forall x,\; x \in \varnothing → x \in A$ (для всіх $x$: якщо $x$ належить порожній множині, то $x$ належить $A$).

Ключове слово by: воно переводить у тактичний режим, у якому доказ будується покроково за допомогою тактик, замість того, щоб одразу надати повний терм доказу.

Тактика intro x h: оскільки наша ціль — це твердження $\forall x,\; x ∈ ∅ \to x ∈ A$, нам потрібно довести універсальне висловлювання з імплікацією. Тактика intro працює з обома частинами:

  • intro x означає: «візьмемо довільний елемент $x$» (це відповідає частині $\forall x$),
  • intro h означає: «припустимо гіпотезу $h : x \in \varnothing$» (це відповідає частині імплікації →).

Після застосування intro x h наші припущення виглядають так:

  • $x : a$ — де $x$ є довільним елементом деякого типу $α$,
  • $h : x \in \varnothing$ — ми припускаємо, що $x$ належить порожній множині.

Наша ціль тепер: довести, що $x ∈ A$ (що $x$ належить множині $A$).

Суперечність: але припущення $h : x ∈ ∅$ насправді означає $h : \text{False}$ (адже належність до порожньої множини завжди хибна). Отже, ми маємо доказ хибності!

Тактика exact False.elim h: із доказу $\text{False}$ можна довести будь-що. False.elim реалізує принцип вибуху (ex falso quodlibet) — якщо виникла суперечність, то будь-яке твердження стає довідним. Оскільки $h : \text{False}$, ми можемо застосувати False.elim h, щоб довести нашу ціль $x ∈ A$.

Властивість (9): Кожна множина є підмножиною самої себе (рефлексивність)

Расьова пояснює: «Формула (9) стверджує, що кожна множина є підмножиною самої себе. Справді, кожен елемент множини 𝐴 є елементом 𝐴».

theorem subset_refl (A : RasiowaSet α) : A ⊆ A := by
  intro x h  -- Припустимо, що x довільне, а h : x ∈ A
             -- Мета стає: x ∈ A
  exact h    -- У нас вже є саме те, що нам потрібно довести

Цей випадок виглядає значно простішим: ми припускаємо $x \in A$ і маємо довести $x \in A$ — усе потрібне вже в нас є!

Властивість (10): Транзитивність відношення підмножини

Расьова пояснює: «Формула (10) є законом транзитивності для відношення включення. Щоб довести це, припустимо, що $A ⊆ B$ і $B ⊆ C$. Тоді кожен елемент множини $A$ є елементом множини $B$, а кожен елемент множини $B$ є елементом множини $C$. Звідси випливає, що кожен елемент множини $A$ є елементом множини $C$, а отже $A ⊆ C$».

theorem subset_trans (A B C : RasiowaSet α) :
  A ⊆ B → B ⊆ C → A ⊆ C := by
  intro h₁ h₂  -- Припустимо h₁ : A ⊆ B та h₂ : B ⊆ C
               -- Мета стає: A ⊆ C (i.e., ∀ x, x ∈ A → x ∈ C)
  intro x h    -- Нехай x довільне, припустимо, що h : x ∈ A
               -- Мета стає: x ∈ C
  have h_B : x ∈ B := h₁ x h  -- Застосуємо h₁ щоб отримати x ∈ B із x ∈ A
  exact h₂ x h_B              -- Застосуємо h₂ щоб отримати x ∈ C із x ∈ B

Ми вибудовуємо імплікації крок за кроком: спочатку отримуємо h_B : x ∈ B з h : x ∈ A, використовуючи h₁, а потім застосовуємо h_B разом із h₂, щоб отримати x ∈ C.

Властивість (11): Антисиметричність — взаємне включення підмножин означає рівність

Расіова пояснює: «Щоб довести (11), припустімо, що $A \subseteq B$ і $B \subseteq A$. Отже, кожен елемент множини $A$ є елементом множини $B$, і кожен елемент множини $B$ є елементом множини $A$. Таким чином, множини $A$ і $B$ мають однакові елементи, тобто вони тотожні».

Вона також зазначає: «Формула (11) часто використовується при доведенні тотожності множин».

theorem subset_antisymm (A B : RasiowaSet α) :
  A ⊆ B → B ⊆ A → A = B := by
  intro h₁ h₂  -- Припустимо h₁ : A ⊆ B та h₂ : B ⊆ A
               -- Мета стає: A = B
  -- Використоємо екстенсіональність множини:
  -- Дві множини рівні, якщоі тільки якщо вони мають однакову нажежність
  rw [set_extensionality]  -- Мета стає: ∀ x, (x ∈ A ↔ x ∈ B)
  intro x      -- Нехай x довільне
               -- Мета стає: x ∈ A ↔ x ∈ B
  constructor  -- Розділити двонаправлений доказ на прямий та зворотний напрямки
  · -- Прямий напрямок: x ∈ A → x ∈ B
    exact h₁ x -- Застосувати відношення підмножини h₁
  · -- Зворотній напрямок: x ∈ B → x ∈ A
    exact h₂ x -- Застосувати відношення підмножини h₂

Властивість (12): Контрапозиція антисиметричності

Рашіова пояснює: «Формула (12) випливає з формули (11). Якби виконувалося $A \subseteq B$ і $B \subseteq A$, то за (11) множини $A$ і $B$ були б однаковими, що суперечить припущенню $A \neq B$».

Нові тактики: ми вводимо by_cases для класичного розгляду випадків — вона розділяє доведення залежно від того, істинне чи хибне твердження. Ми також використовуємо тактики left та right: коли ціллю є диз’юнкція $(P ∨ Q)$, застосовуємо left, щоб довести $P$, або right, щоб довести $Q$.

theorem inequality_disjunction (A B : RasiowaSet α) : 
  A ≠ B → ¬(A ⊆ B) ∨ ¬(B ⊆ A) := by
  intro h   -- Припустимо h : A ≠ B
            -- Мета стає: ¬(A ⊆ B) ∨ ¬(B ⊆ A)
  -- Використовуємо класичні міркування: або A ⊆ B, або A ⊄ B
  by_cases h₁ : A ⊆ B  -- Розділимо на випадки залежно від того, чи A ⊆ B
  · -- Випадок: A ⊆ B
    right  -- Оберемо праву частину диз'юнкції: ¬(B ⊆ A)
    intro h₂  -- Припустимо h₂ : B ⊆ A (для протиріччя)
              -- Мета стає: False
    -- За антисиметрією: A = B
    have h_eq : A = B := subset_antisymm A B h₁ h₂
    -- Суперечність із h : A ≠ B
    exact h h_eq  -- Apply h : A ≠ B to h_eq : A = B to get False
  · -- Випадок: A ⊄ B (¬(A ⊆ B))
    left   -- Оберемо ліву частину диз'юнкції: ¬(A ⊆ B)
    exact h₁  -- У нас вже є докази із розгляду випадка

Розглянемо доказ того, що ${1,2} \subseteq {1,2,3}$:

Спершу задамо наші множини:

def setA : RasiowaSet Nat := fun x => x = 1 ∨ x = 2
def setB : RasiowaSet Nat := fun x => x = 1 ∨ x = 2 ∨ x = 3

Тоді ми можемо довести співвідношення підмножин:

example : setA ⊆ setB := by
  intro x h        -- Припустимо, що x довільне, а h : x ∈ setA
                   -- h : x = 1 ∨ x = 2 (за визначенням setA)
                   -- Мета: x ∈ setB (i.e., x = 1 ∨ x = 2 ∨ x = 3)
  cases h with     -- Аналіз випадків x = 1 ∨ x = 2
  | inl h1 =>      -- Випадок: h1 : x = 1
    left; exact h1 -- Виберіть лівий диз'юнкт 1 ∨ 2 ∨ 3, 
                   -- надаємо доказ h1
  | inr h2 =>      -- Випадок: h2 : x = 2  
    right; left; exact h2 -- Виберіть середній диз'юнкт 1 ∨ 2 ∨ 3, 
                          -- надаємо доказ h2

Схема тут така: ми розкладаємо диз’юнкцію (∨, твердження «або») в нашому припущенні, а потім відновлюємо відповідну диз’юнкцію в нашій цілі.

Ми також можемо перевірити конкретні приклади належності:

example : 1 ∈ setA := by left; rfl   -- 1 ∈ {1, 2} тому що 1 = 1
example : 2 ∈ setA := by right; rfl  -- 2 ∈ {1, 2} тому що 2 = 2
example : 1 ∈ setB := by left; rfl   -- 1 ∈ {1, 2, 3} тому що 1 = 1
example : 2 ∈ setB := by right; left; rfl  -- 2 ∈ {1, 2, 3} 
                                           -- тому що 2 = 2

Приємна формалізація

Робота з визначеннями Расьової в Lean показує, як формальна математика може стати містком між інтуїтивними математичними міркуваннями та точною обчислювальною перевіркою. Тактичні докази, які ми побудували, віддзеркалюють логічні кроки, описані Расьовою у підручнику, але з кожним висновком, зробленим явно та таким, що підлягає перевірці.

Процес перекладу математичного тексту у тактики Lean виявився дуже пізнавальним. Коли Расьова пише: «з визначення підмножини випливає, що…», ми бачимо, як це розгортається у вигляді конкретних правил переписування та логічних перетворень у наших доказах. Її неформальні міркування про свідків та протиріччя перетворюються на структурований розбір випадків та явну побудову доказів.

Відкриваючи зв’язок

Те, що постає з цієї формалізації, виглядає не як переклад між різними математичними системами, а радше як усвідомлення того, що класична теорія множин і типо-теоретичні засади можуть описувати одну й ту ж математичну реальність крізь різні призми. Інсайт Расьової, що множини можна розглядати як властивості — чітко сформульований, коли вона пише «𝐴(𝑥)» у значенні «𝑥 має властивість 𝐴», — саме це Lean кодує як α → Prop.

Логічна структура залишається ідентичною: відношення підмножин — це універсальні імплікації, докази для порожньої множини ґрунтуються на беззмістовній(прим. перекл. vacuous) істинності, а рівність множин випливає з аксіоми розширеності. Формалізація не змінює математику; вона радше робить видимою логічну архітектуру, яка була присутня у ретельному викладі Расьової.

Цей досвід перегукується з тим, що описував Террі Тао у своїй розмові з Лексом Фрідманом — формальна верифікація в Lean 4 робить математичні міркування водночас більш доступними та більш строгими. Пропрацьовуючи базові концепти Расьової у Lean, ми бачимо, як класичний математичний виклад і сучасні помічники для доведень служать одній і тій самій меті: робити математичну істину водночас відкриваною й перевірюваною. Це також веде до формальної верифікації алгоритмів і комп’ютерних програм — теми, яку я теж сподіваюся дослідити в майбутньому.

Подальші кроки

Ця серія дописів — найдовший матеріал у блозі на цей момент, і вона охоплює лише чотири сторінки книги Расьової. Почалося все з однієї статті, але масштаби швидко виросли. Наступний розділ підручника присвячений поняттю об’єднання множин, і, з Божою поміччю, я сподіваюся висвітлити його в наступному дописі.

Якщо якийсь справжній математик дочитав до цього місця — дайте знати, чи я десь помилився, або якщо у вас є коментарі чи поради. Також буду радий почути від тих, хто вчить Lean, чи є для них корисним такий глибокий розбір.