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

insert를 사용하여 Finset에 원소 하나를 추가할 수 있고, 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}를 사용하여 P를 만족하는 s의 원소들의 집합을 정의할 수 있습니다. 이는 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를 사용해 원소들에 대해 이항 연산을 접는 것인데, 이때 연산이 결합적이고 교환적이어야 합니다. 이러한 성질이 연산을 적용하는 순서와 무관하게 결과가 동일함을 보장하기 때문입니다. 유한합, 유한곱, 유한합집합은 이러한 방식으로 정의됩니다. 아래의 마지막 예제에서 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에 새 원소를 하나 추가해도 그 성질이 보존됨을 보이면 됩니다. (다음 예제의 귀납 단계에서 @insert의 @ 기호는 매개변수 a와 s에 이름을 붙이기 위해 필요한데, 이는 이들이 암시적으로 표시되어 있기 때문입니다.)

#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의 원소를 하나 고를 수 있습니다. 마찬가지로, 라이브러리는 선택 공리를 사용하여 s의 원소들을 어떤 순서로 골라내는 Finset.toList 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에서 최소 또는 최대 원소를 선택할 때는 Finset.min과 Finset.max를 사용할 수 있으며, 마찬가지로 격자의 원소로 이루어진 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 위의 추가 구조, 즉 모든 원소를 포함하는 universal 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의 크기(cardinality)를 계산하는 예시로, 즉 range n과 n보다 크게 이동된 range n의 복사본의 합집합입니다. 이 계산에는 합집합에 있는 두 집합이 서로소(disjoint)임을 보이는 과정이 필요합니다. 증명의 첫 번째 줄에서 부수 조건 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는 산술 계산과 부등식을 다루는 데 있어 우리의 주력 도구가 될 것입니다.

더 흥미로운 예제를 살펴보겠습니다. 조건 \(i < j\)를 만족하는 순서쌍 \((i, j)\)로 이루어진 \(\{0, \ldots, n\} \times \{0, \ldots, n\}\)의 부분집합을 생각해 봅시다. 이를 좌표평면의 격자점으로 생각하면, 이들은 대각선을 포함하지 않는, 꼭짓점이 \((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)를 축약한 것입니다. 증명의 나머지 부분은 유한집합 원소 개수에 대한 계산일 뿐입니다.

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을 사용하여 계산을 수행합니다. 타입 α ≃ β는 α와 β 사이의 동치 관계의 타입이며, 정방향 함수와 역방향 함수, 그리고 이 둘이 서로 역함수 관계임을 보이는 증명으로 구성됩니다. 증명의 첫 번째 have는 i가 Fin (n + 1)을 범위로 할 때 triangle n이 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' 택틱을 사용할 수도 있습니다.

물론 이러한 정리들은 이미 표준 라이브러리에 있습니다. 연습 삼아, (표준 List.reverse와 충돌하지 않도록) MyListSpace3 네임스페이스에 리스트를 뒤집는 함수 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인 이진 트리로 간주하는 것이 편리합니다. 문헌에서는 이 데이터 타입을 때때로 확장 이진 트리라고 부릅니다. 빈 트리를 포함한다는 것은, 예를 들어 루트 노드, 빈 왼쪽 부분트리, 그리고 단일 노드로 이루어진 오른쪽 부분트리로 구성된 트리 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