7. 구조체

현대 수학은 대수적 구조를 핵심적으로 활용합니다. 대수적 구조는 여러 상황에서 구체화할 수 있는 패턴을 하나로 묶어 줍니다. 수학은 이러한 구조를 정의하고 특정 인스턴스를 구성하는 다양한 방법을 제공합니다.

따라서 Lean도 구조를 형식적으로 정의하고 다루는 방법을 그에 맞게 제공합니다. 여러분은 이미 Chapter 2에서 다룬 환과 격자처럼 Lean에서 대수적 구조의 예를 본 적이 있습니다. 이 장에서는 그곳에서 보았던 수수께끼 같은 대괄호 표기인 [Ring α]와 [Lattice α]를 설명합니다. 또한 대수적 구조를 직접 정의하고 사용하는 방법도 보여 드립니다.

더 자세한 기술적 내용은 Theorem Proving in Lean과 Anne Baanen의 논문 Use and abuse of instance parameters in the Lean mathematical library를 참고하십시오.

7.1. 구조체 정의하기

가장 넓은 의미에서 구조체란 데이터 모음에 대한 명세이며, 그 데이터가 만족해야 하는 제약 조건을 포함할 수도 있습니다. 구조체의 인스턴스는 제약 조건을 만족하는 특정한 데이터 묶음입니다. 예를 들어, 점을 세 실수의 튜플로 명세할 수 있습니다.

@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

@[ext] 표기는 구조체의 두 인스턴스가 성분이 같을 때 서로 같다는 것을 증명하는 데 쓸 수 있는 정리를 자동으로 생성하라고 Lean에 지시합니다. 이러한 성질을 외연성이라고 합니다.

#check Point.ext

example (a b : Point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) : a = b := by
  ext
  repeat' assumption

그런 다음 Point 구조체의 특정 인스턴스를 정의할 수 있습니다. Lean은 이를 위한 여러 가지 방법을 제공합니다.

def myPoint1 : Point where
  x := 2
  y := -1
  z := 4

def myPoint2 : Point :=
  { x := 2, y := -1, z := 4 }

def myPoint3 : Point :=
  ⟨2, -1, 4⟩

def myPoint4 :=
  Point.mk 2 (-1) 4

첫 번째 예제에서는 구조체의 필드 이름을 명시적으로 지정합니다. myPoint4의 정의에서 사용된 함수 Point.mk는 원소를 구성하는 역할을 하므로 Point 구조체의 생성자라고 합니다. 원한다면 build처럼 다른 이름을 지정할 수도 있습니다.

structure Point' where build ::
  x : ℝ
  y : ℝ
  z : ℝ

#check Point'.build 2 (-1) 4

다음 두 예제는 구조체에 대한 함수를 정의하는 방법을 보여 줍니다. 두 번째 예제는 Point.mk 생성자를 명시적으로 사용하는 반면, 첫 번째 예제는 간결함을 위해 익명 생성자를 사용합니다. Lean은 add에 지정된 타입으로부터 해당 생성자를 추론할 수 있습니다. Point와 같은 구조체와 관련된 정의와 정리는 같은 이름의 네임스페이스에 넣는 것이 관례입니다. 아래 예제에서는 Point 네임스페이스를 열었기 때문에 add의 전체 이름은 Point.add입니다. 네임스페이스가 열려 있지 않을 때는 전체 이름을 사용해야 합니다. 하지만 익명 사영 표기를 사용하면 편리한 경우가 많다는 점을 기억하십시오. 이 표기를 사용하면 Point.add a b 대신 a.add b라고 쓸 수 있습니다. a의 타입이 Point이므로 Lean은 전자를 후자로 해석합니다.

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def add' (a b : Point) : Point where
  x := a.x + b.x
  y := a.y + b.y
  z := a.z + b.z

#check add myPoint1 myPoint2
#check myPoint1.add myPoint2

end Point

#check Point.add myPoint1 myPoint2
#check myPoint1.add myPoint2

아래에서도 정의를 계속 해당 네임스페이스에 넣겠지만, 인용하는 코드 조각에서는 네임스페이스 관련 명령을 생략하겠습니다. 덧셈 함수의 성질을 증명하려면 rw를 사용하여 정의를 펼치고, ext를 사용하여 구조체의 두 원소 사이의 등식을 성분 사이의 등식으로 환원할 수 있습니다. 아래에서는 네임스페이스가 열려 있을 때에도 정리의 이름이 Point.add_comm이 되도록 protected 키워드를 사용합니다. 이는 add_comm과 같은 일반적인 정리와의 모호함을 피하고 싶을 때 유용합니다.

protected theorem add_comm (a b : Point) : add a b = add b a := by
  rw [add, add]
  ext <;> dsimp
  repeat' apply add_comm

example (a b : Point) : add a b = add b a := by simp [add, add_comm]

Lean은 내부적으로 정의를 펼치고 사영을 단순화할 수 있기 때문에, 원하는 등식이 정의상으로 성립하는 경우가 있습니다.

theorem add_x (a b : Point) : (a.add b).x = a.x + b.x :=
  rfl

제 5.2 절에서 재귀 함수를 정의했던 방식과 비슷하게, 구조체에 대한 함수를 패턴 매칭을 사용하여 정의할 수도 있습니다. 아래의 두 정의 addAlt와 addAlt'는 본질적으로 같으며, 유일한 차이는 두 번째 정의에서 익명 생성자 표기법을 사용한다는 점입니다. 이런 방식으로 함수를 정의하는 것이 편리할 때도 있고 구조적 에타 축약(eta-reduction) 덕분에 이 대안 정의가 정의상으로 동치이기는 하지만, 이후의 증명에서는 오히려 불편해질 수 있습니다. 특히 rw [addAlt]를 사용하면 match 명제가 포함된 더 복잡한 목표 화면이 남습니다.

def addAlt : Point → Point → Point
  | Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

def addAlt' : Point → Point → Point
  | ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

theorem addAlt_x (a b : Point) : (a.addAlt b).x = a.x + b.x := by
  rfl

theorem addAlt_comm (a b : Point) : addAlt a b = addAlt b a := by
  rw [addAlt, addAlt]
  -- the same proof still works, but the goal view here is harder to read
  ext <;> dsimp
  repeat' apply add_comm

수학적 구성에서는 묶여 있는 정보를 분해한 뒤 다른 방식으로 다시 조합하는 일이 자주 있습니다. 따라서 Lean과 Mathlib이 이를 효율적으로 수행하는 방법을 이렇게 많이 제공하는 것도 당연합니다. 연습 문제로, Point.add가 결합법칙을 만족함을 증명해 보십시오. 그런 다음 점에 대한 스칼라 곱셈을 정의하고, 그것이 덧셈에 대해 분배법칙을 만족함을 보이십시오.

protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by
  sorry

def smul (r : ℝ) (a : Point) : Point :=
  sorry

theorem smul_distrib (r : ℝ) (a b : Point) :
    (smul r a).add (smul r b) = smul r (a.add b) := by
  sorry

구조체를 사용하는 것은 대수적 추상화로 가는 길의 첫걸음에 불과합니다. 아직은 Point.add를 일반적인 + 기호에 연결하거나, Point.add_comm과 Point.add_assoc을 일반적인 add_comm 및 add_assoc 정리에 연결할 방법이 없습니다. 이러한 작업은 구조체 사용의 대수적 측면에 속하며, 이를 수행하는 방법은 다음 절에서 설명하겠습니다. 지금은 구조체를 대상과 정보를 하나로 묶는 방법이라고만 생각하십시오.

구조체가 데이터 타입뿐만 아니라 데이터가 만족해야 하는 제약 조건까지 명시할 수 있다는 점은 특히 유용합니다. Lean에서 후자는 Prop 타입의 필드로 표현됩니다. 예를 들어 표준 2-심플렉스는 \(x ≥ 0\), \(y ≥ 0\), \(z ≥ 0\), \(x + y + z = 1\)을 만족하는 점 \((x, y, z)\)의 집합으로 정의됩니다. 이 개념에 익숙하지 않다면 그림을 그려 보고, 이 집합이 3차원 공간에서 \((1, 0, 0)\), \((0, 1, 0)\), \((0, 0, 1)\)을 꼭짓점으로 하는 정삼각형과 그 내부를 합친 것임을 스스로 확인해 보십시오. 이를 Lean에서 다음과 같이 표현할 수 있습니다:

structure StandardTwoSimplex where
  x : ℝ
  y : ℝ
  z : ℝ
  x_nonneg : 0 ≤ x
  y_nonneg : 0 ≤ y
  z_nonneg : 0 ≤ z
  sum_eq : x + y + z = 1

마지막 네 필드가 x, y, z, 즉 처음 세 필드를 참조한다는 점에 주목하십시오. x와 y를 맞바꾸는, 2-심플렉스에서 자기 자신으로 가는 사상을 정의할 수 있습니다:

def swapXy (a : StandardTwoSimplex) : StandardTwoSimplex
    where
  x := a.y
  y := a.x
  z := a.z
  x_nonneg := a.y_nonneg
  y_nonneg := a.x_nonneg
  z_nonneg := a.z_nonneg
  sum_eq := by rw [add_comm a.y a.x, a.sum_eq]

더 흥미로운 예로, 심플렉스 위의 두 점의 중점을 계산할 수 있습니다. 실수의 나눗셈을 사용하기 위해 이 파일의 시작 부분에 noncomputable section이라는 구문을 추가했습니다.

noncomputable section

def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex
    where
  x := (a.x + b.x) / 2
  y := (a.y + b.y) / 2
  z := (a.z + b.z) / 2
  x_nonneg := div_nonneg (add_nonneg a.x_nonneg b.x_nonneg) (by norm_num)
  y_nonneg := div_nonneg (add_nonneg a.y_nonneg b.y_nonneg) (by norm_num)
  z_nonneg := div_nonneg (add_nonneg a.z_nonneg b.z_nonneg) (by norm_num)
  sum_eq := by field_simp; linarith [a.sum_eq, b.sum_eq]

여기서는 x_nonneg, y_nonneg, z_nonneg를 간결한 증명 항으로 확립했지만, sum_eq는 by를 사용하여 택틱 모드에서 확립합니다.

\(0 \le \lambda \le 1\)을 만족하는 매개변수 \(\lambda\)가 주어지면, 표준 2-심플렉스의 두 점 \(a\)와 \(b\)의 가중 평균 \(\lambda a + (1 - \lambda) b\)를 구할 수 있습니다. 위의 midpoint 함수와 유사하게 그 함수를 정의해 보십시오.

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardTwoSimplex) : StandardTwoSimplex :=
  sorry

구조체는 매개변수에 의존할 수 있습니다. 예를 들어, 표준 2-심플렉스를 임의의 \(n\)에 대한 표준 \(n\)-심플렉스로 일반화할 수 있습니다. 현재 단계에서는 Fin n 타입에 대해 그것이 \(n\)개의 원소를 가진다는 것과 Lean이 그 위에서 합을 구하는 방법을 안다는 것 외에는 아무것도 알 필요가 없습니다.

open BigOperators

structure StandardSimplex (n : ℕ) where
  V : Fin n → ℝ
  NonNeg : ∀ i : Fin n, 0 ≤ V i
  sum_eq_one : (∑ i, V i) = 1

namespace StandardSimplex

def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
    where
  V i := (a.V i + b.V i) / 2
  NonNeg := by
    intro i
    apply div_nonneg
    · linarith [a.NonNeg i, b.NonNeg i]
    norm_num
  sum_eq_one := by
    simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
      a.sum_eq_one, b.sum_eq_one]
    norm_num

end StandardSimplex

연습 문제로, 표준 \(n\)-심플렉스의 두 점의 가중 평균을 정의할 수 있는지 시도해 보십시오. 관련된 합을 다루기 위해 Finset.sum_add_distrib과 Finset.mul_sum을 사용할 수 있습니다.

지금까지 구조체를 사용해 데이터와 성질을 하나로 묶을 수 있음을 보았습니다. 흥미롭게도 구조체는 데이터 없이 성질만 하나로 묶는 데에도 사용할 수 있습니다. 예를 들어, 다음 구조체 IsLinear는 선형성의 두 가지 구성 요소를 하나로 묶습니다.

structure IsLinear (f : ℝ → ℝ) where
  is_additive : ∀ x y, f (x + y) = f x + f y
  preserves_mul : ∀ x c, f (c * x) = c * f x

section
variable (f : ℝ → ℝ) (linf : IsLinear f)

#check linf.is_additive
#check linf.preserves_mul

end

데이터를 하나로 묶는 방법이 구조체만 있는 것은 아니라는 점을 짚고 넘어갈 만합니다. Point 데이터 구조는 일반적인 곱 타입을 사용하여 정의할 수 있고, IsLinear는 간단한 and로 정의할 수 있습니다.

def Point'' :=
  ℝ × ℝ × ℝ

def IsLinear' (f : ℝ → ℝ) :=
  (∀ x y, f (x + y) = f x + f y) ∧ ∀ x c, f (c * x) = c * f x

일반적인 타입 구성은 구성 요소 사이에 의존성이 있는 구조체를 대신하는 데에도 사용할 수 있습니다. 예를 들어 부분타입 구성은 데이터 하나와 성질 하나를 결합합니다. 다음 예제의 PReal 타입은 양의 실수의 타입이라고 생각할 수 있습니다. 모든 x : PReal은 두 성분, 즉 값과 양수라는 성질을 가집니다. 이 구성 요소들에는 ℝ 타입을 가지는 x.val과 0 < x.val이라는 사실을 나타내는 x.property로 접근할 수 있습니다.

def PReal :=
  { y : ℝ // 0 < y }

section
variable (x : PReal)

#check x.val
#check x.property
#check x.1
#check x.2

end

부분타입을 사용해 표준 2-심플렉스는 물론 임의의 \(n\)에 대한 표준 \(n\)-심플렉스도 정의할 수 있었을 것입니다.

def StandardTwoSimplex' :=
  { p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }

def StandardSimplex' (n : ℕ) :=
  { v : Fin n → ℝ // (∀ i : Fin n, 0 ≤ v i) ∧ (∑ i, v i) = 1 }

마찬가지로, 시그마 타입은 순서쌍을 일반화한 것으로, 두 번째 성분의 타입이 첫 번째 성분의 타입에 의존합니다.

def StdSimplex := Σ n : ℕ, StandardSimplex n

section
variable (s : StdSimplex)

#check s.fst
#check s.snd

#check s.1
#check s.2

end

s : StdSimplex가 주어지면, 첫 번째 성분 s.fst는 자연수이고, 두 번째 성분은 그에 대응하는 심플렉스 StandardSimplex s.fst의 원소입니다. 시그마 타입과 부분타입의 차이점은 시그마 타입의 두 번째 성분이 명제가 아니라 데이터라는 점입니다.

그러나 구조체 대신 곱, 부분타입, 시그마 타입을 사용할 수 있다고 하더라도, 구조체를 사용하면 여러 가지 이점이 있습니다. 구조체를 정의하면 내부 표현이 추상화되고, 성분에 접근하는 함수들에 고유한 이름을 붙일 수 있습니다. 이로 인해 증명이 더 견고해집니다. 구조체의 인터페이스에만 의존하는 증명은, 기존 접근자들을 새 정의를 바탕으로 다시 정의하기만 하면 정의를 변경하더라도 일반적으로 계속 동작합니다. 게다가 곧 살펴보겠지만, Lean은 구조체들을 엮어 서로 긴밀하게 연결된 풍부한 계층 구조를 만들고, 그들 사이의 상호작용을 관리하는 기능을 제공합니다.

7.2. 대수적 구조

대수적 구조라는 말이 무엇을 뜻하는지 분명히 하려면 몇 가지 예를 살펴보는 것이 도움이 될 것입니다.

  1. 부분 순서 집합은 집합 \(P\)와 \(P\) 위에서 정의된 추이적이고 반사적이며 반대칭적인 이항 관계 \(\le\)로 이루어집니다.

  2. 군은 결합법칙을 만족하는 이항 연산, 항등식 원소 \(1\), 그리고 \(G\)의 각 \(g\)에 대해 역원을 돌려주는 함수 \(g \mapsto g^{-1}\)을 갖춘 집합 \(G\)로 이루어집니다. 연산이 교환법칙을 만족하면 그 군을 아벨 군 또는 가환 군이라고 합니다.

  3. 격자는 만남(meet)과 이음(join)을 갖는 부분 순서 집합입니다.

  4. 환은 (덧셈으로 표기된) 아벨 군 \((R, +, 0, x \mapsto -x)\)에 결합법칙을 만족하는 곱셈 연산 \(\cdot\)과 항등식 \(1\)을 함께 갖추고, 곱셈이 덧셈에 대해 분배되는 것으로 이루어집니다. 곱셈이 교환법칙을 만족하면 그 환을 가환 환이라고 합니다.

  5. 순서환 \((R, +, 0, -, \cdot, 1, \le)\)은 환과 그 원소들 위의 부분 순서로 이루어지며, \(R\)의 모든 \(a\), \(b\), \(c\)에 대해 \(a \le b\)이면 \(a + c \le b + c\)이고, \(R\)의 모든 \(a\)와 \(b\)에 대해 \(0 \le a\)이고 \(0 \le b\)이면 \(0 \le a b\)입니다.

  6. 거리 공간은 집합 \(X\)와 함수 \(d : X \times X \to \mathbb{R}\)로 이루어지며, 다음 조건을 만족합니다:

    • \(X\)의 모든 \(x\)와 \(y\)에 대해 \(d(x, y) \ge 0\)입니다.

    • \(d(x, y) = 0\)일 필요충분조건은 \(x = y\)인 것입니다.

    • \(X\)의 모든 \(x\)와 \(y\)에 대해 \(d(x, y) = d(y, x)\)입니다.

    • \(X\)의 모든 \(x\), \(y\), \(z\)에 대해 \(d(x, z) \le d(x, y) + d(y, z)\)입니다.

  7. 위상 공간은 집합 \(X\)와, \(X\)의 열린 부분집합이라고 불리는 \(X\)의 부분집합들의 모임 \(\mathcal T\)로 이루어지며, 다음 조건을 만족합니다:

    • 공집합과 \(X\)는 열린 집합입니다.

    • 두 열린 집합의 교집합은 열린 집합입니다.

    • 열린 집합들의 임의의 합집합은 열린 집합입니다.

이 예들 각각에서 구조의 원소들은 바탕 집합이라는 한 집합에 속하며, 이 집합이 때로는 구조 전체를 대신하기도 합니다. 예를 들어 “\(G\)를 군이라고 합시다”라고 말한 다음 “\(g \in G\)라고 합시다”라고 말할 때, 우리는 \(G\)를 구조와 그 바탕 집합 모두를 나타내는 데 사용하고 있습니다. 모든 대수적 구조가 이런 식으로 하나의 바탕 집합과 연관되는 것은 아닙니다. 예를 들어 이분 그래프는 두 집합 사이의 관계를 포함하며, 갈루아 연결도 마찬가지입니다. 범주 또한 흔히 대상과 사상이라고 불리는, 관심 대상이 되는 두 집합을 포함합니다.

이 예시들은 증명 보조기가 대수적 추론을 지원하기 위해 해야 하는 일 몇 가지를 보여 줍니다. 첫째, 증명 보조기는 구조의 구체적인 인스턴스를 인식할 수 있어야 합니다. 수 체계 \(\mathbb{Z}\), \(\mathbb{Q}\), \(\mathbb{R}\)은 모두 순서환이며, 순서환에 관한 일반적인 정리를 이 인스턴스들 중 어디에든 적용할 수 있어야 합니다. 때로는 하나의 구체적인 집합이 둘 이상의 방식으로 어떤 구조의 인스턴스가 될 수도 있습니다. 예를 들어, 실해석학의 기저를 이루는 \(\mathbb{R}\) 위의 통상적인 위상 외에도, 모든 집합이 열린집합인 \(\mathbb{R}\) 위의 이산 위상을 생각할 수도 있습니다.

둘째, 증명 보조기는 구조에 대한 일반적인 표기법을 지원해야 합니다. Lean에서 * 표기는 모든 통상적인 수 체계에서의 곱셈뿐만 아니라 일반적인 군과 환에서의 곱셈에도 사용됩니다. f x * y와 같은 표현식을 사용하면, Lean은 f, x, y의 타입에 관한 정보를 이용하여 우리가 어떤 곱셈을 의도하는지 결정해야 합니다.

셋째, 구조가 다른 구조로부터 정의, 정리, 표기법을 다양한 방식으로 상속받을 수 있다는 사실을 다뤄야 합니다. 어떤 구조는 공리를 더 추가하여 다른 구조를 확장합니다. 가환환도 여전히 환이므로, 환에서 의미가 있는 정의는 모두 가환환에서도 의미가 있으며, 환에서 성립하는 정리는 모두 가환환에서도 성립합니다. 어떤 구조는 데이터를 더 추가하여 다른 구조를 확장합니다. 예를 들어, 임의의 환의 덧셈 부분은 덧셈군입니다. 환 구조는 곱셈과 항등식을 더하며, 이들을 규율하고 덧셈 부분과 연결하는 공리도 함께 더합니다. 때로는 한 구조를 다른 구조를 이용하여 정의할 수 있습니다. 모든 거리 공간에는 그와 연관된 표준적인 위상, 즉 거리 공간 위상이 있으며, 임의의 선형 순서에도 연관 지을 수 있는 다양한 위상이 있습니다.

마지막으로, 수학에서는 함수와 연산을 사용해 수를 정의하는 것과 똑같은 방식으로 함수와 연산을 사용해 구조를 정의할 수 있다는 점을 명심하는 것이 중요합니다. 군의 곱과 거듭제곱은 다시 군이 됩니다. 모든 \(n\)에 대해 \(n\)을 법으로 하는 정수는 환을 이루며, 모든 \(k > 0\)에 대해 그 환에 계수를 갖는 다항식들로 이루어진 \(k \times k\) 행렬은 다시 환을 이룹니다. 따라서 구조의 원소를 가지고 계산하는 것만큼이나 쉽게 구조 자체를 가지고도 계산할 수 있습니다. 이는 수학에서 대수적 구조가 대상들의 모임을 담는 그릇으로서, 그리고 그 자체로 하나의 대상으로서 이중의 삶을 산다는 뜻입니다. 증명 보조기는 이러한 이중 역할을 수용해야 합니다.

대수적 구조가 연관된 타입의 원소를 다룰 때, 증명 보조기는 그 구조를 인식하고 관련된 정의, 정리, 표기법을 찾아내야 합니다. 이 모든 것이 상당히 많은 작업처럼 들릴 텐데, 실제로도 그렇습니다. 하지만 Lean은 이러한 작업을 수행하기 위해 소수의 근본적인 메커니즘을 사용합니다. 이 절의 목표는 이러한 메커니즘을 설명하고 그 사용법을 보여 드리는 것입니다.

첫 번째 요소는 언급할 필요조차 없을 만큼 자명합니다. 형식적으로 말하면, 대수적 구조는 제 7.1 절에서 말한 의미의 구조입니다. 대수적 구조는 어떤 공리적 가설을 만족하는 데이터 묶음의 명세이며, 제 7.1 절에서 보았듯이 이는 바로 structure 명령이 담아내도록 설계된 것입니다. 그야말로 천생연분입니다!

데이터 타입 α가 주어지면, 다음과 같이 α 위의 군 구조를 정의할 수 있습니다.

structure Group₁ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  inv_mul_cancel : ∀ x : α, mul (inv x) x = one

타입 α가 Group₁의 정의에서 매개변수라는 점에 주목하십시오. 따라서 대상 struc : Group₁ α는 α 위의 군 구조라고 생각하면 됩니다. 제 2.2 절에서 보았듯이 inv_mul_cancel에 대응하는 mul_inv_cancel은 다른 군 공리로부터 따라 나오므로, 이를 정의에 추가할 필요는 없습니다.

이 군의 정의는 Mathlib에 있는 Group의 정의와 비슷하며, 우리 버전을 구별하기 위해 Group₁이라는 이름을 붙였습니다. #check Group을 작성하고 정의를 ctrl-클릭하면, Mathlib 버전의 Group이 다른 구조체를 확장하도록 정의되어 있음을 볼 수 있습니다. 이렇게 하는 방법은 나중에 설명하겠습니다. #print Group을 입력하면 Mathlib 버전의 Group에 여러 개의 추가 필드가 있다는 것도 볼 수 있습니다. 나중에 설명할 이유로, 구조에 중복된 정보를 추가하여 핵심 데이터로부터 정의할 수 있는 대상과 함수를 위한 추가 필드를 두는 것이 유용할 때가 있습니다. 지금은 이에 대해 걱정하지 않으셔도 됩니다. 우리가 단순화한 버전인 Group₁은 Mathlib이 사용하는 군의 정의와 본질적으로 같으니 안심하십시오.

타입을 구조체와 함께 묶는 것이 유용할 때도 있으며, Mathlib에는 다음과 동등한 Grp 구조체의 정의도 들어 있습니다.

structure Grp₁ where
  α : Type*
  str : Group₁ α

Mathlib 버전은 Mathlib.Algebra.Category.Grp.Basic에 있으며, 예제 파일 맨 앞의 import 목록에 이를 추가하면 #check로 확인할 수 있습니다.

아래에서 더 분명해질 이유로, 타입 α를 구조체 Group α와 분리해 두는 편이 더 자주 유용합니다. 이 표현은 구성 요소를 전부는 아니지만 대부분 하나의 구조로 결합하므로, 두 대상을 함께 부분적으로 묶인 구조라고 부릅니다. Mathlib에서는 어떤 타입이 군의 바탕 집합 타입으로 쓰일 때 G와 같은 로마자 대문자를 사용하는 것이 일반적입니다.

Group₁ 타입의 원소를 정의하여 군을 하나 구성해 봅시다. 임의의 두 타입 α와 β에 대해, Mathlib은 α와 β 사이의 동치(equivalence)들로 이루어진 타입 Equiv α β를 정의합니다. Mathlib은 이 타입을 위해 의미가 잘 드러나는 표기법 α ≃ β도 정의합니다. 원소 f : α ≃ β는 α와 β 사이의 전단사 함수이며, 네 가지 구성 요소로 표현됩니다. 곧 α에서 β로 가는 함수 f.toFun, β에서 α로 가는 역함수 f.invFun, 그리고 이 두 함수가 실제로 서로의 역함수임을 명시하는 두 성질입니다.

variable (α β γ : Type*)
variable (f : α ≃ β) (g : β ≃ γ)

#check Equiv α β
#check (f.toFun : α → β)
#check (f.invFun : β → α)
#check (f.right_inv : ∀ x : β, f (f.invFun x) = x)
#check (f.left_inv : ∀ x : α, f.invFun (f x) = x)
#check (Equiv.refl α : α ≃ α)
#check (f.symm : β ≃ α)
#check (f.trans g : α ≃ γ)

마지막 세 구성의 이름이 독창적으로 지어졌다는 점에 주목하십시오. 우리는 항등 함수 Equiv.refl, 역연산 Equiv.symm, 합성 연산 Equiv.trans를 전단사 대응 관계에 있다는 성질이 동치 관계임을 보여 주는 명시적 증거로 여깁니다.

또한 f.trans g에서는 정방향 함수들을 역순으로 합성해야 한다는 점에도 주목하십시오. Mathlib은 Equiv α β에서 함수 타입 α → β로의 강제 변환을 선언해 두었으므로, .toFun을 생략하고 Lean이 대신 삽입하게 할 수 있습니다.

example (x : α) : (f.trans g).toFun x = g.toFun (f.toFun x) :=
  rfl

example (x : α) : (f.trans g) x = g (f x) :=
  rfl

example : (f.trans g : α → γ) = g ∘ f :=
  rfl

Mathlib은 α와 자기 자신 사이의 동치들로 이루어진 타입 Perm α도 정의합니다.

example (α : Type*) : Equiv.Perm α = (α ≃ α) :=
  rfl

Equiv.Perm α가 동치의 합성에 대해 군을 이룬다는 것은 분명할 것입니다. mul f g가 g.trans f와 같아지도록 방향을 정하며, g.trans f의 순방향 함수는 f ∘ g입니다. 다시 말해, 곱셈은 우리가 보통 전단사 함수의 합성이라고 생각하는 것과 같습니다. 여기서 이 군을 정의합니다:

def permGroup {α : Type*} : Group₁ (Equiv.Perm α)
    where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc h g f).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

사실 Mathlib은 Algebra.Group.End 파일에서 Equiv.Perm α 위에 정확히 이 Group 구조를 정의합니다. 언제나처럼 permGroup의 정의에 사용된 정리들 위에 마우스를 올리면 그 명제를 확인할 수 있으며, 원본 파일에 있는 해당 정의로 이동하여 그것들이 어떻게 구현되어 있는지 더 자세히 알아볼 수 있습니다.

일반적인 수학에서는 보통 표기법이 구조와 무관하다고 생각합니다. 예를 들어, 군 \((G_1, \cdot, 1, \cdot^{-1})\), \((G_2, \circ, e, i(\cdot))\), \((G_3, +, 0, -)\)를 생각해 볼 수 있습니다. 첫 번째 경우에는 이항 연산을 \(\cdot\)으로, 항등식을 \(1\)로, 역함수를 \(x \mapsto x^{-1}\)로 씁니다. 두 번째와 세 번째 경우에는 제시된 다른 표기법을 사용합니다. 그러나 Lean에서 군의 개념을 형식화하면 표기법이 구조와 더 긴밀하게 연결됩니다. Lean에서 모든 Group의 구성 요소는 mul, one, inv라는 이름을 가지며, 곱셈 표기법이 이들을 가리키도록 어떻게 설정되는지 곧 살펴보겠습니다. 덧셈 표기법을 사용하려면 대신 동형인 구조 AddGroup (덧셈군의 바탕이 되는 구조)을 사용합니다. 이 구조의 구성 요소는 add, zero, neg라는 이름을 가지며, 관련 표기법은 예상하시는 그대로입니다.

제 7.1 절에서 정의한 Point 타입과 그곳에서 정의한 덧셈 함수를 떠올려 보십시오. 이 정의들은 이 절에 딸린 예제 파일에 다시 수록되어 있습니다. 연습 문제로, 위에서 정의한 Group₁ 구조와 비슷하되 방금 설명한 덧셈식 이름 체계를 사용하는 AddGroup₁ 구조를 정의하십시오. Point 데이터 타입에 부호 반전과 영원소를 정의하고, Point 위에 AddGroup₁ 구조를 정의하십시오.

structure AddGroup₁ (α : Type*) where
  (add : α → α → α)
  -- fill in the rest
@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def neg (a : Point) : Point := sorry

def zero : Point := sorry

def addGroupPoint : AddGroup₁ Point := sorry

end Point

진전이 있습니다. 이제 우리는 Lean에서 대수적 구조를 정의하는 방법을 알고, 그 구조의 인스턴스를 정의하는 방법도 압니다. 하지만 구조에 표기법을 연결하여 각 인스턴스에서도 그 표기법을 사용할 수 있게 하고 싶습니다. 더 나아가 어떤 구조에 연산을 정의하면 임의의 특정 인스턴스에서 그 연산을 사용할 수 있도록 하고, 어떤 구조에 관한 정리를 증명하면 임의의 인스턴스에서 그 정리를 사용할 수 있도록 하고 싶습니다.

실제로 Mathlib에는 Equiv.Perm α에 대해 일반적인 군 표기법, 정의, 정리를 사용할 수 있도록 이미 설정되어 있습니다.

variable {α : Type*} (f g : Equiv.Perm α) (n : ℕ)

#check f * g
#check mul_assoc f g g⁻¹

-- group power, defined for any group
#check g ^ n

example : f * g * g⁻¹ = f := by rw [mul_assoc, mul_inv_cancel, mul_one]

example : f * g * g⁻¹ = f :=
  mul_inv_cancel_right f g

example {α : Type*} (f g : Equiv.Perm α) : g.symm.trans (g.trans f) = f :=
  mul_inv_cancel_right f g

위에서 정의해 보라고 했던 Point 위의 덧셈군 구조에서는 그렇지 않다는 것을 확인할 수 있습니다. 이제 우리가 할 일은 Equiv.Perm α에 대한 예제들이 그렇게 동작하도록 내부에서 일어나는 마법을 이해하는 것입니다.

문제는 Lean이 우리가 입력한 표현식에 담긴 정보를 사용하여 관련 표기법과 암묵적인 군 구조를 찾을 수 있어야 한다는 점입니다. 마찬가지로 ℝ 타입을 가진 표현식 x와 y로 x + y를 쓰면, Lean은 + 기호를 실수에서의 해당 덧셈 함수로 해석해야 합니다. 또한 Lean은 ℝ 타입을 가환환의 인스턴스로 인식해야 하며, 그래야 가환환에 관한 모든 정의와 정리를 사용할 수 있습니다. 다른 예로, Lean에서 연속성은 임의의 두 위상 공간에 대해 정의됩니다. f : ℝ → ℂ가 있을 때 Continuous f라고 쓰면, Lean은 ℝ과 ℂ에서 해당하는 위상을 찾아야 합니다.

이 마법은 세 가지 요소를 결합하여 이루어집니다.

  1. 논리. 임의의 군에서 해석되어야 하는 정의는 군의 타입과 군 구조를 인자로 받습니다. 마찬가지로, 임의의 군의 원소에 관한 정리는 군의 타입과 군 구조에 대한 전칭 한정기호로 시작합니다.

  2. 암시적 인자. 타입과 구조에 대한 인자는 일반적으로 암시적으로 남겨 두므로, 우리는 이를 직접 작성하거나 Lean 정보 창에서 볼 필요가 없습니다. Lean이 우리 대신 이 정보를 조용히 채워 넣습니다.

  3. 타입 클래스 추론. 클래스 추론이라고도 하는 이것은 Lean이 나중에 사용할 정보를 등록할 수 있게 해 주는 단순하지만 강력한 메커니즘입니다. Lean은 정의, 정리 또는 표기법의 암시적 인자를 채워야 할 때 등록된 정보를 활용할 수 있습니다.

표기 (grp : Group G)는 해당 인자가 명시적으로 주어질 것을 예상하라고 Lean에 알려 주고, 표기 {grp : Group G}는 표현식의 문맥상 단서로부터 그 인자를 알아내도록 시도하라고 Lean에 알려 주는 반면, 표기 [grp : Group G]는 해당 인자를 타입 클래스 추론을 사용하여 합성해야 한다고 Lean에 알려 줍니다. 이러한 인자를 사용하는 요점은 일반적으로 이를 명시적으로 참조할 필요가 없다는 데 있으므로, Lean에서는 [Group G]라고 작성하여 이름을 익명으로 남겨 둘 수 있습니다. Lean이 _inst_1과 같은 이름을 자동으로 선택한다는 것을 아마 이미 눈치채셨을 것입니다. variable 명령과 함께 익명의 대괄호 표기를 사용하면, 변수가 아직 유효 범위 안에 있는 동안에는 Lean이 G를 언급하는 모든 정의나 정리에 인자 [Group G]를 자동으로 추가합니다.

Lean이 탐색을 수행하는 데 필요한 정보는 어떻게 등록합니까? 앞의 군 예제로 돌아가면, 두 가지만 바꾸면 됩니다. 첫째, 군 구조를 정의할 때 structure 명령을 사용하는 대신 class 키워드를 사용하여 그것이 클래스 추론의 후보임을 나타냅니다. 둘째, 특정 인스턴스를 def로 정의하는 대신 instance 키워드를 사용하여 해당 인스턴스를 Lean에 등록합니다. 클래스 변수의 이름과 마찬가지로 인스턴스 정의의 이름도 익명으로 둘 수 있습니다. 일반적으로 우리는 Lean이 세부 사항으로 우리를 번거롭게 하지 않고 그것을 찾아서 사용하기를 의도하기 때문입니다.

class Group₂ (α : Type*) where
  mul : α → α → α
  one : α
  inv : α → α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ x : α, mul x one = x
  one_mul : ∀ x : α, mul one x = x
  inv_mul_cancel : ∀ x : α, mul (inv x) x = one

instance {α : Type*} : Group₂ (Equiv.Perm α) where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc h g f).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

다음은 그 사용법을 보여 줍니다.

#check Group₂.mul

def mySquare {α : Type*} [Group₂ α] (x : α) :=
  Group₂.mul x x

#check mySquare

section
variable {β : Type*} (f g : Equiv.Perm β)

example : Group₂.mul f g = g.trans f :=
  rfl

example : mySquare f = f.trans f :=
  rfl

end

#check 명령을 실행하면 Group₂.mul에 클래스 추론으로 찾아질 것으로 기대되는 암시적 인자 [Group₂ α]가 있음을 알 수 있습니다. 여기서 α는 Group₂.mul에 전달되는 인자의 타입입니다. 다시 말해, {α : Type*}는 군 원소의 타입에 대한 암시적 인자이고 [Group₂ α]는 α 위의 군 구조에 대한 암시적 인자입니다. 마찬가지로, Group₂에 대한 일반적인 제곱 함수 my_square를 정의할 때 원소의 타입에는 암시적 인자 {α : Type*}를, Group₂ 구조에는 암시적 인자 [Group₂ α]를 사용합니다.

첫 번째 예제에서 Group₂.mul f g라고 쓰면, f와 g의 타입은 Group₂.mul의 인수 α가 Equiv.Perm β로 인스턴스화되어야 한다는 것을 Lean에게 알려 줍니다. 이는 Lean이 Group₂ (Equiv.Perm β)의 원소를 찾아야 한다는 뜻입니다. 앞의 instance 선언은 그 방법을 Lean에게 정확히 알려 줍니다. 문제가 해결되었습니다!

Lean이 필요할 때 찾을 수 있도록 정보를 등록해 두는 이 단순한 메커니즘은 놀라울 만큼 유용합니다. 이 메커니즘이 쓰이는 한 가지 예를 살펴보겠습니다. Lean의 기초 체계에서 데이터 타입 α는 비어 있을 수 있습니다. 그러나 여러 응용에서는 어떤 타입이 적어도 하나의 원소를 가진다는 사실을 아는 것이 유용합니다. 예를 들어, 리스트의 첫 번째 원소를 반환하는 함수 List.headI는 리스트가 비어 있을 때 기본값을 반환할 수 있습니다. 이것이 가능하도록 Lean 라이브러리는 기본값을 저장하는 일만 하는 클래스 Inhabited α를 정의합니다. Point 타입이 그 인스턴스임을 다음과 같이 보일 수 있습니다:

instance : Inhabited Point where default := ⟨0, 0, 0⟩

#check (default : Point)

example : ([] : List Point).headI = default :=
  rfl

클래스 추론 메커니즘은 범용 표기법에도 사용됩니다. 표현식 x + y는 Add.add x y의 약어이며, 여기서—짐작하셨겠지만—Add α는 α 위의 이항 함수를 저장하는 클래스입니다. x + y라고 쓰면 Lean은 [Add.add α]의 등록된 인스턴스를 찾아 해당 함수를 사용합니다. 아래에서는 Point에 대한 덧셈 함수를 등록합니다.

instance : Add Point where add := Point.add

section
variable (x y : Point)

#check x + y

example : x + y = Point.add x y :=
  rfl

end

이런 방식으로 다른 타입의 이항 연산에도 + 표기법을 부여할 수 있습니다.

하지만 이보다 더 나은 방법도 있습니다. 앞에서 *는 모든 군에서, +는 모든 덧셈군에서 사용할 수 있고, 둘 다 모든 환에서 사용할 수 있음을 보았습니다. Lean에서 환의 새 인스턴스를 정의할 때는 그 인스턴스에 대해 +와 *를 정의할 필요가 없습니다. Lean은 이것들이 모든 환에 대해 정의되어 있음을 알고 있기 때문입니다. 이 방법을 사용하여 우리의 Group₂ 클래스에 대한 표기법을 지정할 수 있습니다:

instance {α : Type*} [Group₂ α] : Mul α :=
  ⟨Group₂.mul⟩

instance {α : Type*} [Group₂ α] : One α :=
  ⟨Group₂.one⟩

instance {α : Type*} [Group₂ α] : Inv α :=
  ⟨Group₂.inv⟩

section
variable {α : Type*} (f g : Equiv.Perm α)

#check f * 1 * g⁻¹

def foo : f * 1 * g⁻¹ = g.symm.trans ((Equiv.refl α).trans f) :=
  rfl

end

이 접근 방식이 작동하는 이유는 Lean이 재귀적 탐색을 수행하기 때문입니다. 우리가 선언한 인스턴스들에 따라 Lean은 Group₂ (Equiv.Perm α)의 인스턴스를 찾음으로써 Mul (Equiv.Perm α)의 인스턴스를 찾을 수 있으며, Group₂ (Equiv.Perm α)의 인스턴스는 우리가 제공했으므로 찾을 수 있습니다. Lean은 이 두 사실을 찾아내어 서로 연결할 수 있습니다.

방금 든 예제는 위험합니다. Lean 라이브러리에도 Group (Equiv.Perm α)의 인스턴스가 있고, 곱셈은 모든 군에서 정의되기 때문입니다. 따라서 어느 인스턴스가 선택될지 모호합니다. 실제로 Lean은 다른 우선순위를 명시적으로 지정하지 않는 한 더 최근의 선언을 우선합니다. 또한 extends 키워드를 사용하여 한 구조체가 다른 구조체의 인스턴스임을 Lean에 알리는 방법도 있습니다. 예를 들어 Mathlib은 이 방법으로 모든 가환환이 환임을 명시합니다. 더 자세한 내용은 제 8 절와 Theorem Proving in Lean의 클래스 추론에 관한 절에서 찾을 수 있습니다.

일반적으로, 이미 표기가 정의되어 있는 대수적 구조의 인스턴스에 대해 *의 값을 지정하는 것은 좋지 않은 생각입니다. Lean에서 Group의 개념을 재정의하는 것은 인위적인 예제입니다. 하지만 이 경우에는 군 표기법의 두 해석 모두 똑같은 방식으로 Equiv.trans, Equiv.refl, Equiv.symm으로 펼쳐집니다.

비슷하게 인위적인 연습 문제로, Group₂와 유사하게 AddGroup₂ 클래스를 정의하십시오. Add, Neg, Zero 클래스를 사용하여 임의의 AddGroup₂에서 쓸 덧셈, 부호 반전, 영에 대한 통상적인 표기법을 정의하십시오. 그런 다음 Point가 AddGroup₂의 인스턴스임을 보이십시오. 직접 시험해 보고 Point의 원소에 대해 덧셈군 표기법이 작동하는지 확인하십시오.

class AddGroup₂ (α : Type*) where
  add : α → α → α
  -- fill in the rest

위에서 이미 Point에 대해 Add, Neg, Zero 인스턴스를 선언했다는 점은 큰 문제가 되지 않습니다. 이번에도 표기법을 합성하는 두 가지 방법은 같은 결과를 내야 합니다.

클래스 추론은 미묘하므로 사용할 때 주의해야 합니다. 클래스 추론은 우리가 입력하는 표현식의 해석을 보이지 않게 좌우하는 자동화를 설정하기 때문입니다. 그러나 현명하게 사용하면 클래스 추론은 강력한 도구입니다. Lean에서 대수적 추론을 가능하게 하는 것이 바로 클래스 추론입니다.

7.3. 가우스 정수 만들기

이제 중요한 수학적 대상인 가우스 정수를 만들고 이것이 유클리드 정역임을 보이면서 Lean에서 대수적 계층 구조를 어떻게 사용하는지 설명하겠습니다. 다시 말해, 지금까지 사용해 온 용어로 표현하면, 가우스 정수를 정의하고 이것이 유클리드 정역 구조의 인스턴스임을 보이겠습니다.

일반적인 수학 용어로 말하면, 가우스 정수의 집합 \(\Bbb{Z}[i]\)는 복소수의 집합 \(\{ a + b i \mid a, b \in \Bbb{Z}\}\)입니다. 하지만 여기서 우리의 목표는 이를 복소수의 부분집합으로 정의하는 것이 아니라 그 자체로 독립적인 데이터 타입으로 정의하는 것입니다. 이를 위해 가우스 정수를 정수의 쌍으로 표현하며, 두 정수를 각각 실수부와 허수부로 생각합니다.

@[ext]
structure GaussInt where
  re : ℤ
  im : ℤ

먼저 0을 ⟨0, 0⟩으로, 1을 ⟨1, 0⟩으로 정의하고 덧셈을 성분별로 정의하여 가우스 정수가 환의 구조를 가짐을 보이겠습니다. 곱셈의 정의를 구하려면 ⟨0, 1⟩로 표현되는 원소 \(i\)가 \(-1\)의 제곱근이 되어야 한다는 점을 기억하십시오. 따라서 다음이 성립해야 합니다.

\[\begin{split}(a + bi) (c + di) & = ac + bci + adi + bd i^2 \\ & = (ac - bd) + (bc + ad)i.\end{split}\]

이것으로 아래 Mul의 정의가 설명됩니다.

instance : Zero GaussInt :=
  ⟨⟨0, 0⟩⟩

instance : One GaussInt :=
  ⟨⟨1, 0⟩⟩

instance : Add GaussInt :=
  ⟨fun x y ↦ ⟨x.re + y.re, x.im + y.im⟩⟩

instance : Neg GaussInt :=
  ⟨fun x ↦ ⟨-x.re, -x.im⟩⟩

instance : Mul GaussInt :=
  ⟨fun x y ↦ ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩

제 7.1 절에서 언급했듯이, 어떤 데이터 타입과 관련된 모든 정의는 그 타입과 같은 이름의 네임스페이스에 넣는 것이 좋습니다. 따라서 이 장과 관련된 Lean 파일에서는 이 정의들을 GaussInt 네임스페이스 안에서 작성합니다.

여기서는 표기 0, 1, +, -, *에 GaussInt.zero 같은 이름을 붙이고 그 이름에 표기를 할당하는 대신, 각 표기의 해석을 직접 정의하고 있다는 점에 주목하십시오. 정의에 명시적인 이름이 있으면 유용한 경우가 많습니다. 예를 들어 simp나 rw와 함께 사용할 때 그렇습니다.

theorem zero_def : (0 : GaussInt) = ⟨0, 0⟩ :=
  rfl

theorem one_def : (1 : GaussInt) = ⟨1, 0⟩ :=
  rfl

theorem add_def (x y : GaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ :=
  rfl

theorem neg_def (x : GaussInt) : -x = ⟨-x.re, -x.im⟩ :=
  rfl

theorem mul_def (x y : GaussInt) :
    x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ :=
  rfl

실수부와 허수부를 계산하는 규칙에 이름을 붙이고 이를 단순화기(simplifier)에 등록해 두는 것도 유용합니다.

@[simp]
theorem zero_re : (0 : GaussInt).re = 0 :=
  rfl

@[simp]
theorem zero_im : (0 : GaussInt).im = 0 :=
  rfl

@[simp]
theorem one_re : (1 : GaussInt).re = 1 :=
  rfl

@[simp]
theorem one_im : (1 : GaussInt).im = 0 :=
  rfl

@[simp]
theorem add_re (x y : GaussInt) : (x + y).re = x.re + y.re :=
  rfl

@[simp]
theorem add_im (x y : GaussInt) : (x + y).im = x.im + y.im :=
  rfl

@[simp]
theorem neg_re (x : GaussInt) : (-x).re = -x.re :=
  rfl

@[simp]
theorem neg_im (x : GaussInt) : (-x).im = -x.im :=
  rfl

@[simp]
theorem mul_re (x y : GaussInt) : (x * y).re = x.re * y.re - x.im * y.im :=
  rfl

@[simp]
theorem mul_im (x y : GaussInt) : (x * y).im = x.re * y.im + x.im * y.re :=
  rfl

이제 가우스 정수가 가환환의 인스턴스임을 보이는 일은 놀라울 만큼 쉽습니다. 구조체 개념을 유용하게 활용하고 있는 것입니다. 각각의 가우스 정수는 GaussInt 구조체의 인스턴스인 반면, GaussInt 타입 자체는 관련 연산과 함께 CommRing 구조체의 인스턴스입니다. CommRing 구조체는 다시 표기 구조체인 Zero, One, Add, Neg, Mul을 확장합니다.

instance : CommRing GaussInt := _를 입력하고 VS Code에 나타나는 전구 아이콘을 클릭한 다음 Lean에게 구조체 정의의 뼈대를 채워 달라고 요청하면, 겁이 날 만큼 많은 항목이 나타납니다. 하지만 구조체의 정의로 이동해 보면, 많은 필드에 Lean이 자동으로 채워 주는 기본 정의가 있다는 것을 알 수 있습니다. 반드시 필요한 필드는 아래 정의에 나와 있습니다. nsmul과 zsmul은 특별한 경우로, 지금은 무시해도 되며 다음 장에서 설명합니다. 각 경우에 해당 항등식은 정의를 펼치고, ext 택틱을 사용하여 항등식을 실수부와 허수부 성분으로 환원하고, 단순화한 뒤, 필요하면 정수에서 해당 환 계산을 수행하여 증명합니다. 이 코드를 모두 반복하는 것은 쉽게 피할 수 있지만, 그것은 지금 논의할 주제가 아니라는 점에 유의하십시오.

instance instCommRing : CommRing GaussInt where
  zero := 0
  one := 1
  add := (· + ·)
  neg x := -x
  mul := (· * ·)
  nsmul := nsmulRec
  zsmul := zsmulRec
  add_assoc := by
    intros
    ext <;> simp <;> ring
  zero_add := by
    intro
    ext <;> simp
  add_zero := by
    intro
    ext <;> simp
  neg_add_cancel := by
    intro
    ext <;> simp
  add_comm := by
    intros
    ext <;> simp <;> ring
  mul_assoc := by
    intros
    ext <;> simp <;> ring
  one_mul := by
    intro
    ext <;> simp
  mul_one := by
    intro
    ext <;> simp
  left_distrib := by
    intros
    ext <;> simp <;> ring
  right_distrib := by
    intros
    ext <;> simp <;> ring
  mul_comm := by
    intros
    ext <;> simp <;> ring
  zero_mul := by
    intros
    ext <;> simp
  mul_zero := by
    intros
    ext <;> simp

Lean 라이브러리는 자명하지 않은 타입의 클래스를 서로 다른 원소를 적어도 두 개 가진 타입으로 정의합니다. 환의 문맥에서 이것은 0이 1과 같지 않다고 말하는 것과 동치입니다. 몇몇 일반적인 정리가 이 사실에 의존하므로, 지금 이를 증명해 두는 편이 좋겠습니다.

instance : Nontrivial GaussInt := by
  use 0, 1
  rw [Ne, GaussInt.ext_iff]
  simp

이제 가우스 정수가 중요한 성질을 하나 더 가진다는 것을 보이겠습니다. 유클리드 정역이란 다음 두 성질을 만족하는 노름 함수 \(N : R \to \mathbb{N}\)을 갖춘 환 \(R\)을 말합니다:

  • \(R\)의 모든 \(a\)와 \(b \ne 0\)에 대해, \(a = bq + r\)이고 \(r = 0\)이거나 \(N(r) < N(b)\)인 \(q\)와 \(r\)이 \(R\)에 존재합니다.

  • 모든 \(a\)와 \(b \ne 0\)에 대해 \(N(a) \le N(ab)\)입니다.

\(N(a) = |a|\)를 갖춘 정수환 \(\Bbb{Z}\)는 유클리드 정역의 전형적인 예입니다. 이 경우 \(q\)는 \(a\)를 \(b\)로 나눈 정수 나눗셈의 결과로, \(r\)은 그 나머지로 잡을 수 있습니다. a와 b가 정수일 때 Lean에서 a / b는 정수 나눗셈을, a % b는 나머지를 나타낸다는 점에 유의하십시오. 이들은 다음을 만족하도록 정의되어 있습니다:

example (a b : ℤ) : a = b * (a / b) + a % b :=
  Eq.symm (Int.mul_ediv_add_emod a b)

example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b :=
  Int.emod_nonneg a

example (a b : ℤ) : b ≠ 0 → a % b < |b| :=
  Int.emod_lt_abs a

임의의 환에서 원소 \(a\)가 \(1\)을 나누면 이를 단위원이라고 합니다. 0이 아닌 원소 \(a\)를 \(b\)와 \(c\) 모두 단위원이 아닌 \(a = bc\) 꼴로 쓸 수 없으면 이를 기약원이라고 합니다. 정수에서는 모든 기약 원소 \(a\)가 소원입니다. 즉, \(a\)가 곱 \(bc\)를 나눌 때마다 \(b\)와 \(c\) 중 하나를 나눕니다. 그러나 다른 환에서는 이 성질이 성립하지 않을 수 있습니다. 환 \(\Bbb{Z}[\sqrt{-5}]\)에서는 다음이 성립합니다.

\[6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),\]

그리고 원소 \(2\), \(3\), \(1 + \sqrt{-5}\), \(1 - \sqrt{-5}\)는 모두 기약원이지만 소원은 아닙니다. 예를 들어, \(2\)는 곱 \((1 + \sqrt{-5})(1 - \sqrt{-5})\)를 나누지만, 두 인수 중 어느 것도 나누지 않습니다. 특히 더 이상 유일 인수분해가 성립하지 않습니다. 수 \(6\)은 두 가지 이상의 방법으로 기약 원소들로 인수분해될 수 있습니다.

반면에 모든 유클리드 정역은 유일 인수분해 정역이며, 이는 모든 기약 원소가 소원임을 함의합니다. 유클리드 정역의 공리들은 0이 아닌 임의의 원소를 기약 원소들의 유한한 곱으로 쓸 수 있음을 함의합니다. 또한 이 공리들로부터 유클리드 알고리즘을 사용하여 0이 아닌 임의의 두 원소 a와 b의 최대공약수, 즉 다른 모든 공약수로 나누어떨어지는 원소를 찾을 수 있음이 따라 나옵니다. 이는 다시 기약 원소로의 인수분해가 단원의 곱셈을 제외하면 유일하다는 것을 함의합니다.

이제 가우스 정수가 노름 \(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\)에 대해 유클리드 정역임을 보이겠습니다. 가우스 정수 \(a - bi\)를 \(a + bi\)의 켤레라고 합니다. 임의의 복소수 \(x\)와 \(y\)에 대해 \(N(xy) = N(x)N(y)\)가 성립함은 어렵지 않게 확인할 수 있습니다.

이 노름의 정의가 가우스 정수를 유클리드 정역으로 만든다는 것을 확인할 때 까다로운 것은 첫 번째 성질뿐입니다. 적당한 \(q\)와 \(r\)에 대해 \(a + bi = (c + di) q + r\)로 쓰고 싶다고 합시다. \(a + bi\)와 \(c + di\)를 복소수로 보고 다음 나눗셈을 수행하십시오.

\[\frac{a + bi}{c + di} = \frac{(a + bi)(c - di)}{(c + di)(c-di)} = \frac{ac + bd}{c^2 + d^2} + \frac{bc -ad}{c^2+d^2} i.\]

실수부와 허수부는 정수가 아닐 수도 있지만, 이를 가장 가까운 정수 \(u\)와 \(v\)로 반올림할 수 있습니다. 그러면 우변을 \((u + vi) + (u' + v'i)\)로 나타낼 수 있으며, 여기서 \(u' + v'i\)는 남은 부분입니다. \(|u'| \le 1/2\)이고 \(|v'| \le 1/2\)임에 유의하십시오. 따라서 다음이 성립합니다.

\[N(u' + v' i) = (u')^2 + (v')^2 \le 1/4 + 1/4 \le 1/2.\]

양변에 \(c + di\)를 곱하면 다음을 얻습니다.

\[a + bi = (c + di) (u + vi) + (c + di) (u' + v'i).\]

\(q = u + vi\)와 \(r = (c + di) (u' + v'i)\)로 두면 \(a + bi = (c + di) q + r\)이 성립하므로, \(N(r)\)의 상계만 구하면 됩니다.

\[N(r) = N(c + di)N(u' + v'i) \le N(c + di) \cdot 1/2 < N(c + di).\]

방금 수행한 논증에서는 가우스 정수를 복소수의 부분집합으로 보아야 합니다. 따라서 이를 Lean에서 형식화하는 한 가지 방법은 가우스 정수를 복소수에 매장하고, 정수를 가우스 정수에 매장하고, 실수에서 정수로 가는 반올림 함수를 정의한 뒤, 이 수 체계들 사이를 적절히 오가도록 세심하게 주의를 기울이는 것입니다. 실제로 이것이 바로 Mathlib에서 따르는 접근 방식이며, Mathlib에서는 가우스 정수 자체가 이차 정수환의 특수한 경우로 구성됩니다. GaussianInt.lean 파일을 참고하십시오.

여기서는 그 대신 정수 안에서 이루어지는 논증을 전개하겠습니다. 이는 수학을 형식화할 때 흔히 마주치는 선택을 보여 줍니다. 라이브러리에 아직 없는 개념이나 도구가 필요한 논증이 주어지면 두 가지 선택지가 있습니다. 필요한 개념과 도구를 형식화하거나, 이미 가지고 있는 개념과 도구를 활용하도록 논증을 수정하는 것입니다. 그 결과를 다른 문맥에서도 사용할 수 있다면 첫 번째 선택은 일반적으로 시간을 잘 투자하는 것입니다. 그러나 실용적으로 말하자면, 때로는 더 초등적인 증명을 찾는 편이 더 효율적입니다.

정수에 대한 일반적인 몫-나머지 정리에 따르면, 모든 \(a\)와 0이 아닌 \(b\)에 대해 \(a = b q + r\)이고 \(0 \le r < |b|\)를 만족하는 \(q\)와 \(r\)이 존재합니다. 여기서는 다음과 같은 변형을 사용하겠습니다. 이 변형에 따르면 \(a = b q' + r'\)이고 \(|r'| \le |b|/2\)를 만족하는 \(q'\)와 \(r'\)이 존재합니다. 첫 번째 명제에서 \(r\)의 값이 \(r \le |b|/2\)를 만족하면 \(q' = q\)와 \(r' = r\)로 잡을 수 있고, 그렇지 않으면 \(q' = q + 1\)과 \(r' = r - b\)로 잡을 수 있음을 확인할 수 있습니다(\(b\)가 양수인 경우이며, 그렇지 않은 경우에도 필요한 부분만 바꾸면 마찬가지입니다). 경우에 따른 정의를 피하는 다음의 더 우아한 접근법을 제안해 준 Heather Macbeth에게 감사드립니다. 나누기 전에 a에 b / 2를 더하고, 그런 다음 나머지에서 그 값을 빼기만 하면 됩니다.

def div' (a b : ℤ) :=
  (a + b / 2) / b

def mod' (a b : ℤ) :=
  (a + b / 2) % b - b / 2

theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a := by
  rw [div', mod']
  linarith [Int.mul_ediv_add_emod (a + b / 2) b]

theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by
  rw [mod', abs_le]
  constructor
  · linarith [Int.emod_nonneg (a + b / 2) h.ne']
  have := Int.emod_lt_of_pos (a + b / 2) h
  have := Int.mul_ediv_add_emod b 2
  have := Int.emod_lt_of_pos b zero_lt_two
  linarith

우리의 오랜 친구인 linarith를 사용한다는 점에 주목하십시오. 또한 mod'를 div'로 표현해야 합니다.

theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b := by linarith [div'_add_mod' a b]

\(x^2 + y^2\)이 0일 필요충분조건은 \(x\)와 \(y\)가 모두 0인 것이라는 사실을 사용하겠습니다. 연습 문제로, 이것이 임의의 순서환에서 성립함을 증명해 보십시오.

theorem sq_add_sq_eq_zero {α : Type*} [Ring α] [LinearOrder α] [IsStrictOrderedRing α]
    (x y : α) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
  sorry

이 절의 나머지 정의와 정리는 모두 GaussInt 네임스페이스 안에 두겠습니다. 먼저 norm 함수를 정의하고, 그 성질 몇 가지를 여러분이 직접 증명해 보시기 바랍니다. 증명은 모두 짧습니다.

def norm (x : GaussInt) :=
  x.re ^ 2 + x.im ^ 2

@[simp]
theorem norm_nonneg (x : GaussInt) : 0 ≤ norm x := by
  sorry
theorem norm_eq_zero (x : GaussInt) : norm x = 0 ↔ x = 0 := by
  sorry
theorem norm_pos (x : GaussInt) : 0 < norm x ↔ x ≠ 0 := by
  sorry
theorem norm_mul (x y : GaussInt) : norm (x * y) = norm x * norm y := by
  sorry

다음으로 켤레 함수를 정의합니다:

def conj (x : GaussInt) : GaussInt :=
  ⟨x.re, -x.im⟩

@[simp]
theorem conj_re (x : GaussInt) : (conj x).re = x.re :=
  rfl

@[simp]
theorem conj_im (x : GaussInt) : (conj x).im = -x.im :=
  rfl

theorem norm_conj (x : GaussInt) : norm (conj x) = norm x := by simp [norm]

마지막으로, 가우스 정수의 나눗셈을 x / y 표기로 정의합니다. 이 나눗셈은 복소수 몫을 가장 가까운 가우스 정수로 반올림합니다. 이를 위해 직접 만든 Int.div' 함수를 사용합니다. 위에서 계산한 것처럼 x가 \(a + bi\)이고 y가 \(c + di\)이면, x / y의 실수부와 허수부는 다음 값에 가장 가까운 정수입니다.

\[\frac{ac + bd}{c^2 + d^2} \quad \text{and} \quad \frac{bc -ad}{c^2+d^2},\]

각각 가장 가까운 정수입니다. 여기서 분자는 \((a + bi) (c - di)\)의 실수부와 허수부이고, 분모는 둘 다 \(c + di\)의 노름과 같습니다.

instance : Div GaussInt :=
  ⟨fun x y ↦ ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩⟩

x / y를 정의했으므로, 이제 x % y를 나머지, 즉 x - (x / y) * y로 정의합니다. 앞에서와 마찬가지로, 이 정의들을 simp과 rw에서 사용할 수 있도록 정리 div_def와 mod_def에 기록해 둡니다.

instance : Mod GaussInt :=
  ⟨fun x y ↦ x - y * (x / y)⟩

theorem div_def (x y : GaussInt) :
    x / y = ⟨Int.div' (x * conj y).re (norm y), Int.div' (x * conj y).im (norm y)⟩ :=
  rfl

theorem mod_def (x y : GaussInt) : x % y = x - y * (x / y) :=
  rfl

이 정의들로부터 모든 x와 y에 대해 x = y * (x / y) + x % y가 바로 나오므로, y가 0이 아닐 때 x % y의 노름이 y의 노름보다 작다는 것만 보이면 됩니다.

방금 x / y의 실수부와 허수부를 각각 div' (x * conj y).re (norm y)와 div' (x * conj y).im (norm y)로 정의했습니다. 계산하면 다음을 얻습니다.

(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x / y * (y * conj y)

우변의 실수부와 허수부는 정확히 mod' (x * conj y).re (norm y)와 mod' (x * conj y).im (norm y)입니다. div'와 mod'의 성질에 의해, 이 값들은 norm y / 2 이하임이 보장됩니다. 따라서 다음을 얻습니다.

norm ((x % y) * conj y) ≤ (norm y / 2)^2 + (norm y / 2)^2 ≤ (norm y / 2) * norm y.

한편, 다음이 성립합니다.

norm ((x % y) * conj y) = norm (x % y) * norm (conj y) = norm (x % y) * norm y.

norm y로 양변을 나누면 norm (x % y) ≤ (norm y) / 2 < norm y를 얻으며, 이것이 바로 원하던 결과입니다.

이 번거로운 계산은 다음 증명에서 수행됩니다. 세부 사항을 단계별로 따라가 보고, 더 깔끔한 논증을 찾을 수 있는지 시도해 보시기 바랍니다.

theorem norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    (x % y).norm < y.norm := by
  have norm_y_pos : 0 < norm y := by rwa [norm_pos]
  have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
  · ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
  have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
  · calc
      norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
      _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
          + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
      _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
      _ = norm y / 2 * (norm y / 2 * 2) := by ring
      _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
  calc norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right H2 norm_y_pos
    _ < norm y := by
        apply Int.ediv_lt_of_lt_mul
        · norm_num
        · linarith

이제 거의 다 왔습니다. 우리의 norm 함수는 가우스 정수를 음이 아닌 정수로 보냅니다. 가우스 정수를 자연수로 보내는 함수가 필요하며, 이는 norm과 정수를 자연수로 보내는 함수 Int.natAbs를 합성하여 얻습니다. 다음 두 보조정리 중 첫 번째는 노름을 자연수로 보냈다가 다시 정수로 되돌려도 값이 바뀌지 않는다는 것을 보입니다. 두 번째 보조정리는 노름이 감소한다는 사실을 다시 표현합니다.

theorem coe_natAbs_norm (x : GaussInt) : (x.norm.natAbs : ℤ) = x.norm :=
  Int.natAbs_of_nonneg (norm_nonneg _)

theorem natAbs_norm_mod_lt (x y : GaussInt) (hy : y ≠ 0) :
    (x % y).norm.natAbs < y.norm.natAbs := by
  apply Int.ofNat_lt.1
  simp only [Int.natCast_natAbs, abs_of_nonneg, norm_nonneg]
  exact norm_mod_lt x hy

또한 유클리드 정역에서 노름 함수가 갖는 두 번째 핵심 성질도 증명해야 합니다.

theorem not_norm_mul_left_lt_norm (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
    ¬(norm (x * y)).natAbs < (norm x).natAbs := by
  apply not_lt_of_ge
  rw [norm_mul, Int.natAbs_mul]
  apply le_mul_of_one_le_right (Nat.zero_le _)
  apply Int.ofNat_le.1
  rw [coe_natAbs_norm]
  exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)

이제 이를 종합하여 가우스 정수가 유클리드 정역의 인스턴스임을 보일 수 있습니다. 앞서 정의한 몫 함수와 나머지 함수를 사용합니다. Mathlib의 유클리드 정역 정의는 임의의 정초 측도(well-founded measure)에 대해 나머지가 감소함을 보일 수 있게 한다는 점에서 위의 정의보다 더 일반적입니다. 자연수를 반환하는 노름 함수의 값을 비교하는 것은 그러한 측도의 한 예일 뿐이며, 이 경우 필요한 성질은 natAbs_norm_mod_lt 정리와 not_norm_mul_left_lt_norm 정리입니다.

instance : EuclideanDomain GaussInt :=
  { GaussInt.instCommRing with
    quotient := (· / ·)
    remainder := (· % ·)
    quotient_mul_add_remainder_eq :=
      fun x y ↦ by rw [mod_def, add_comm] ; ring
    quotient_zero := fun x ↦ by
      simp [div_def, norm, Int.div']
      rfl
    r := (measure (Int.natAbs ∘ norm)).1
    r_wellFounded := (measure (Int.natAbs ∘ norm)).2
    remainder_lt := natAbs_norm_mod_lt
    mul_left_not_lt := not_norm_mul_left_lt_norm }

이로써 곧바로 얻는 성과는, 이제 가우스 정수에서 소원(prime)이라는 개념과 기약원(irreducible)이라는 개념이 일치한다는 것을 알게 되었다는 점입니다.

example (x : GaussInt) : Irreducible x ↔ Prime x :=
  irreducible_iff_prime