6. 이산 수학

이산 수학은 유한 집합, 유한한 대상과 구조를 연구하는 분야입니다. 유한 집합의 원소 개수를 셀 수 있고, 그 원소들에 대한 유한 합이나 유한 곱을 계산할 수 있으며, 최댓값과 최솟값을 구하는 등의 일도 할 수 있습니다. 또한 특정 생성 함수를 유한 번 적용하여 생성되는 대상을 연구할 수 있고, 구조적 재귀로 함수를 정의할 수 있으며, 구조적 귀납법으로 정리를 증명할 수도 있습니다. 이 장에서는 이러한 작업을 뒷받침하는 Mathlib의 여러 부분을 설명합니다.

6.1. Finset과 Fintype

Mathlib에서 유한 집합과 유한 타입을 다루는 일은 혼란스러울 수 있습니다. 라이브러리가 이를 다루는 방법을 여러 가지 제공하기 때문입니다. 이 절에서는 그중 가장 흔히 쓰이는 방법들을 살펴보겠습니다.

우리는 이미 제 5.2 절과 제 5.3 절에서 Finset 타입을 접한 적이 있습니다. 이름에서 알 수 있듯이, Finset α 타입의 원소는 α 타입의 원소들로 이루어진 유한 집합입니다. 이를 “finset”이라고 부르겠습니다. Finset 데이터 타입은 계산적 해석을 갖도록 설계되었으며, Finset α에 대한 많은 기본 연산은 α가 결정 가능한 동등성을 갖는다고 가정합니다. 이 가정은 a : α가 finset s의 원소인지 판정하는 알고리즘이 존재함을 보장합니다.

section
variable {α : Type*} [DecidableEq α] (a : α) (s t : Finset α)

#check a ∈ s
#check s ∩ t

end

[DecidableEq α] 선언을 제거하면, Lean은 교집합을 계산할 수 없으므로 #check s ∩ t 줄에서 오류를 냅니다. 하지만 계산에 쓸 수 있으리라 기대되는 데이터 타입은 모두 결정 가능한 동등성을 갖추고 있습니다. 또한 Classical 네임스페이스를 열고 noncomputable section을 선언하여 고전적으로 작업하면, 어떤 타입의 원소로 이루어진 finset이든 추론할 수 있습니다.

Finset은 집합이 지원하는 집합론적 연산을 대부분 지원합니다:

open Finset

variable (a b c : Finset ℕ)
variable (n : ℕ)

#check a ∩ b
#check a ∪ b
#check a \ b
#check (∅ : Finset ℕ)

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by
  ext x; simp only [mem_inter, mem_union]; tauto

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by rw [inter_union_distrib_left]

finset에 관한 정리들이 들어 있는 Finset 네임스페이스를 열어 두었다는 점에 유의하십시오. 아래의 마지막 예제를 한 단계씩 따라가 보면, ext를 적용한 뒤 simp를 적용하면 항등식이 명제 논리 문제로 환원되는 것을 확인할 수 있습니다. 연습 문제로, Chapter 4의 집합 항등식 중 일부를 finset으로 옮겨 증명해 볼 수 있습니다.

자연수의 유한 집합 \(\{ 0, 1, \ldots, n-1 \}\)을 나타내는 Finset.range n 표기법은 이미 보았습니다. Finset을 사용하면 원소를 나열하여 유한 집합을 정의할 수도 있습니다:

#check ({0, 2, 5} : Finset Nat)

def example1 : Finset ℕ := {0, 1, 2}

이렇게 표현된 집합에서 원소의 순서와 중복이 중요하지 않다는 것을 Lean이 인식하도록 하는 방법은 여러 가지가 있습니다.

example : ({0, 1, 2} : Finset ℕ) = {1, 2, 0} := by decide

example : ({0, 1, 2} : Finset ℕ) = {0, 1, 1, 2} := by decide

example : ({0, 1} : Finset ℕ) = {1, 0} := by rw [Finset.pair_comm]

example (x : Nat) : ({x, x} : Finset ℕ) = {x} := by simp

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp [or_comm, or_left_comm]

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp; tauto

Finset에 원소 하나를 추가하려면 insert를, 원소 하나를 삭제하려면 Finset.erase를 사용하면 됩니다. erase는 Finset 네임스페이스에 있지만 insert는 루트 네임스페이스에 있다는 점에 유의하십시오.

example (s : Finset ℕ) (a : ℕ) (h : a ∉ s) : (insert a s |>.erase a) = s :=
  Finset.erase_insert h

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : insert a (s.erase a) = s :=
  Finset.insert_erase h

사실 {0, 1, 2}는 insert 0 (insert 1 (singleton 2))를 나타내는 표기법일 뿐입니다.

set_option pp.notation false in
#check ({0, 1, 2} : Finset ℕ)

finset s와 술어 P가 주어지면, 조건제시법 표기 {x ∈ s | P x}를 사용하여 s의 원소 중 P를 만족하는 원소들의 집합을 정의할 수 있습니다. 이것은 Finset.filter P s를 나타내는 표기법이며, s.filter P로 쓸 수도 있습니다.

example : {m ∈ range n | Even m} = (range n).filter Even := rfl
example : {m ∈ range n | Even m ∧ m ≠ 3} = (range n).filter (fun m ↦ Even m ∧ m ≠ 3) := rfl

example : {m ∈ range 10 | Even m} = {0, 2, 4, 6, 8} := by decide

Mathlib은 함수에 의한 finset의 상(image)이 finset이라는 것을 알고 있습니다.

#check (range 5).image (fun x ↦ x * 2)

example : (range 5).image (fun x ↦ x * 2) = {x ∈ range 10 | Even x} := by decide

Lean은 또한 두 finset의 데카르트 곱 s ×ˢ t가 finset이라는 것과 finset의 멱집합이 finset이라는 것도 알고 있습니다. (s ×ˢ t 표기법은 집합에도 사용할 수 있다는 점에 유의하십시오.)

#check s ×ˢ t
#check s.powerset

finset의 연산을 원소를 이용해 정의하기는 까다롭습니다. 그러한 정의는 모두 원소가 제시되는 순서와 무관해야 하기 때문입니다. 물론 기존 연산을 조합하여 함수를 정의하는 방법은 언제나 쓸 수 있습니다. 또 다른 방법은 Finset.fold를 사용하여 원소들에 대해 이항 연산을 접는(fold) 것입니다. 단, 그 연산이 결합법칙과 교환법칙을 만족해야 합니다. 이 성질들이 연산이 적용되는 순서와 무관하게 결과가 같음을 보장하기 때문입니다. 유한 합, 유한 곱, 유한 합집합이 이러한 방식으로 정의됩니다. 아래 마지막 예제에서 biUnion은 “bounded indexed union”(유계 첨자가 붙은 합집합)을 뜻합니다. 관례적인 수학 표기로는 이 표현식을 \(\bigcup_{i ∈ s} g(i)\)로 씁니다.

#check Finset.fold

def f (n : ℕ) : Int := (↑n)^2

#check (range 5).fold (fun x y : Int ↦ x + y) 0 f
#eval (range 5).fold (fun x y : Int ↦ x + y) 0 f

#check ∑ i ∈ range 5, i^2
#check ∏ i ∈ range 5, i + 1

variable (g : Nat → Finset Int)

#check (range 5).biUnion g

finset에는 자연스러운 귀납법 원리가 있습니다. 모든 finset이 어떤 성질을 가짐을 증명하려면, 공집합이 그 성질을 가지며 finset에 새 원소를 하나 추가해도 그 성질이 유지됨을 보이면 됩니다. (다음 예제의 귀납 단계에서 매개변수 a와 s에 이름을 붙이려면 @insert의 @ 기호가 필요합니다. 이 매개변수들이 암시적(implicit)으로 지정되어 있기 때문입니다.)

#check Finset.induction

example {α : Type*} [DecidableEq α] (f : α → ℕ)  (s : Finset α) (h : ∀ x ∈ s, f x ≠ 0) :
    ∏ x ∈ s, f x ≠ 0 := by
  induction s using Finset.induction_on with
  | empty => simp
  | @insert a s anins ih =>
    rw [prod_insert anins]
    apply mul_ne_zero
    · apply h; apply mem_insert_self
    apply ih
    intros x xs
    exact h x (mem_insert_of_mem xs)

s가 finset이면 Finset.Nonempty s는 ∃ x, x ∈ s로 정의됩니다. 고전적 선택을 사용하면 비어 있지 않은 finset에서 원소를 하나 고를 수 있습니다. 마찬가지로 라이브러리는 Finset.toList s를 정의하는데, 이 함수는 선택을 사용하여 s의 원소들을 어떤 순서로 골라 나열합니다.

noncomputable example (s : Finset ℕ) (h : s.Nonempty) : ℕ := Classical.choose h

example (s : Finset ℕ) (h : s.Nonempty) : Classical.choose h ∈ s := Classical.choose_spec h

noncomputable example (s : Finset ℕ) : List ℕ := s.toList

example (s : Finset ℕ) (a : ℕ) : a ∈ s.toList ↔ a ∈ s := mem_toList

Finset.min과 Finset.max를 사용하면 선형 순서의 원소로 이루어진 finset에서 최소 원소나 최대 원소를 고를 수 있습니다. 마찬가지로 격자의 원소로 이루어진 finset에는 Finset.inf와 Finset.sup을 사용할 수 있습니다. 하지만 한 가지 주의할 점이 있습니다. 빈 finset의 최소 원소는 무엇이어야 합니까? 아래 함수들 가운데 프라임이 붙은 버전에는 finset이 비어 있지 않다는 전제 조건이 추가되어 있음을 확인할 수 있습니다. 프라임이 붙지 않은 버전인 Finset.min과 Finset.max는 finset이 비어 있는 경우를 처리하기 위해 출력 타입에 각각 최대 원소 또는 최소 원소를 추가합니다. 프라임이 붙지 않은 버전인 Finset.inf와 Finset.sup은 격자가 각각 최대 원소 또는 최소 원소를 갖추고 있다고 가정합니다.

#check Finset.min
#check Finset.min'
#check Finset.max
#check Finset.max'
#check Finset.inf
#check Finset.inf'
#check Finset.sup
#check Finset.sup'

example : Finset.Nonempty {2, 6, 7} := ⟨6, by trivial⟩
example : Finset.min' {2, 6, 7} ⟨6, by trivial⟩ = 2 := by trivial

모든 finset s는 유한한 기수 Finset.card s를 가지며, Finset 네임스페이스가 열려 있을 때는 이를 #s로 쓸 수 있습니다.

#check Finset.card

#eval (range 5).card

example (s : Finset ℕ) : s.card = #s := by rfl

example (s : Finset ℕ) : s.card = ∑ _i ∈ s, 1 := by rw [card_eq_sum_ones]

example (s : Finset ℕ) : s.card = ∑ _i ∈ s, 1 := by simp

다음 절은 전적으로 기수에 관한 추론을 다룹니다.

수학을 형식화할 때는 정의와 정리를 집합으로 표현할지 타입으로 표현할지 결정해야 하는 경우가 많습니다. 타입을 사용하면 표기와 증명이 간단해지는 경우가 많지만, 타입의 부분집합을 다루는 편이 더 유연할 수 있습니다. finset에 대응하는 타입 기반 개념은 fintype, 즉 어떤 α에 대한 타입 Fintype α입니다. 정의에 따르면 fintype은 자신의 모든 원소를 포함하는 finset univ를 갖춘 데이터 타입일 뿐입니다.

variable {α : Type*} [Fintype α]

example : ∀ x : α, x ∈ Finset.univ := by
  intro x; exact mem_univ x

Fintype.card α는 대응하는 finset의 기수와 같습니다.

example : Fintype.card α = (Finset.univ : Finset α).card := rfl

우리는 이미 fintype의 대표적인 예를 살펴보았습니다. 바로 각 n에 대한 Fin n 타입들입니다. Lean은 fintype이 곱 연산과 같은 연산에 대해 닫혀 있다는 것을 인식합니다.

example : Fintype.card (Fin 5) = 5 := by simp
example : Fintype.card ((Fin 5) × (Fin 3)) = 15 := by simp

Finset α의 임의의 원소 s는 타입 (↑s : Type α), 즉 α의 원소 가운데 s에 포함된 원소들로 이루어진 부분타입으로 강제 변환될 수 있습니다. 게다가 Lean은 ↑s가 fintype이라는 것을 알고 있습니다.

variable (s : Finset ℕ)

example : (↑s : Type) = {x : ℕ // x ∈ s} := rfl
example : Fintype.card ↑s = s.card := by simp

Lean과 Mathlib은 타입 클래스 추론을 사용하여 fintype의 추가 구조, 즉 모든 원소를 포함하는 전체 finset을 추적합니다. 다시 말해, fintype을 그러한 추가 데이터를 갖춘 대수적 구조로 생각할 수 있습니다. 이것이 어떻게 작동하는지는 Chapter 7에서 설명합니다.

6.2. 개수 세기 논증

대상을 세는 기술은 조합론의 핵심적인 부분입니다. Mathlib에는 finset의 원소 개수를 세기 위한 몇 가지 기본 항등식이 있습니다.

open Finset

variable {α β : Type*} [DecidableEq α] [DecidableEq β] (s t : Finset α) (f : α → β)

example : #(s ×ˢ t) = #s * #t := by rw [card_product]
example : #(s ×ˢ t) = #s * #t := by simp

example : #(s ∪ t) = #s + #t - #(s ∩ t) := by rw [card_union]

example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by rw [card_union_of_disjoint h]
example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by simp [h]

example (h : Function.Injective f) : #(s.image f) = #s := by rw [card_image_of_injective _ h]

example (h : Set.InjOn f s) : #(s.image f) = #s := by rw [card_image_of_injOn h]

Finset 네임스페이스를 열면 s.card를 #s 표기로 쓸 수 있고, card_union 등의 축약된 이름도 사용할 수 있습니다.

Mathlib은 fintype의 원소 개수도 셀 수 있습니다.

open Fintype

variable {α β : Type*} [Fintype α] [Fintype β]

example : card (α × β) = card α * card β := by simp

example : card (α ⊕ β) = card α + card β := by simp

example (n : ℕ) : card (Fin n → α) = (card α)^n := by simp

variable {n : ℕ} {γ : Fin n → Type*} [∀ i, Fintype (γ i)]

example : card ((i : Fin n) → γ i) = ∏ i, card (γ i) := by simp

example : card (Σ i, γ i) = ∑ i, card (γ i) := by simp

Fintype 네임스페이스가 열려 있지 않으면 card 대신 Fintype.card를 사용해야 합니다.

다음은 finset의 기수를 계산하는 예입니다. 구체적으로는 range n과, range n을 n보다 크게 이동시킨 복사본의 합집합의 기수를 계산합니다. 이 계산을 하려면 합집합을 이루는 두 집합이 서로소임을 보여야 합니다. 증명의 첫 줄에서 부가 조건 Disjoint (range n) (image (fun i ↦ m + i) (range n))이 생기며, 이 조건은 증명의 마지막 부분에서 증명됩니다. Disjoint 술어는 너무 일반적이어서 그대로는 쓰기 어렵지만, 정리 disjoint_iff_ne를 쓰면 이를 우리가 사용할 수 있는 형태로 바꿀 수 있습니다.

#check Disjoint

example (m n : ℕ) (h : m ≥ n) :
    card (range n ∪ (range n).image (fun i ↦ m + i)) = 2 * n := by
  rw [card_union_of_disjoint, card_range, card_image_of_injective, card_range]; omega
  . apply add_right_injective
  . simp [disjoint_iff_ne]; omega

이 절 전체에서 omega는 산술 계산과 부등식을 처리하는 주력 도구가 될 것입니다.

좀 더 흥미로운 예제를 살펴보겠습니다. \(\{0, \ldots, n\} \times \{0, \ldots, n\}\)의 부분집합 중에서 \(i < j\)를 만족하는 쌍 \((i, j)\)로 이루어진 부분집합을 생각해 봅시다. 이 쌍들을 좌표평면 위의 격자점으로 생각하면, 이들은 꼭짓점이 \((0, 0)\)과 \((n, n)\)인 정사각형에서 대각선을 제외한 위쪽 삼각형을 이룹니다. 전체 정사각형의 기수는 \((n + 1)^2\)이고, 여기서 대각선의 크기를 빼고 그 결과를 절반으로 나누면 삼각형의 기수가 \(n (n + 1) / 2\)임을 알 수 있습니다.

또는 삼각형의 행들의 크기가 \(0, 1, \ldots, n\)이므로, 기수가 처음 \(n\)개의 양의 정수의 합이라는 점에 주목할 수도 있습니다. 아래 증명의 첫 번째 have는 삼각형을 행들의 합집합으로 나타내며, 여기서 행 \(j\)는 수 \(0, 1, ..., j - 1\)을 각각 \(j\)와 짝지은 쌍들로 이루어집니다. 아래 증명에서 (., j) 표기는 함수 fun i ↦ (i, j)를 줄여 쓴 것입니다. 증명의 나머지 부분은 finset 기수에 대한 계산일 뿐입니다.

def triangle (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range (n+1) ×ˢ range (n+1) | p.1 < p.2}

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n = (range (n+1)).biUnion (fun j ↦ (range j).image (., j)) := by
    ext p
    simp only [triangle, mem_filter, mem_product, mem_range, mem_biUnion, mem_image]
    constructor
    . rintro ⟨⟨hp1, hp2⟩, hp3⟩
      use p.2, hp2, p.1, hp3
    . rintro ⟨p1, hp1, p2, hp2, rfl⟩
      omega
  rw [this, card_biUnion]; swap
  · -- take care of disjointness first
    intro x _ y _ xney
    simp [disjoint_iff_ne, xney]
  -- continue the calculation
  transitivity (∑ i ∈ range (n + 1), i)
  · congr; ext i
    rw [card_image_of_injective, card_range]
    intros i1 i2; simp
  rw [sum_range_id]; rfl

다음은 이 증명의 변형으로, finset 대신 fintype을 사용하여 계산을 수행합니다. 타입 α ≃ β는 α와 β 사이의 동치(equivalence)들의 타입으로, 정방향 사상, 역방향 사상, 그리고 이 둘이 서로의 역이라는 증명으로 구성됩니다. 증명의 첫 번째 have는 triangle n이 i가 Fin (n + 1)에 걸쳐 변할 때의 Fin i들의 서로소 합집합과 동치임을 보여 줍니다. 흥미롭게도 정방향 함수와 역방향 함수는 명시적으로 작성되지 않고 택틱으로 구성됩니다. 이 함수들은 데이터와 정보를 옮기는 일 외에는 아무것도 하지 않으므로, rfl로 이들이 서로의 역임을 확립할 수 있습니다.

그다음 rw [←Fintype.card_coe]는 #(triangle n)을 부분타입 { x // x ∈ triangle n }의 기수로 다시 쓰며, 나머지 증명은 계산입니다.

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n ≃ Σ i : Fin (n + 1), Fin i.val :=
    { toFun := by
        rintro ⟨⟨i, j⟩, hp⟩
        have : (i ≤ n ∧ j ≤ n) ∧ i < j := by simpa [triangle] using hp
        exact ⟨⟨j, by linarith⟩, ⟨i, by linarith⟩⟩
      invFun := by
        rintro ⟨i, j⟩
        use ⟨j, i⟩
        suffices j ≤ n ∧ i ≤ n by simpa [triangle]
        constructor <;> linarith [i.2, j.2]
      left_inv := by intro i; rfl
      right_inv := by intro i; rfl }
  rw [←Fintype.card_coe]
  trans; apply (Fintype.card_congr this)
  rw [Fintype.card_sigma, sum_fin_eq_sum_range]
  convert! Finset.sum_range_id (n + 1)
  simp_all

또 다른 접근 방식도 있습니다. 아래 증명의 첫 줄은 문제를 2 * #(triangle n) = (n + 1) * n을 보이는 것으로 환원합니다. 이는 삼각형 두 개가 직사각형 range n ×ˢ range (n + 1)을 정확히 채운다는 것을 보임으로써 할 수 있습니다. 연습 문제로, 계산의 단계들을 채울 수 있는지 시도해 보십시오. 풀이에서는 끝에서 두 번째 단계에서 omega에 크게 의존하지만, 안타깝게도 상당한 양의 작업을 손으로 직접 해야 합니다.

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  apply Nat.eq_div_of_mul_eq_right (by norm_num)
  let turn (p : ℕ × ℕ) : ℕ × ℕ := (n - 1 - p.1, n - p.2)
  calc 2 * #(triangle n)
      = #(triangle n) + #(triangle n) := by
          sorry
    _ = #(triangle n) + #(triangle n |>.image turn) := by
          sorry
    _ = #(range n ×ˢ range (n + 1)) := by
          sorry
    _ = (n + 1) * n := by
          sorry

triangle의 정의에서 n을 n + 1로 바꾸고 <를 ≤로 바꾸면 같은 삼각형이 아래로 이동한 모양을 얻는다는 것을 직접 확인할 수 있습니다. 아래 연습 문제에서는 이 사실을 이용하여 두 삼각형의 크기가 같음을 보여야 합니다.

def triangle' (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range n ×ˢ range n | p.1 ≤ p.2}

example (n : ℕ) : #(triangle' n) = #(triangle n) := by sorry

2023년 Lean for the Curious Mathematician에서 Bhavik Mehta가 진행한 조합론 튜토리얼의 예제와 연습 문제로 이 절을 마무리합시다. 꼭짓점 집합이 s와 t인 이분 그래프가 있고, s의 모든 a에 대해 a에서 나가는 간선이 적어도 세 개 있으며, t의 모든 b에 대해 b로 들어오는 간선이 많아야 하나라고 가정합시다. 그러면 그래프의 간선의 총 개수는 s의 기수의 세 배 이상이고 t의 기수 이하이며, 이로부터 s의 기수의 세 배가 t의 기수 이하라는 결론이 나옵니다. 다음 정리는 이 논증을 구현하며, 여기서는 관계 r을 사용하여 그래프의 간선을 나타냅니다. 증명은 우아한 계산으로 이루어집니다.

open Classical
variable (s t : Finset ℕ) (a b : ℕ)

theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β)
    (r : α → β → Prop)
    (h_left : ∀ a ∈ s, 3 ≤ #{b ∈ t | r a b})
    (h_right : ∀ b ∈ t, #{a ∈ s | r a b} ≤ 1) :
    3 * #(s) ≤ #(t) := by
  calc 3 * #(s)
      = ∑ a ∈ s, 3                               := by simp [mul_comm]
    _ ≤ ∑ a ∈ s, #({b ∈ t | r a b})              := sum_le_sum h_left
    _ = ∑ a ∈ s, ∑ b ∈ t, if r a b then 1 else 0 := by simp
    _ = ∑ b ∈ t, ∑ a ∈ s, if r a b then 1 else 0 := sum_comm
    _ = ∑ b ∈ t, #({a ∈ s | r a b})              := by simp
    _ ≤ ∑ b ∈ t, 1                               := sum_le_sum h_right
    _ ≤ #(t)                                     := by simp

다음 연습 문제도 Mehta의 튜토리얼에서 가져왔습니다. A가 n + 1개의 원소를 가진 range (2 * n)의 부분집합이라고 가정합시다. A가 연속한 두 정수를 반드시 포함하고, 따라서 서로소인 두 원소를 포함한다는 것은 쉽게 알 수 있습니다. 튜토리얼을 보면 다음 사실을 증명하는 데 상당한 노력이 들었다는 것을 알 수 있는데, 이 사실은 이제 omega가 자동으로 증명합니다.

example (m k : ℕ) (h : m ≠ k) (h' : m / 2 = k / 2) : m = k + 1 ∨ k = m + 1 := by omega

Mehta의 연습 문제 풀이에서는 exists_lt_card_fiber_of_mul_lt_card_of_maps_to 형태의 비둘기집 원리를 사용하여, A에 m / 2 = k / 2를 만족하는 서로 다른 두 원소 m과 k가 존재함을 보입니다. 그 사실의 정당화를 완성한 다음, 이를 이용하여 증명을 마무리할 수 있는지 시도해 보십시오.

example {n : ℕ} (A : Finset ℕ)
    (hA : #(A) = n + 1)
    (hA' : A ⊆ range (2 * n)) :
    ∃ m ∈ A, ∃ k ∈ A, Nat.Coprime m k := by
  have : ∃ t ∈ range n, 1 < #({u ∈ A | u / 2 = t}) := by
    apply exists_lt_card_fiber_of_mul_lt_card_of_maps_to
    · sorry
    · sorry
  rcases this with ⟨t, ht, ht'⟩
  simp only [one_lt_card, mem_filter] at ht'
  sorry

6.3. 귀납적으로 정의된 타입

Lean의 기반 이론을 사용하면 귀납적 타입, 즉 인스턴스가 아래에서 위로 생성되는 데이터 타입을 정의할 수 있습니다. 예를 들어, α의 원소로 이루어진 리스트의 데이터 타입 List α는 빈 리스트 nil에서 시작하여 리스트 앞쪽에 원소를 차례로 추가함으로써 생성됩니다. 아래에서는 이진 트리의 타입 BinTree를 정의할 것입니다. 이 타입의 원소는 빈 트리에서 시작하여, 기존의 두 트리에 새 노드를 붙여 새로운 트리를 만드는 방식으로 생성됩니다.

Lean에서는 가산 개로 가지가 뻗는 정초 트리처럼 대상이 무한한 귀납적 타입도 정의할 수 있습니다. 그러나 이산 수학에서는, 특히 컴퓨터 과학과 관련된 이산 수학 분야에서는 유한한 귀납적 정의가 흔히 사용됩니다. Lean은 이러한 타입을 정의하는 수단뿐만 아니라 귀납법의 원리와 재귀에 의한 정의의 원리도 제공합니다. 예를 들어, 데이터 타입 List α는 다음과 같이 귀납적으로 정의됩니다:

namespace MyListSpace

inductive List (α : Type*) where
  | nil  : List α
  | cons : α → List α → List α

end MyListSpace

귀납적 정의에 따르면 List α의 모든 원소는 빈 리스트인 nil이거나 cons a as이며, 여기서 a는 α의 원소이고 as는 α의 원소들로 이루어진 리스트입니다. 생성자의 정식 이름은 List.nil과 List.cons이지만, List 네임스페이스가 열려 있을 때는 더 짧은 표기를 사용할 수 있습니다. List 네임스페이스가 열려 있지 않을 때는 Lean이 리스트를 기대하는 곳이라면 어디서나 .nil과 .cons a as라고 쓸 수 있으며, Lean이 자동으로 List 한정자를 삽입합니다. 이 절 전체에서는 표준 라이브러리와의 충돌을 피하기 위해 임시 정의를 MyListSpace와 같은 별도의 네임스페이스에 넣겠습니다. 임시 네임스페이스 밖에서는 다시 표준 라이브러리의 정의를 사용합니다.

Lean은 nil을 나타내는 표기로 []를, cons를 나타내는 표기로 ::를 정의하며, a :: b :: c :: [] 대신 [a, b, c]라고 쓸 수 있습니다. append 함수와 map 함수는 다음과 같이 재귀적으로 정의됩니다:

def append {α : Type*} : List α → List α → List α
  | [],      bs => bs
  | a :: as, bs => a :: append as bs

def map {α β : Type*} (f : α → β) : List α → List β
  | []      => []
  | a :: as => f a :: map f as

#eval append [1, 2, 3] [4, 5, 6]
#eval map (fun n => n^2) [1, 2, 3, 4, 5]

기저 사례와 재귀 사례가 있다는 점에 주목하십시오. 각 경우에 두 정의 절은 정의상 성립합니다:

theorem nil_append {α : Type*} (as : List α) : append [] as = as := rfl

theorem cons_append {α : Type*} (a : α) (as : List α) (bs : List α) :
    append (a :: as) bs = a :: append as bs := rfl

theorem map_nil {α β : Type*} (f : α → β) : map f [] = [] := rfl

theorem map_cons {α β : Type*} (f : α → β) (a : α) (as : List α) :
    map f (a :: as) = f a :: map f as := rfl

append 함수와 map 함수는 표준 라이브러리에 정의되어 있으며, append as bs는 as ++ bs로 쓸 수 있습니다.

Lean에서는 정의의 구조를 따라 귀납법으로 증명을 작성할 수 있습니다.

variable {α β γ : Type*}
variable (as bs cs : List α)
variable (a b c : α)

open List

theorem append_nil : ∀ as : List α, as ++ [] = as
  | [] => rfl
  | a :: as => by rw [cons_append, append_nil as]

theorem map_map (f : α → β) (g : β → γ) :
    ∀ as : List α, map g (map f as) = map (g ∘ f) as
  | [] => rfl
  | a :: as => by rw [map_cons, map_cons, map_cons, map_map f g as]; rfl

induction' 택틱을 사용할 수도 있습니다.

물론 이 정리들은 이미 표준 라이브러리에 들어 있습니다. 연습 삼아, 리스트를 뒤집는 함수 reverse를 MyListSpace3 네임스페이스에 정의해 보십시오(표준 List.reverse와 충돌하지 않도록 하기 위함입니다). #eval reverse [1, 2, 3, 4, 5]를 사용하여 시험해 볼 수 있습니다. reverse를 가장 단순하게 정의하면 이차 시간이 걸리지만, 그 점은 신경 쓰지 않아도 됩니다. 표준 라이브러리에 있는 List.reverse의 정의로 이동하면 선형 시간 구현을 볼 수 있습니다. reverse (as ++ bs) = reverse bs ++ reverse as와 reverse (reverse as) = as를 증명해 보십시오. cons_append와 append_assoc을 사용할 수 있지만, 보조적인 보조정리를 직접 고안하여 증명해야 할 수도 있습니다.

def reverse : List α → List α := sorry

theorem reverse_append (as bs : List α) : reverse (as ++ bs) = reverse bs ++ reverse as := by
  sorry

theorem reverse_reverse (as : List α) : reverse (reverse as) = as := by sorry

또 다른 예로, 이진 트리의 다음 귀납적 정의와 함께 이진 트리의 크기와 깊이를 계산하는 함수들을 살펴보십시오.

inductive BinTree where
  | empty : BinTree
  | node  : BinTree → BinTree → BinTree

namespace BinTree

def size : BinTree → ℕ
  | empty    => 0
  | node l r => size l + size r + 1

def depth : BinTree → ℕ
  | empty    => 0
  | node l r => max (depth l) (depth r) + 1

빈 이진 트리를 크기 0, 깊이 0인 이진 트리로 간주하면 편리합니다. 문헌에서는 이 데이터 타입을 확장 이진 트리(extended binary trees)라고 부르기도 합니다. 빈 트리를 포함한다는 것은, 예를 들어 루트 노드, 비어 있는 왼쪽 부분 트리, 그리고 노드 하나로 이루어진 오른쪽 부분 트리로 구성된 트리 node empty (node empty empty)를 정의할 수 있다는 뜻입니다.

다음은 크기와 깊이 사이의 관계를 나타내는 중요한 부등식입니다.

theorem size_le : ∀ t : BinTree, size t ≤ 2^depth t - 1
  | empty    => Nat.zero_le _
  | node l r => by
    simp only [depth, size]
    calc l.size + r.size + 1
      ≤ (2^l.depth - 1) + (2^r.depth - 1) + 1 := by
          gcongr <;> apply size_le
    _ ≤ (2 ^ max l.depth r.depth - 1) + (2 ^ max l.depth r.depth - 1) + 1 := by
          gcongr <;> simp
    _ ≤ 2 ^ (max l.depth r.depth + 1) - 1 := by
          have : 0 < 2 ^ max l.depth r.depth := by simp
          omega

다음 부등식을 증명해 보십시오. 이 부등식은 조금 더 쉽습니다. 앞의 정리에서처럼 귀납법으로 증명한다면 := by를 지워야 한다는 점을 기억하십시오.

theorem depth_le_size : ∀ t : BinTree, depth t ≤ size t := by sorry

이진 트리에 대한 flip 연산도 정의하십시오. 이 연산은 왼쪽 부분 트리와 오른쪽 부분 트리를 재귀적으로 맞바꿉니다.

def flip : BinTree → BinTree := sorry

올바르게 했다면 다음의 증명은 rfl이어야 합니다.

example: flip  (node (node empty (node empty empty)) (node empty empty)) =
    node (node empty empty) (node (node empty empty) empty) := sorry

다음을 증명하십시오:

theorem size_flip : ∀ t, size (flip t) = size t := by sorry

이 절은 약간의 형식 논리로 마무리합니다. 다음은 명제 논리식의 귀납적 정의입니다.

inductive PropForm : Type where
  | var (n : ℕ)           : PropForm
  | fls                   : PropForm
  | conj (A B : PropForm) : PropForm
  | disj (A B : PropForm) : PropForm
  | impl (A B : PropForm) : PropForm

모든 명제 논리식은 변수 var n, 상수 거짓 fls, 또는 conj A B, disj A B, impl A B 형태의 복합 논리식 중 하나입니다. 일반적인 수학 표기법으로는 이들을 각각 \(p_n\), \(\bot\), \(A \wedge B\), \(A \vee B\), \(A \to B\)로 흔히 씁니다. 다른 명제 결합자는 이들을 사용하여 정의할 수 있습니다. 예를 들어 \(\neg A\)는 \(A \to \bot\)로, \(A \leftrightarrow B\)는 \((A \to B) \wedge (B \to A)\)로 정의할 수 있습니다.

명제 논리식의 데이터 타입을 정의했으니, 이제 변수에 불리언 진릿값을 대응시키는 할당 v에 대하여 명제 논리식을 평가한다는 것이 무엇을 의미하는지 정의합니다.

def eval : PropForm → (ℕ → Bool) → Bool
  | var n,    v => v n
  | fls,      _ => false
  | conj A B, v => A.eval v && B.eval v
  | disj A B, v => A.eval v || B.eval v
  | impl A B, v => ! A.eval v || B.eval v

다음 정의는 논리식에 나타나는 변수들의 집합을 지정하고, 이어지는 정리는 논리식의 변수들에서 일치하는 두 진릿값 할당으로 논리식을 평가하면 같은 값이 나온다는 것을 보여 줍니다.

def vars : PropForm → Finset ℕ
  | var n    => {n}
  | fls      => ∅
  | conj A B => A.vars ∪ B.vars
  | disj A B => A.vars ∪ B.vars
  | impl A B => A.vars ∪ B.vars

theorem eval_eq_eval : ∀ (A : PropForm) (v1 v2 : ℕ → Bool),
    (∀ n ∈ A.vars, v1 n = v2 n) → A.eval v1 = A.eval v2
  | var n, v1, v2, h    => by simp_all [vars, eval]
  | fls, v1, v2, h      => by simp_all [eval]
  | conj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | disj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | impl A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]

반복되는 부분이 있다는 점을 알아차리면 자동화를 영리하게 활용할 수 있습니다.

theorem eval_eq_eval' (A : PropForm) (v1 v2 : ℕ → Bool) (h : ∀ n ∈ A.vars, v1 n = v2 n) :
    A.eval v1 = A.eval v2 := by
  cases A <;> simp_all [eval, vars, fun A => eval_eq_eval' A v1 v2]

함수 subst A m C는 논리식 A에 나타나는 변수 var m의 모든 출현을 논리식 C로 치환한 결과를 나타냅니다.

def subst : PropForm → ℕ → PropForm → PropForm
  | var n,    m, C => if n = m then C else var n
  | fls,      _, _ => fls
  | conj A B, m, C => conj (A.subst m C) (B.subst m C)
  | disj A B, m, C => disj (A.subst m C) (B.subst m C)
  | impl A B, m, C => impl (A.subst m C) (B.subst m C)

예를 들어, 논리식에 나타나지 않는 변수를 치환해도 아무런 효과가 없음을 보이십시오:

theorem subst_eq_of_not_mem_vars :
    ∀ (A : PropForm) (n : ℕ) (C : PropForm), n ∉ A.vars → A.subst n C = A := sorry

다음 정리는 더 미묘하고 흥미로운 내용을 말합니다. 진리 할당 v에서 A.subst n C를 평가하는 것은 var n에 C의 값을 할당하는 진리 할당에서 A를 평가하는 것과 같습니다. 이를 증명할 수 있는지 시도해 보십시오.

theorem subst_eval_eq : ∀ (A : PropForm) (n : ℕ) (C : PropForm) (v : ℕ → Bool),
  (A.subst n C).eval v = A.eval (fun m => if m = n then C.eval v else v m) := sorry