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)\)의 집합으로 정의됩니다. 이 개념이 익숙하지 않다면 그림을 그려서, 이 집합이 꼭짓점이 \((1, 0, 0)\), \((0, 1, 0)\), \((0, 0, 1)\)인 3차원 공간의 정삼각형과 그 내부임을 스스로 확인해 보십시오. 이를 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를 사용하여 택틱 모드에서 확립합니다.
매개변수 \(\lambda\)가 \(0 \le \lambda \le 1\)을 만족할 때, 표준 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
구조체는 매개변수에 의존할 수 있습니다. 예를 들어, 임의의 \(n\)에 대해 표준 2-심플렉스를 표준 \(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의 원소입니다. Sigma 타입과 부분타입의 차이는, Sigma 타입의 두 번째 성분이 명제가 아니라 데이터라는 점입니다.
하지만 구조체 대신 곱, 부분타입, Sigma 타입을 사용할 수 있다 하더라도, 구조체를 사용하는 데에는 여러 가지 장점이 있습니다. 구조체를 정의하면 기저 표현이 추상화되고, 성분에 접근하는 함수에 사용자 지정 이름을 부여할 수 있습니다. 이는 증명을 더 견고하게 만듭니다. 구조체의 인터페이스에만 의존하는 증명은, 이전 접근자를 새 정의를 이용해 다시 정의하기만 하면, 정의를 변경하더라도 일반적으로 계속 작동합니다. 게다가 곧 살펴보겠지만, Lean은 구조체들을 엮어 풍부하고 상호 연결된 계층 구조를 만들고, 그들 사이의 상호작용을 관리하는 기능을 제공합니다.
7.2. 대수적 구조
대수적 구조라는 문구가 의미하는 바를 명확히 하기 위해, 몇 가지 예를 살펴보는 것이 도움이 될 것입니다.
부분 순서 집합은 집합 \(P\)와 \(P\) 위에서 추이적이고, 반사적이며, 반대칭적인 이항 관계 \(\le\)로 구성됩니다.
군은 집합 \(G\)와 결합 법칙을 만족하는 이항 연산, 항등원 \(1\), 그리고 \(G\)의 각 \(g\)에 대해 역원을 반환하는 함수 \(g \mapsto g^{-1}\)로 구성됩니다. 연산이 가환적이면 군은 아벨군 또는 가환군이라 합니다.
격자는 만남과 이음을 갖는 부분 순서 집합입니다.
환은 결합 법칙을 만족하는 곱셈 연산 \(\cdot\)와 항등원 \(1\)을 갖춘 (덧셈으로 표기된) 아벨군 \((R, +, 0, x \mapsto -x)\)로 구성되며, 곱셈은 덧셈에 대해 분배법칙을 만족합니다. 곱셈이 가환적이면 환은 가환환이라 합니다.
순서환 \((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\)입니다.
거리 공간은 집합 \(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)\)입니다.
위상 공간은 집합 \(X\)와 \(X\)의 부분집합들의 모임 \(\mathcal T\)로 구성되며, 이 부분집합들을 \(X\)의 열린 부분집합이라고 부르고, 다음이 성립합니다:
공집합과 \(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을 작성하고 정의를 컨트롤-클릭해 보면, 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에서는 군의 담지 타입(carrier type)으로 사용되는 타입에 대해 G와 같은 대문자 로마자를 사용하는 것이 일반적입니다.
Group₁ 타입의 원소를 정의하여 군을 구성해 봅시다. 임의의 타입 쌍 α와 β에 대해, Mathlib은 α와 β사이의 동치인 타입 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와 같도록 방향을 정하는데, 이때 순방향 함수는 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에서 임의의 두 위상 공간에 대해 상대적으로 정의됩니다. f : ℝ → ℂ가 있고 Continuous f를 작성하면, Lean은 ℝ와 ℂ상의 관련 위상을 찾아야 합니다.
이 마법은 세 가지 요소의 조합으로 이루어집니다.
논리. 임의의 군에서 해석되어야 하는 정의는 군의 타입과 군의 구조를 인자로 받습니다. 마찬가지로, 임의의 군의 원소에 관한 정리는 군의 타입과 군의 구조에 대한 전칭 한정자로 시작합니다.
암묵적 인자. 타입과 구조에 대한 인자는 일반적으로 암묵적으로 남겨두므로, 이를 직접 작성하거나 Lean 정보 창에서 볼 필요가 없습니다. Lean은 이 정보를 우리 대신 조용히 채워 넣습니다.
타입 클래스 추론. 클래스 추론이라고도 하는 이것은, 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\)의 제곱근이 되기를 원한다는 것을 기억하십시오. 따라서 우리는 다음을 원합니다
이는 아래의 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 네임스페이스에 작성되어 있습니다.
여기서 우리는 GaussInt.zero 등과 같이 이름을 붙이고 그 이름에 표기법을 지정하는 대신, 0, 1, +, -, * 표기법의 해석을 직접 정의하고 있다는 점에 유의하십시오. 정의에 명시적인 이름을 붙여두면, 예를 들어 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
이제 가우스 정수가 가환환의 인스턴스임을 보이는 것은 놀라울 정도로 쉽습니다. 우리는 구조체(structure) 개념을 유용하게 활용하고 있습니다. 각각의 특정한 가우스 정수는 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의 라이브러리는 nontrivial 타입의 클래스를 서로 다른 원소가 적어도 두 개 있는 타입으로 정의합니다. 환의 맥락에서, 이는 0이 1과 같지 않다는 것과 동치입니다. 일부 일반적인 정리들이 그 사실에 의존하므로, 지금 이를 확립해 두는 것이 좋겠습니다.
instance : Nontrivial GaussInt := by
use 0, 1
rw [Ne, GaussInt.ext_iff]
simp
이제 가우스 정수가 중요한 추가적인 성질을 가짐을 보이겠습니다. 유클리드 정역은 다음 두 가지 성질을 만족하는 노름 함수 \(N : R \to \mathbb{N}\)을 갖춘 환 \(R\)입니다:
모든 \(a\)와 \(R\)의 \(b \ne 0\)에 대해, \(a = bq + r\)이고 \(r = 0\)이거나 \(N(r) < N(b)\)인 \(q\)와 \(r\)이 \(R\)에 존재합니다.
모든 \(a\)와 \(b \ne 0\)에 대해, \(N(a) \le N(ab)\)입니다.
정수환 \(\Bbb{Z}\)는 \(N(a) = |a|\)로 정의할 때 유클리드 정역의 전형적인 예입니다. 이 경우 \(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}]\)에서 다음이 성립합니다.
그리고 원소 \(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\)를 취급하여, 나눗셈을 수행합니다
실수부와 허수부는 정수가 아닐 수 있지만, 이를 가장 가까운 정수 \(u\)와 \(v\)로 반올림할 수 있습니다. 그러면 우변을 \((u + vi) + (u' + v'i)\)로 표현할 수 있으며, 여기서 \(u' + v'i\)는 남은 부분입니다. 여기서 \(|u'| \le 1/2\)이고 \(|v'| \le 1/2\)임에 유의하십시오. 따라서
양변에 \(c + di\)를 곱하면 다음을 얻습니다
이제 \(q = u + vi\)와 \(r = (c + di) (u' + v'i)\)로 설정하면 \(a + bi = (c + di) q + r\)이 성립하므로, \(N(r)\)의 상한만 구하면 됩니다:
방금 수행한 논증은 가우스 정수를 복소수의 부분집합으로 보는 것을 요구합니다. 따라서 이를 Lean에서 형식화하는 한 가지 방법은, 가우스 정수를 복소수에 내장하고, 정수를 가우스 정수에 내장하고, 실수에서 정수로의 반올림 함수를 정의한 다음, 이러한 수 체계들 사이를 적절히 오가는 데 세심한 주의를 기울이는 것입니다. 실제로 이는 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의 실수부와 허수부는 다음에 가장 가까운 정수입니다
각각. 여기서 분자는 \((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 함수는 가우스 정수를 음이 아닌 정수로 대응시킵니다. 가우스 정수를 자연수로 대응시키는 함수가 필요하며, 정수를 자연수로 대응시키는 함수인 Int.natAbs와 norm을 합성하여 이를 얻습니다. 다음 두 보조정리 중 첫 번째는 노름을 자연수로 대응시켰다가 다시 정수로 대응시켜도 값이 바뀌지 않음을 증명합니다. 두 번째는 노름이 감소한다는 사실을 다시 표현합니다.
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