2. 기초
이 장은 Lean에서 수학적 추론을 하는 데 필요한 기본기, 즉 계산하기, 보조정리와 정리 적용하기, 일반적인 구조에 대해 추론하기를 소개하도록 구성되어 있습니다.
2.1. 계산하기
우리는 보통 수학적 계산을 증명으로 생각하지 않고 수행하는 법을 배웁니다. 그러나 Lean이 요구하는 대로 계산의 각 단계를 정당화하면, 최종 결과는 계산의 좌변이 우변과 같다는 증명이 됩니다.
Lean에서 정리를 진술하는 것은 목표, 즉 그 정리를 증명한다는 목표를 진술하는 것과 같습니다. Lean은 목표에서 항등식의 좌변을 우변으로 바꾸는 재작성 택틱 rw를 제공합니다. a, b, c가 실수라면, mul_assoc a b c는 항등식 a * b * c = a * (b * c)이고 mul_comm a b는 항등식 a * b = b * a입니다. Lean은 이러한 사실을 명시적으로 언급할 필요를 대개 없애 주는 자동화 기능을 제공하지만, 이러한 사실은 설명을 위해서는 유용합니다. Lean에서 곱셈은 왼쪽으로 결합하므로, mul_assoc의 좌변은 (a * b) * c로도 쓸 수 있습니다. 그러나 일반적으로 Lean의 표기 관례에 유의하여 Lean이 괄호를 생략하는 곳에서는 똑같이 괄호를 생략하는 것이 좋은 스타일입니다.
rw를 사용해 봅시다.
example (a b c : ℝ) : a * b * c = b * (a * c) := by
rw [mul_comm a b]
rw [mul_assoc b a c]
관련 예제 파일의 시작 부분에 있는 import 줄은 Mathlib에서 실수 이론과 함께 유용한 자동화 기능을 가져옵니다. 간결함을 위해 이 교재에서는 대개 이러한 정보를 생략합니다.
자유롭게 내용을 바꿔 보면서 어떤 일이 일어나는지 확인해 보십시오. VS Code에서는 ℝ 문자를 \R 또는 \real로 입력할 수 있습니다. 스페이스나 탭 키를 누르기 전까지는 기호가 나타나지 않습니다. Lean 파일을 읽을 때 기호 위에 마우스를 올리면 VS Code가 그 기호를 입력하는 데 사용할 수 있는 구문을 보여 줍니다. 사용할 수 있는 약어를 모두 보고 싶다면 Ctrl-Shift-P를 누른 뒤 abbreviations를 입력하여 Lean 4: Show Unicode Input Abbreviations 명령을 실행할 수 있습니다. 키보드에서 백슬래시를 입력하기 불편하다면 lean4.input.leader 설정을 바꿔 선행 문자를 변경할 수 있습니다.
커서가 택틱 증명 중간에 있으면 Lean은 Lean Infoview 창에 현재 증명 상태를 표시합니다. 커서를 옮기며 증명의 각 단계를 지나가면 상태가 바뀌는 것을 볼 수 있습니다. Lean의 전형적인 증명 상태는 다음과 같은 모습일 수 있습니다:
1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4
⊢로 시작하는 줄 앞의 줄들은 문맥을 나타냅니다. 문맥은 현재 다루고 있는 대상과 가정들입니다. 이 예에서 문맥에는 x와 y라는 두 대상이 있으며, 둘 다 자연수입니다. 또한 h₁, h₂, h₃이라는 이름이 붙은 세 가정도 있습니다. Lean에서는 문맥에 있는 모든 것에 식별자로 이름이 붙습니다. 이 아래첨자 이름들은 h\1, h\2, h\3으로 입력할 수 있지만, 올바른 식별자라면 무엇이든 괜찮습니다. 대신 h1, h2, h3을 쓰거나 foo, bar, baz를 써도 됩니다. 마지막 줄은 목표, 즉 증명해야 할 사실을 나타냅니다. 증명해야 할 사실을 대상(target)이라 부르고, 문맥과 대상을 합친 것을 목표라고 부르는 사람들도 있습니다. 실제로는 어떤 뜻으로 쓰였는지 대개 분명합니다.
이 항등식들을 증명해 보십시오. 각 경우에 sorry를 택틱 증명으로 바꾸면 됩니다. rw 택틱에서는 왼쪽 화살표(\l)를 사용하여 항등식을 반대 방향으로 적용할 수 있습니다. 예를 들어 rw [← mul_assoc a b c]는 현재 목표에서 a * (b * c)를 a * b * c로 바꿉니다. 왼쪽을 가리키는 화살표는 mul_assoc이 제공하는 항등식을 오른쪽에서 왼쪽으로 적용한다는 뜻이며, 목표의 좌변이나 우변과는 아무 관계가 없다는 점에 유의하십시오.
example (a b c : ℝ) : c * b * a = b * (a * c) := by
sorry
example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
sorry
mul_assoc나 mul_comm 같은 항등식은 인자 없이 사용할 수도 있습니다. 이 경우 rewrite 택틱은 좌변을 목표에 있는 표현식과 매칭하려고 시도하며, 처음 발견한 패턴을 사용합니다.
example (a b c : ℝ) : a * b * c = b * c * a := by
rw [mul_assoc]
rw [mul_comm]
일부 정보만 제공할 수도 있습니다. 예를 들어 mul_comm a는 a * ? 꼴의 모든 패턴과 맞아떨어지며, 이를 ? * a로 다시 씁니다. 이 예제 중 첫 번째는 인자를 전혀 제공하지 않고, 두 번째는 인자를 하나만 제공하여 풀어 보십시오.
example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
sorry
example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
sorry
지역 문맥에 있는 사실을 rw와 함께 사용할 수도 있습니다.
example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
rw [h']
rw [← mul_assoc]
rw [h]
rw [mul_assoc]
다음 예제들을 풀어 보십시오. 두 번째 예제에는 정리 sub_self를 사용하십시오:
example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by
sorry
example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := by
sorry
관련 항등식들을 대괄호 안에 쉼표로 구분하여 나열하면, 여러 개의 rewrite 명령을 명령 하나로 수행할 수 있습니다.
example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
rw [h', ← mul_assoc, h, mul_assoc]
이때에도 rewrite 목록에서 아무 쉼표 뒤에나 커서를 두면 단계별 진행 상황을 볼 수 있습니다.
또 다른 요령은 변수를 예제나 정리 바깥에서 한 번에 선언해 둘 수 있다는 것입니다. 그러면 Lean이 그 변수들을 자동으로 포함합니다.
variable (a b c d e f : ℝ)
example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
rw [h', ← mul_assoc, h, mul_assoc]
위 증명의 시작 부분에서 택틱 상태를 살펴보면 Lean이 실제로 모든 변수를 포함했음을 알 수 있습니다. 선언을 section ... end 블록 안에 넣으면 선언의 범위를 제한할 수 있습니다. 마지막으로, 도입부에서 Lean이 표현식의 타입을 확인하는 명령을 제공한다는 것을 떠올려 봅시다:
section
variable (a b c : ℝ)
#check a
#check a + b
#check (a : ℝ)
#check mul_comm a b
#check (mul_comm a b : a * b = b * a)
#check mul_assoc c a b
#check mul_comm a
#check mul_comm
end
#check 명령은 대상과 사실 모두에 대해 동작합니다. #check a 명령에 대해 Lean은 a의 타입이 ℝ이라고 알려 줍니다. #check mul_comm a b 명령에 대해 Lean은 mul_comm a b가 a * b = b * a라는 사실의 증명이라고 알려 줍니다. #check (a : ℝ) 명령은 a의 타입이 ℝ일 것이라는 우리의 예상을 나타내며, 그렇지 않으면 Lean은 오류를 발생시킵니다. 마지막 세 #check 명령의 출력은 나중에 설명하겠지만, 그동안 출력을 살펴보고 직접 #check 명령을 몇 가지 실험해 보아도 좋습니다.
예제를 몇 가지 더 살펴봅시다. 정리 two_mul a는 2 * a = a + a임을 말해 줍니다. 정리 add_mul과 mul_add는 덧셈에 대한 곱셈의 분배법칙을 나타내고, 정리 add_assoc은 덧셈의 결합법칙을 나타냅니다. 정확한 명제를 확인하려면 #check 명령을 사용하십시오.
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
rw [mul_add, add_mul, add_mul]
rw [← add_assoc, add_assoc (a * a)]
rw [mul_comm b a, ← two_mul]
편집기에서 이 증명을 한 단계씩 따라가 보면 무슨 일이 일어나는지 파악할 수는 있지만, 증명 자체만 놓고 읽기는 어렵습니다. Lean은 calc 키워드를 사용하여 이와 같은 증명을 더 구조적으로 작성하는 방법을 제공합니다.
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
(a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
rw [mul_add, add_mul, add_mul]
_ = a * a + (b * a + a * b) + b * b := by
rw [← add_assoc, add_assoc (a * a)]
_ = a * a + 2 * (a * b) + b * b := by
rw [mul_comm b a, ← two_mul]
이 증명이 by로 시작하지 않는다는 점에 주목하십시오. calc로 시작하는 표현식은 증명 항입니다. calc 표현식은 택틱 증명 안에서도 사용할 수 있지만, 이 경우 Lean은 이를 결과로 나온 증명 항을 사용하여 목표를 해결하라는 지시로 해석합니다. calc 구문은 까다롭습니다. 밑줄과 근거는 위에 제시된 형식을 따라야 합니다. Lean은 택틱 블록이나 calc 블록이 어디에서 시작하고 끝나는지 등을 들여쓰기로 판단합니다. 위 증명의 들여쓰기를 바꿔 보고 어떤 일이 일어나는지 확인해 보십시오.
calc 증명을 작성하는 한 가지 방법은 먼저 근거 자리에 sorry 택틱을 넣어 개요를 잡고, 이 부분들을 제외하면 Lean이 표현식을 받아들이는지 확인한 다음, 택틱을 사용하여 각 단계의 근거를 채우는 것입니다.
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
(a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
sorry
_ = a * a + (b * a + a * b) + b * b := by
sorry
_ = a * a + 2 * (a * b) + b * b := by
sorry
다음 항등식을 순수한 rw 증명과 더 구조적인 calc 증명 두 가지 방식으로 모두 증명해 보십시오:
example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
sorry
다음 연습 문제는 조금 더 어렵습니다. 아래에 나열된 정리들을 사용할 수 있습니다.
example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
sorry
#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a
문맥에 있는 가정에서도 재작성을 수행할 수 있습니다. 예를 들어, rw [mul_comm a b] at hyp는 가정 hyp에서 a * b를 b * a로 바꿉니다.
example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
rw [hyp'] at hyp
rw [mul_comm d a] at hyp
rw [← two_mul (a * d)] at hyp
rw [← mul_assoc 2 a d] at hyp
exact hyp
마지막 단계에서 exact 택틱은 hyp를 사용해 목표를 해결할 수 있습니다. 그 시점에서 hyp가 목표와 정확히 일치하기 때문입니다.
이 절을 마치며, Mathlib이 ring 택틱이라는 유용한 자동화 도구를 제공한다는 점을 짚어 둡니다. 이 택틱은 지역 가정을 전혀 사용하지 않고 순전히 환 공리로부터 따라 나오는 항등식이라면 어떤 가환환에서든 증명하도록 설계되었습니다.
example : c * b * a = b * (a * c) := by
ring
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
ring
example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
ring
example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
rw [hyp, hyp']
ring
ring 택틱은 Mathlib.Data.Real.Basic을 임포트할 때 간접적으로 함께 임포트되지만, 다음 절에서 이 택틱을 실수 이외의 구조에 대한 계산에도 사용할 수 있음을 보게 될 것입니다. 이 택틱은 import Mathlib.Tactic 명령으로 명시적으로 임포트할 수 있습니다. 다른 흔한 종류의 대수적 구조에 대해서도 비슷한 택틱이 있음을 보게 될 것입니다.
rw의 변형으로 nth_rw가 있는데, 이를 사용하면 목표에 있는 표현식 중 특정 사례만 바꿀 수 있습니다. 일치할 수 있는 항목에는 1부터 번호가 매겨지므로, 다음 예제에서 nth_rw 2 [h]는 a + b의 두 번째 출현을 c로 바꿉니다.
example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
nth_rw 2 [h]
rw [add_mul]
2.2. 대수적 구조에서 항등식 증명하기
수학적으로 환은 대상들의 모임 \(R\), 연산 \(+\)와 \(\times\), 상수 \(0\)과 \(1\), 그리고 연산 \(x \mapsto -x\)로 이루어지며, 다음을 만족합니다:
\(R\)은 \(+\)에 대해 아벨 군을 이루며, \(0\)이 덧셈 항등식의 항등원 역할을 하고 부호 반전이 역원 역할을 합니다.
곱셈은 결합법칙을 만족하며 \(1\)을 항등식의 항등원으로 가지고, 곱셈은 덧셈에 대해 분배됩니다.
Lean에서 대상들의 모임은 타입 R로 표현됩니다. 환 공리는 다음과 같습니다:
variable (R : Type*) [Ring R]
#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (neg_add_cancel : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)
첫 번째 줄의 대괄호에 대해서는 나중에 더 자세히 배우겠지만, 지금은 이 선언이 타입 R과 R 위의 환 구조를 제공한다는 정도만 알아 두면 충분합니다. 그러면 Lean은 R의 원소에 일반적인 환 표기법을 사용할 수 있게 해 주고, 환에 관한 정리 라이브러리도 활용할 수 있게 해 줍니다.
일부 정리의 이름은 낯익을 것입니다. 바로 앞 절에서 실수를 계산할 때 사용했던 바로 그 정리들이기 때문입니다. Lean은 자연수나 정수 같은 구체적인 수학적 구조에 대한 사실을 증명하는 데뿐만 아니라, 환처럼 공리로 특징지어지는 추상적인 구조에 대한 사실을 증명하는 데에도 유용합니다. 더 나아가 Lean은 추상적인 구조와 구체적인 구조 모두에 대해 일반적 추론을 지원하며, 적절한 인스턴스를 인식하도록 훈련시킬 수 있습니다. 따라서 환에 관한 정리는 무엇이든 정수 ℤ, 유리수 ℚ, 복소수 ℂ와 같은 구체적인 환에 적용할 수 있습니다. 또한 순서환이나 체처럼 환을 확장하는 추상적인 구조의 어떤 인스턴스에도 적용할 수 있습니다.
그러나 실수의 중요한 성질이 모두 임의의 환에서 성립하는 것은 아닙니다. 예를 들어 실수의 곱셈은 교환 법칙을 만족하지만, 일반적인 환에서는 그렇지 않습니다. 선형대수 강의를 들어 본 적이 있다면, 모든 \(n\)에 대해 실수를 성분으로 하는 \(n\) 행 \(n\) 열 행렬들이 교환법칙이 대개 성립하지 않는 환을 이룬다는 것을 알 것입니다. 사실 R을 가환 환으로 선언하면, 앞 절의 모든 정리는 ℝ을 R로 바꾸어도 여전히 성립합니다.
variable (R : Type*) [CommRing R]
variable (a b c d : R)
example : c * b * a = b * (a * c) := by ring
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring
example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring
example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
rw [hyp, hyp']
ring
나머지 증명들이 수정 없이 그대로 통과하는지는 여러분이 직접 확인해 보십시오. by ring이나 by linarith, by sorry처럼 증명이 짧을 때는 by와 같은 줄에 쓰는 것이 일반적이며 (또한 허용된다는) 점에 유의하십시오. 좋은 증명 작성 스타일은 간결성과 가독성 사이에서 균형을 이루어야 합니다.
이 절의 목표는 이전 절에서 익힌 기술을 강화하고, 이를 환에 대한 공리적 추론에 적용하는 것입니다. 위에 나열한 공리에서 출발하여, 이를 이용해 다른 사실들을 유도하겠습니다. 우리가 증명하는 사실 대부분은 이미 Mathlib에 들어 있습니다. 라이브러리의 내용과 명명 규칙을 익히는 데 도움이 되도록, 우리가 증명하는 버전에도 같은 이름을 붙이겠습니다.
Lean은 프로그래밍 언어에서 사용하는 것과 비슷한 조직화 메커니즘을 제공합니다. 정의나 정리 foo가 네임스페이스 bar 안에서 도입되면, 그 전체 이름은 bar.foo입니다. 이후 open bar 명령은 해당 네임스페이스를 열어 더 짧은 이름 foo를 사용할 수 있게 해 줍니다. 이름 충돌로 인한 오류를 피하기 위해, 다음 예제에서는 라이브러리 정리의 우리 버전을 MyRing.이라는 새 네임스페이스에 넣습니다.
다음 예제는 add_zero나 add_neg_cancel이 다른 공리로부터 유도되므로 환 공리로 둘 필요가 없음을 보여 줍니다.
namespace MyRing
variable {R : Type*} [Ring R]
theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]
theorem add_neg_cancel (a : R) : a + -a = 0 := by rw [add_comm, neg_add_cancel]
#check MyRing.add_zero
#check add_zero
end MyRing
결과적으로 라이브러리에 있는 정리를 일시적으로 다시 증명한 뒤, 그 이후로는 라이브러리 버전을 계속 사용할 수 있습니다. 하지만 속임수를 쓰지는 마십시오! 이어지는 연습 문제에서는 이 절의 앞부분에서 증명한 환에 대한 일반적인 사실만 사용하도록 주의하십시오.
(주의 깊게 살펴보셨다면 (R : Type*)의 소괄호를 {R : Type*}의 중괄호로 바꾼 것을 눈치채셨을 수도 있습니다. 이는 R을 암시적 인자로 선언합니다. 이것이 무엇을 의미하는지는 곧 설명할 것이므로, 그때까지는 신경 쓰지 않으셔도 됩니다.)
다음은 유용한 정리입니다:
theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
rw [← add_assoc, neg_add_cancel, zero_add]
짝이 되는 버전을 증명하십시오:
theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
sorry
이것들을 사용하여 다음을 증명하십시오:
theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
sorry
theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
sorry
충분히 계획을 세우면 각각을 세 번의 재작성으로 해낼 수 있습니다.
이제 중괄호의 쓰임을 설명하겠습니다. 문맥에 a, b, c와 가설 h : a + b = a + c가 있고, 여기서 b = c라는 결론을 이끌어 내고 싶은 상황을 떠올려 보십시오. Lean에서는 정리를 대상에 적용할 때와 똑같은 방식으로 가설과 사실에도 적용할 수 있으므로, add_left_cancel a b c h가 b = c라는 사실의 증명이라고 생각할 수도 있습니다. 하지만 가설 h를 보면 우리가 염두에 둔 대상이 무엇인지 분명하므로, a, b, c를 명시적으로 쓰는 것은 불필요하다는 점에 주목하십시오. 이 경우에는 몇 글자 더 입력하는 것이 번거롭지 않지만, add_left_cancel을 더 복잡한 표현식에 적용하려 한다면 그것들을 모두 적는 일은 지루할 것입니다. 이런 경우를 위해 Lean에서는 인자를 암시적(implicit)으로 표시할 수 있습니다. 이는 해당 인자를 생략하고, 뒤따르는 인자나 가설 같은 다른 수단으로 추론하게 한다는 뜻입니다. {a b c : R}의 중괄호가 바로 그 역할을 합니다. 따라서 위 정리의 명제가 주어졌을 때, 올바른 표현식은 간단히 add_left_cancel h입니다.
예를 들어, a * 0 = 0이 환 공리로부터 따라 나온다는 것을 보여 봅시다.
theorem mul_zero (a : R) : a * 0 = 0 := by
have h : a * 0 + a * 0 = a * 0 + 0 := by
rw [← mul_add, add_zero, add_zero]
rw [add_left_cancel h]
새로운 기법을 사용했습니다! 증명을 한 단계씩 따라가 보면 무슨 일이 일어나는지 확인할 수 있습니다. have 택틱은 원래 목표와 같은 문맥을 가진 새로운 목표 a * 0 + a * 0 = a * 0 + 0을 도입합니다. 다음 줄이 들여쓰기되어 있다는 것은 Lean이 이 새로운 목표를 증명하는 데 쓰일 택틱 블록을 기대하고 있음을 나타냅니다. 따라서 들여쓰기는 모듈식 증명 스타일을 장려합니다. 들여쓰기된 하위 증명은 have로 도입된 목표를 증명합니다. 그 후에는 다시 원래 목표를 증명하는 단계로 돌아오지만, 새로운 가설 h가 추가되어 있습니다. 이 가설은 이미 증명했으므로 이제 자유롭게 사용할 수 있습니다. 이 시점에서 목표는 정확히 add_left_cancel h의 결과입니다.
apply add_left_cancel h 또는 exact add_left_cancel h로 증명을 마무리해도 똑같이 좋았을 것입니다. exact 택틱은 현재 목표를 완전히 증명하는 증명 항을 인자로 받으며, 새로운 목표를 만들지 않습니다. apply 택틱은 인자가 반드시 완전한 증명일 필요는 없는 변형입니다. 빠진 부분은 Lean이 자동으로 추론하거나, 증명해야 할 새로운 목표가 됩니다. exact 택틱은 apply보다 엄밀히 덜 강력하므로 기술적으로는 불필요하지만, 사람이 읽기에 증명 스크립트를 조금 더 명확하게 만들고 라이브러리가 발전할 때 유지 관리하기 쉽게 해 줍니다.
곱셈이 교환법칙을 만족한다고 가정하지 않는다는 점을 기억하십시오. 따라서 다음 정리도 증명하려면 약간의 작업이 필요합니다.
theorem zero_mul (a : R) : 0 * a = 0 := by
sorry
이제는 다음 연습 문제의 각 sorry도 증명으로 바꿀 수 있을 것입니다. 이번에도 이 절에서 확립한 환에 관한 사실과 공리 eq_symm만 사용하십시오.
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
sorry
theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
sorry
theorem neg_zero : (-0 : R) = 0 := by
apply neg_eq_of_add_eq_zero
rw [add_zero]
theorem neg_neg (a : R) : - -a = a := by
sorry
세 번째 정리에서 0 대신 (-0 : R)이라는 표기를 사용해야 했던 이유는, R을 명시하지 않으면 Lean이 우리가 염두에 둔 0이 어떤 것인지 추론할 수 없고, 기본적으로는 자연수로 해석되기 때문입니다.
Lean에서 환의 뺄셈은 덧셈에 대한 역원을 더하는 것과 같음을 증명할 수 있습니다.
example (a b : R) : a - b = a + -b :=
sub_eq_add_neg a b
실수에서는 뺄셈이 그렇게 정의되어 있습니다:
example (a b : ℝ) : a - b = a + -b :=
rfl
example (a b : ℝ) : a - b = a + -b := by
rfl
증명 항 rfl은 “반사성(reflexivity)”의 줄임말입니다. 이 항을 a - b = a + -b의 증명으로 제시하면 Lean은 정의를 펼쳐서 양변이 같다는 것을 인식할 수밖에 없습니다. rfl 택틱도 같은 일을 합니다. 이는 Lean의 기반 논리에서 정의상 동등성이라고 알려진 것의 한 예입니다. 이는 sub_eq_add_neg로 재작성하여 a - b = a + -b를 대체할 수 있을 뿐만 아니라, 어떤 문맥에서는 실수를 다룰 때 등식의 양변을 서로 바꾸어 사용할 수 있다는 뜻입니다. 예를 들어, 이제 지난 절의 정리 self_sub을 증명하는 데 필요한 정보를 모두 갖추었습니다:
theorem self_sub (a : R) : a - a = 0 := by
sorry
rw를 사용해 이를 증명할 수 있음을 보이십시오. 다만 임의의 환 R을 실수로 바꾸면 apply나 exact를 사용해서도 증명할 수 있습니다.
Lean은 모든 환에서 1 + 1 = 2가 성립한다는 것을 알고 있습니다. 약간의 노력을 기울이면 이를 이용해 지난 절의 정리 two_mul을 증명할 수 있습니다:
theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
norm_num
theorem two_mul (a : R) : 2 * a = a + a := by
sorry
이 절을 마무리하며, 위에서 확립한 덧셈과 부호 반전에 관한 사실 중 일부는 환 공리 전체는 물론이고 덧셈의 교환법칙조차 필요로 하지 않는다는 점을 짚어 두겠습니다. 더 약한 개념인 군은 다음과 같이 공리화할 수 있습니다:
variable (A : Type*) [AddGroup A]
#check (add_assoc : ∀ a b c : A, a + b + c = a + (b + c))
#check (zero_add : ∀ a : A, 0 + a = a)
#check (neg_add_cancel : ∀ a : A, -a + a = 0)
군 연산이 가환일 때는 덧셈 표기법을, 그렇지 않을 때는 곱셈 표기법을 사용하는 것이 관례입니다. 그래서 Lean은 덧셈 버전뿐 아니라 곱셈 버전도 정의합니다(그리고 이들의 아벨 변형인 AddCommGroup과 CommGroup도 정의합니다).
variable {G : Type*} [Group G]
#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1)
자신이 있다면 이 공리들만 사용하여 군에 관한 다음 사실들을 증명해 보십시오. 그 과정에서 여러 보조정리를 증명해야 할 것입니다. 이 절에서 수행한 증명들이 몇 가지 힌트를 줍니다.
theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by
sorry
theorem mul_one (a : G) : a * 1 = a := by
sorry
theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
sorry
이 보조정리들을 명시적으로 호출하는 것은 번거로우므로, Mathlib은 대부분의 용도를 다룰 수 있도록 ring과 비슷한 택틱을 제공합니다: group은 비가환 곱셈군을, abel은 아벨 덧셈군을, noncomm_ring은 비가환환을 위한 것입니다. 대수적 구조는 Ring과 CommRing이라고 부르는 반면 택틱의 이름은 noncomm_ring과 ring이라는 점이 이상하게 보일 수도 있습니다. 이는 부분적으로는 역사적인 이유 때문이지만, 가환환을 다루는 택틱이 더 자주 쓰이므로 그 택틱에 더 짧은 이름을 붙이는 편이 편리하기 때문이기도 합니다.
2.3. 정리와 보조정리 사용하기
재작성은 등식을 증명하는 데 매우 유용하지만, 다른 종류의 정리는 어떻게 증명하겠습니까? 예를 들어, \(b \le c\)일 때마다 \(a + e^b \le a + e^c\)가 성립한다는 사실과 같은 부등식은 어떻게 증명할 수 있겠습니까? 우리는 정리를 인수와 가설에 적용할 수 있다는 것과, apply와 exact 택틱을 사용하여 목표를 해결할 수 있다는 것을 이미 살펴보았습니다. 이 절에서는 이러한 도구들을 잘 활용해 보겠습니다.
라이브러리 정리 le_refl과 le_trans를 살펴봅시다:
#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
제 3.1 절에서 더 자세히 설명하겠지만, le_trans의 명제에 있는 암묵적 괄호는 오른쪽으로 결합하므로 a ≤ b → (b ≤ c → a ≤ c)로 해석해야 합니다. 라이브러리 설계자들은 le_trans의 인수 a, b, c를 암묵적 인수로 설정해 두었으므로, Lean에서는 (나중에 논의하겠지만 정말로 고집하지 않는 한) 이 인수들을 명시적으로 제공할 수 없습니다. 대신 Lean은 이 인수들이 사용되는 문맥으로부터 이를 추론하려고 합니다. 예를 들어, 가설 h : a ≤ b와 h' : b ≤ c가 문맥에 있을 때, 다음은 모두 작동합니다:
variable (h : a ≤ b) (h' : b ≤ c)
#check (le_refl : ∀ a : Real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)
apply 택틱은 일반적인 명제나 함의의 증명을 받아 그 결론을 현재 목표와 맞춰 보고, 가설이 있으면 그것들을 새로운 목표로 남깁니다. 주어진 증명이 목표와 (정의상 동등성까지 감안하여) 정확히 일치한다면 apply 대신 exact 택틱을 사용할 수 있습니다. 따라서 다음은 모두 동작합니다:
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
apply le_trans
· apply h₀
· apply h₁
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
apply le_trans h₀
apply h₁
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
le_trans h₀ h₁
example (x : ℝ) : x ≤ x := by
apply le_refl
example (x : ℝ) : x ≤ x :=
le_refl x
첫 번째 예제에서 le_trans를 적용하면 두 개의 목표가 생기며, 각 목표의 증명이 어디서 시작되는지 점으로 표시합니다. 점은 선택 사항이지만 목표에 초점을 맞추는 역할을 합니다: 점으로 시작하는 블록 안에서는 목표 하나만 보이며, 블록이 끝나기 전에 그 목표를 완료해야 합니다. 여기서는 다른 점으로 새 블록을 시작하여 첫 번째 블록을 끝냅니다. 들여쓰기를 줄여도 똑같이 할 수 있었습니다. 세 번째 예제와 마지막 예제에서는 택틱 모드에 아예 들어가지 않습니다: le_trans h₀ h₁과 le_refl x가 바로 필요한 증명 항입니다.
라이브러리 정리를 몇 가지 더 소개합니다:
#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)
이 정리들을 apply 및 exact와 함께 사용하여 다음을 증명하십시오:
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
sorry
사실 Lean에는 이런 종류의 작업을 자동으로 해 주는 택틱이 있습니다:
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
linarith
linarith 택틱은 선형 산술을 처리하도록 설계되었습니다.
example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
linarith
지역 문맥에 있는 등식과 부등식 외에도, linarith는 인자로 전달한 추가 부등식도 사용합니다. 다음 예제에서 exp_le_exp.mpr h'는 exp b ≤ exp c의 증명입니다. 이에 대해서는 잠시 후 설명하겠습니다. Lean에서는 함수 f를 인자 x에 적용한 것을 f x로 나타내며, 이는 사실이나 정리 h를 인자 x에 적용한 결과를 h x로 나타내는 것과 정확히 같은 방식이라는 점에 주목하십시오. 괄호는 f (x + y)처럼 복합 인자에서만 필요합니다. 괄호가 없으면 f x + y는 (f x) + y로 파싱됩니다.
example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
linarith [exp_le_exp.mpr h']
라이브러리에는 실수에 대한 부등식을 증명하는 데 사용할 수 있는 정리가 몇 가지 더 있습니다.
#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_right : a ≤ b → ∀ c, c + a ≤ c + b)
#check (add_le_add_left : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
#check (add_lt_add_right : a < b → ∀ c, c + a < c + b)
#check (add_lt_add_left : a < b → ∀ c, a + c < b + c)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check add_le_add_right
이 정리 중 exp_le_exp, exp_lt_exp 등 일부는 “if and only if(필요충분조건)”라는 표현을 나타내는 쌍방향 함의를 사용합니다. (VS Code에서는 \lr 또는 \iff로 입력할 수 있습니다.) 이 연결사에 대해서는 다음 장에서 더 자세히 다루겠습니다. 이러한 정리는 rw와 함께 사용하여 목표를 그와 동치인 목표로 다시 쓸 수 있습니다:
example (h : a ≤ b) : exp a ≤ exp b := by
rw [exp_le_exp]
exact h
하지만 이 절에서는 h : A ↔ B가 그러한 동치일 때 h.mp는 정방향인 A → B를 증명하고, h.mpr은 역방향인 B → A를 증명한다는 사실을 사용하겠습니다. 여기서 mp는 “modus ponens(전건 긍정)”를, mpr은 “modus ponens reverse(역방향 전건 긍정)”를 뜻합니다. 원한다면 h.mp와 h.mpr 대신 각각 h.1과 h.2를 사용할 수도 있습니다. 따라서 다음 증명은 올바르게 작동합니다:
example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := by
apply add_lt_add_of_lt_of_le
· apply add_lt_add_of_le_of_lt h₀
apply exp_lt_exp.mpr h₁
apply le_refl
첫 번째 줄인 apply add_lt_add_of_lt_of_le는 두 개의 목표를 만들며, 이번에도 점을 사용하여 첫 번째 목표의 증명과 두 번째 목표의 증명을 구분합니다.
다음 예제들을 직접 풀어 보십시오. 가운데 예제는 norm_num 택틱을 사용하여 구체적인 수치 목표를 해결할 수 있음을 보여 줍니다.
example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry
example : (0 : ℝ) < 1 := by norm_num
example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
have h₀ : 0 < 1 + exp a := by sorry
apply log_le_log h₀
sorry
이 예제들을 보면 필요한 라이브러리 정리를 찾아내는 능력이 형식화의 중요한 부분이라는 점이 분명해집니다. 활용할 수 있는 전략은 여러 가지가 있습니다:
Mathlib은 GitHub 저장소에서 둘러볼 수 있습니다.
Mathlib 웹 페이지에 있는 API 문서를 이용할 수 있습니다.
Loogle <https://loogle.lean-lang.org>을 사용하여 Lean과 Mathlib의 정의와 정리를 패턴으로 검색할 수 있습니다.
정리 이름을 짐작할 때는 Mathlib 명명 규칙과 편집기의 Ctrl-space 자동 완성(Mac 키보드에서는 Cmd-space)을 활용할 수 있습니다. Lean에서
A_of_B_of_C라는 이름의 정리는B형태와C형태의 가설로부터A형태의 무언가를 증명합니다. 여기서A,B,C는 우리가 목표를 소리 내어 읽는 방식을 대략적으로 나타냅니다. 따라서x + y ≤ ...와 같은 것을 증명하는 정리는 아마도add_le로 시작할 것입니다.add_le를 입력하고 Ctrl-space를 누르면 도움이 되는 몇 가지 선택지가 나타납니다. Ctrl-space를 두 번 누르면 사용 가능한 자동 완성 항목에 대한 더 많은 정보가 표시된다는 점에 유의하십시오.VS Code에서 기존 정리 이름을 마우스 오른쪽 버튼으로 클릭하면, 편집기는 그 정리가 정의된 파일로 이동하는 옵션이 포함된 메뉴를 보여 주며, 그 근처에서 비슷한 정리들을 찾을 수 있습니다.
라이브러리에서 관련 정리를 찾으려고 시도하는
apply?택틱을 사용할 수 있습니다.
example : 0 ≤ a ^ 2 := by
-- apply?
exact sq_nonneg a
이 예제에서 apply?를 시험해 보려면 exact 명령을 지우고 그 앞 줄의 주석을 해제하십시오. 이러한 요령을 사용하여 다음 예제를 푸는 데 필요한 것을 찾을 수 있는지 확인해 보십시오:
example (h : a ≤ b) : c - exp b ≤ c - exp a := by
sorry
같은 요령을 사용하여 apply? 대신 linarith로도 작업을 마칠 수 있음을 확인하십시오.
다음은 부등식의 또 다른 예입니다:
example : 2*a*b ≤ a^2 + b^2 := by
have h : 0 ≤ a^2 - 2*a*b + b^2
calc
a^2 - 2*a*b + b^2 = (a - b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
calc
2*a*b = 2*a*b + 0 := by ring
_ ≤ 2*a*b + (a^2 - 2*a*b + b^2) := add_le_add (le_refl _) h
_ = a^2 + b^2 := by ring
Mathlib은 *나 ^ 같은 이항 연산 앞뒤에 공백을 두는 경향이 있지만, 이 예제에서는 더 압축된 형식이 가독성을 높입니다. 주목할 만한 점이 몇 가지 있습니다. 첫째, 표현식 s ≥ t는 t ≤ s와 정의상 동치입니다. 원칙적으로 이는 두 표현을 서로 바꾸어 쓸 수 있어야 한다는 뜻입니다. 하지만 Lean의 자동화 기능 중 일부는 이 동치를 인식하지 못하므로, Mathlib은 ≥보다 ≤를 선호하는 경향이 있습니다. 둘째, 우리는 ring 택틱을 폭넓게 사용했습니다. 이 택틱은 정말로 시간을 크게 절약해 줍니다! 마지막으로, 두 번째 calc 증명의 두 번째 줄에서 by exact add_le_add (le_refl _) h라고 쓰는 대신 증명 항 add_le_add (le_refl _) h를 그대로 쓸 수 있다는 점에 주목하십시오.
사실 위 증명에서 유일하게 기발함이 필요한 부분은 가설 h를 찾아내는 것입니다. 일단 이 가설을 얻으면 두 번째 계산에는 선형 산술만 필요하므로 linarith가 처리할 수 있습니다:
example : 2*a*b ≤ a^2 + b^2 := by
have h : 0 ≤ a^2 - 2*a*b + b^2
calc
a^2 - 2*a*b + b^2 = (a - b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
linarith
정말 멋집니다! 이 아이디어들을 사용하여 다음 정리를 증명해 보십시오. abs_le'.mpr 정리를 사용할 수 있습니다. 또한 논리곱을 두 개의 목표로 나누려면 constructor 택틱이 필요합니다. 제 3.4 절을 참고하십시오.
example : |a*b| ≤ (a^2 + b^2)/2 := by
sorry
#check abs_le'.mpr
이 문제를 해결하셨다면 축하드립니다! 여러분은 형식화의 달인이 되는 길을 순조롭게 걸어가고 있습니다.
2.4. apply와 rw를 사용하는 더 많은 예제
실수에서 min 함수는 다음 세 가지 사실로 유일하게 특징지어집니다.
#check (min_le_left a b : min a b ≤ a)
#check (min_le_right a b : min a b ≤ b)
#check (le_min : c ≤ a → c ≤ b → c ≤ min a b)
이와 비슷한 방식으로 max를 특징짓는 정리들의 이름을 짐작할 수 있습니까?
min을 두 인수 a와 b에 적용할 때는 min (a, b)가 아니라 min a b라고 써야 한다는 점에 주목하십시오. 형식적으로 min은 ℝ → ℝ → ℝ 타입의 함수입니다. 이처럼 화살표가 여러 개인 타입을 쓸 때는 암묵적인 괄호가 오른쪽으로 결합한다는 관례가 있으므로, 이 타입은 ℝ → (ℝ → ℝ)로 해석됩니다. 결과적으로 a와 b가 ℝ 타입을 가지면 min a는 ℝ → ℝ 타입을 가지고 min a b는 ℝ 타입을 가지므로, min은 우리가 기대하는 대로 두 인수를 받는 함수처럼 동작합니다. 이런 방식으로 여러 인수를 다루는 것을 논리학자 Haskell Curry의 이름을 따서 커링(currying)이라고 합니다.
Lean의 연산 순서도 익숙해지는 데 시간이 조금 걸릴 수 있습니다. 함수 적용은 중위 연산보다 결합 우선순위가 높으므로, 표현식 min a b + c는 (min a b) + c로 해석됩니다. 시간이 지나면 이러한 관례가 자연스럽게 몸에 밸 것입니다.
le_antisymm 정리를 사용하면, 두 실수가 서로 상대보다 작거나 같을 때 두 실수가 같다는 것을 보일 수 있습니다. 이것과 위의 사실들을 사용하면 min이 교환법칙을 만족한다는 것을 보일 수 있습니다:
example : min a b = min b a := by
apply le_antisymm
· show min a b ≤ min b a
apply le_min
· apply min_le_right
apply min_le_left
· show min b a ≤ min a b
apply le_min
· apply min_le_right
apply min_le_left
여기서는 서로 다른 목표의 증명을 구분하기 위해 점을 사용했습니다. 점을 쓰는 방식이 일관되지는 않습니다: 바깥쪽 수준에서는 두 목표 모두에 점과 들여쓰기를 사용한 반면, 중첩된 증명에서는 목표가 하나만 남을 때까지만 점을 사용했습니다. 두 관례 모두 합리적이고 유용합니다. 또한 show 택틱을 사용하여 증명을 구조화하고 각 블록에서 무엇을 증명하고 있는지 나타냈습니다. show 명령이 없어도 증명은 여전히 동작하지만, 이를 사용하면 증명을 읽고 유지보수하기가 더 쉬워집니다.
증명이 반복적이라는 점이 거슬릴 수도 있습니다. 나중에 배울 기술을 미리 보여 드리자면, 반복을 피하는 한 가지 방법은 지역 보조정리를 기술한 다음 그것을 사용하는 것입니다:
example : min a b = min b a := by
have h : ∀ x y : ℝ, min x y ≤ min y x := by
intro x y
apply le_min
apply min_le_right
apply min_le_left
apply le_antisymm
apply h
apply h
전칭 한정기호에 대해서는 제 3.1 절에서 더 자세히 다루겠지만, 여기서는 가설 h가 임의의 x와 y에 대해 원하는 부등식이 성립한다는 것을 말하며, intro 택틱이 결론을 확립하기 위해 임의의 x와 y를 도입한다는 것만 말해 두겠습니다. le_antisymm 다음의 첫 번째 apply는 암묵적으로 h a b를 사용하고, 두 번째 apply는 h b a를 사용합니다.
또 다른 해결책은 repeat 택틱을 사용하는 것입니다. 이 택틱은 하나의 택틱(또는 블록)을 적용할 수 있는 만큼 여러 번 적용합니다.
example : min a b = min b a := by
apply le_antisymm
repeat
apply le_min
apply min_le_right
apply min_le_left
다음 내용을 연습 문제로 증명해 보시기를 권합니다. 방금 설명한 두 가지 요령 중 어느 쪽을 사용해도 첫 번째 증명을 줄일 수 있습니다.
example : max a b = max b a := by
sorry
example : min (min a b) c = min a (min b c) := by
sorry
물론 max의 결합법칙도 증명해 보셔도 좋습니다.
곱셈이 덧셈에 대해 분배되는 것처럼 min이 max에 대해 분배되고, 그 반대도 성립한다는 것은 흥미로운 사실입니다. 다시 말해, 실수에서는 min a (max b c) = max (min a b) (min a c)라는 항등식이 성립하며, max와 min을 서로 바꾼 대응 버전도 성립합니다. 그러나 다음 절에서 이것이 ≤의 추이성과 반사성, 그리고 위에서 열거한 min과 max의 특성 성질로부터 도출되지 않는다는 것을 보게 될 것입니다. 실수에서 ≤가 전순서라는 사실, 즉 ∀ x y, x ≤ y ∨ y ≤ x를 만족한다는 사실을 사용해야 합니다. 여기서 논리합 기호 ∨는 “또는”을 나타냅니다. 첫 번째 경우에는 min x y = x이고, 두 번째 경우에는 min x y = y입니다. 경우를 나누어 추론하는 방법은 제 3.5 절에서 배우겠지만, 지금은 경우 분할이 필요 없는 예제만 다루겠습니다.
다음은 그러한 예제 중 하나입니다.
theorem aux : min a b + c ≤ min (a + c) (b + c) := by
sorry
example : min a b + c = min (a + c) (b + c) := by
sorry
aux가 등식을 증명하는 데 필요한 두 부등식 중 하나를 제공한다는 것은 분명하지만, 이를 적절한 값에 적용하면 반대 방향의 부등식도 얻을 수 있습니다. 힌트를 드리자면, add_neg_cancel_right 정리와 linarith 택틱을 사용할 수 있습니다.
Lean의 명명 규칙은 라이브러리에서 삼각 부등식에 붙인 이름에서 잘 드러납니다:
#check (abs_add_le : ∀ a b : ℝ, |a + b| ≤ |a| + |b|)
이를 사용하고 add_sub_cancel_right도 함께 사용하여 다음 변형을 증명하십시오:
example : |a| - |b| ≤ |a - b| :=
sorry
end
이것을 세 줄 이하로 할 수 있는지 시도해 보십시오. sub_add_cancel 정리를 사용할 수 있습니다.
이어지는 절들에서 사용할 또 다른 중요한 관계는 자연수에 대한 나누어떨어짐 관계인 x ∣ y입니다. 주의하십시오: 나누어떨어짐 기호는 키보드에 있는 일반적인 세로 막대가 아닙니다. 그 대신 VS Code에서 \|를 입력하면 얻을 수 있는 유니코드 문자입니다. 관례에 따라 Mathlib에서는 정리 이름에서 이를 가리킬 때 dvd를 사용합니다.
example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z :=
dvd_trans h₀ h₁
example : x ∣ y * x * z := by
apply dvd_mul_of_dvd_left
apply dvd_mul_left
example : x ∣ x ^ 2 := by
apply dvd_mul_left
마지막 예제에서 지수는 자연수이며, dvd_mul_left를 적용하면 Lean이 x^2의 정의를 x^1 * x로 전개하게 됩니다. 다음을 증명하는 데 필요한 정리들의 이름을 추측할 수 있는지 시도해 보십시오:
example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
sorry
end
나누어떨어짐 관계에서 최대공약수 gcd와 최소공배수 lcm은 각각 min과 max에 대응합니다. 모든 수는 0을 나누므로, 나누어떨어짐 관계에서는 실제로 0이 가장 큰 원소입니다:
variable (m n : ℕ)
#check (Nat.gcd_zero_right n : Nat.gcd n 0 = n)
#check (Nat.gcd_zero_left n : Nat.gcd 0 n = n)
#check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0)
#check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0)
다음을 증명하는 데 필요한 정리들의 이름을 추측할 수 있는지 시도해 보십시오:
example : Nat.gcd m n = Nat.gcd n m := by
sorry
힌트: dvd_antisymm을 사용할 수 있지만, 그렇게 하면 Lean은 이 표현식이 일반적인 정리와 자연수 전용 버전인 Nat.dvd_antisymm 사이에서 모호하다고 불평할 것입니다. 일반적인 정리를 지정하려면 _root_.dvd_antisymm을 사용하면 됩니다. 어느 쪽을 사용해도 동작합니다.
2.5. 대수적 구조에 관한 사실 증명하기
제 2.2 절에서 우리는 실수를 지배하는 여러 일반적인 항등식이 가환환과 같은 더 일반적인 대수적 구조의 클래스에서도 성립함을 보았습니다. 대수적 구조를 기술할 때는 등식뿐만 아니라 원하는 어떤 공리든 사용할 수 있습니다. 예를 들어, 부분 순서는 반사적이고 추이적이며 반대칭적인 이항 관계를 갖춘 집합으로 이루어집니다. 실수에서의 ≤와 같은 관계입니다. Lean은 부분 순서에 대해 알고 있습니다:
variable {α : Type*} [PartialOrder α]
variable (x y z : α)
#check x ≤ y
#check (le_refl x : x ≤ x)
#check (le_trans : x ≤ y → y ≤ z → x ≤ z)
#check (le_antisymm : x ≤ y → y ≤ x → x = y)
여기서는 임의의 타입에 α, β, γ와 같은 문자(\a, \b, \g로 입력합니다)를 사용하는 Mathlib의 관례를 따릅니다. 라이브러리에서는 환과 군 같은 대수적 구조의 바탕 집합에 각각 R과 G 같은 문자를 흔히 사용하지만, 일반적으로 타입에는 그리스 문자를 사용하며, 특히 연관된 구조가 거의 없거나 전혀 없을 때 그렇습니다.
임의의 부분 순서 ≤에는 엄격한 부분 순서 <도 연관되어 있으며, 이는 실수에서의 <와 어느 정도 비슷하게 동작합니다. 이 순서에서 x가 y보다 작다고 말하는 것은 x가 y보다 작거나 같고 y와 같지 않다고 말하는 것과 동치입니다.
#check x < y
#check (lt_irrefl x : ¬ (x < x))
#check (lt_trans : x < y → y < z → x < z)
#check (lt_of_le_of_lt : x ≤ y → y < z → x < z)
#check (lt_of_lt_of_le : x < y → y ≤ z → x < z)
example : x < y ↔ x ≤ y ∧ x ≠ y :=
lt_iff_le_and_ne
이 예제에서 기호 ∧는 “그리고(and)”를, 기호 ¬는 “아니다(not)”를 나타내며, x ≠ y는 ¬ (x = y)의 약어입니다. Chapter 3에서는 이러한 논리 연결사를 사용하여 <가 앞서 제시한 성질을 가짐을 증명하는 방법을 배우게 됩니다.
격자는 부분 순서에 실수에서의 min, max와 유사한 연산 ⊓, ⊔를 더하여 확장한 구조입니다:
variable {α : Type*} [Lattice α]
variable (x y z : α)
#check x ⊓ y
#check (inf_le_left : x ⊓ y ≤ x)
#check (inf_le_right : x ⊓ y ≤ y)
#check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)
#check x ⊔ y
#check (le_sup_left : x ≤ x ⊔ y)
#check (le_sup_right : y ≤ x ⊔ y)
#check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z)
⊓와 ⊔의 이러한 특성을 보면 이들을 각각 최대 하계와 최소 상계라고 부르는 것이 타당합니다. VS Code에서는 \glb와 \lub를 사용하여 이 기호들을 입력할 수 있습니다. 이 기호들은 흔히 하한(infimum)과 상한(supremum)이라고도 불리며, Mathlib은 정리 이름에서 이들을 inf와 sup으로 지칭합니다. 설상가상으로, 이들은 흔히 meet과 join이라고도 불립니다. 따라서 격자를 다룰 때에는 다음 용어 대응을 염두에 두어야 합니다.
⊓는 최대 하계, 하한, 또는 meet입니다.⊔는 최소 상계, 상한, 또는 join입니다.
격자의 몇 가지 예는 다음과 같습니다.
≤가 주어진 정수나 실수와 같은 임의의 전순서 위의min과max순서
⊆가 주어진, 어떤 정의역의 부분집합들의 모임 위의∩와∪x가 거짓이거나y가 참일 때x ≤ y인 순서가 주어진, 불리언 진릿값 위의∧와∨나누어떨어짐 순서
∣가 주어진, 자연수(또는 양의 자연수) 위의gcd와lcm벡터 공간의 선형 부분공간들의 모임으로, 최대 하계는 교집합으로 주어지고, 최소 상계는 두 공간의 합으로 주어지며, 순서는 포함 관계입니다.
집합(또는 Lean에서는 타입) 위의 위상들의 모임으로, 두 위상의 최대 하계는 두 위상의 합집합으로 생성되는 위상이고, 최소 상계는 두 위상의 교집합이며, 순서는 역포함 관계입니다.
min / max 및 gcd / lcm의 경우와 마찬가지로, 하한과 상한의 교환법칙과 결합법칙을 이들을 특징짓는 공리와 le_refl, le_trans만으로 증명할 수 있음을 확인할 수 있습니다.
x ≤ z 형태의 목표를 보았을 때 apply le_trans를 사용하는 것은 좋은 생각이 아닙니다. 실제로 Lean은 우리가 어떤 중간 원소 y를 사용하려는지 추측할 방법이 없습니다. 따라서 apply le_trans는 x ≤ ?a, ?a ≤ z, α와 같은 세 개의 목표를 만들어 내며, 여기서 ?a(아마도 더 복잡한 자동 생성 이름으로 나타날 것입니다)는 정체를 알 수 없는 y를 나타냅니다. 타입이 α인 마지막 목표는 y의 값을 제공하는 것입니다. 이 목표가 마지막에 오는 이유는 Lean이 첫 번째 목표 x ≤ ?a의 증명으로부터 이 값을 자동으로 추론하기를 기대하기 때문입니다. 이러한 달갑지 않은 상황을 피하려면 calc 택틱을 사용하여 y를 명시적으로 제공할 수 있습니다. 또는 y를 인수로 받아 기대한 대로 x ≤ y와 y ≤ z 목표를 만들어 내는 trans 택틱을 사용할 수도 있습니다. 물론 exact le_trans inf_le_left inf_le_right와 같은 완전한 증명을 직접 제공하여 이 문제를 피할 수도 있지만, 이 방법은 훨씬 더 많은 사전 계획을 필요로 합니다.
example : x ⊓ y = y ⊓ x := by
sorry
example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := by
sorry
example : x ⊔ y = y ⊔ x := by
sorry
example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := by
sorry
이 정리들은 Mathlib에서 각각 inf_comm, inf_assoc, sup_comm, sup_assoc이라는 이름으로 찾을 수 있습니다.
또 다른 좋은 연습 문제는 이 공리들만 사용하여 흡수 법칙을 증명하는 것입니다:
theorem absorb1 : x ⊓ (x ⊔ y) = x := by
sorry
theorem absorb2 : x ⊔ x ⊓ y = x := by
sorry
이들은 Mathlib에서 inf_sup_self와 sup_inf_self라는 이름으로 찾을 수 있습니다.
추가 항등식 x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)와 x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)를 만족하는 격자를 분배 격자라고 합니다. Lean도 이것들을 알고 있습니다:
variable {α : Type*} [DistribLattice α]
variable (x y z : α)
#check (inf_sup_left x y z : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z)
#check (inf_sup_right x y z : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
#check (sup_inf_left x y z : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
#check (sup_inf_right x y z : x ⊓ y ⊔ z = (x ⊔ z) ⊓ (y ⊔ z))
⊓와 ⊔의 교환법칙을 이용하면 왼쪽 버전과 오른쪽 버전이 동치임을 쉽게 보일 수 있습니다. 원소가 유한 개인 비분배 격자를 명시적으로 기술하여 모든 격자가 분배적인 것은 아님을 보이는 것도 좋은 연습 문제입니다. 임의의 격자에서 두 분배 법칙 중 어느 하나가 다른 하나를 함의함을 보이는 것 또한 좋은 연습 문제입니다:
variable {α : Type*} [Lattice α]
variable (a b c : α)
example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) := by
sorry
example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
sorry
공리적 구조들을 결합하여 더 큰 구조를 만들 수 있습니다. 예를 들어 강순서환은 환과 그 바탕 집합 위의 부분 순서로 이루어지며, 이 부분 순서는 환 연산이 순서와 호환됨을 나타내는 추가 공리를 만족합니다:
variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
variable (a b c : R)
#check (add_le_add_right : a ≤ b → ∀ c, c + a ≤ c + b)
#check (mul_pos : 0 < a → 0 < b → 0 < a * b)
Chapter 3에서는 mul_pos와 <의 정의로부터 다음을 유도하는 방법을 제공할 것입니다:
#check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b)
그다음에는 실수의 산술과 순서에 관해 추론할 때 사용하는 여러 일반적인 사실이 임의의 순서환에서 일반적으로 성립함을 보이는 것이 확장된 연습 문제입니다. 다음은 환과 부분 순서의 성질, 그리고 앞의 두 예제에서 나열한 사실만을 사용하여 시도해 볼 수 있는 몇 가지 예제입니다(이 환들은 가환이라고 가정하지 않으므로 ring 택틱을 사용할 수 없다는 점에 주의하십시오):
example (h : a ≤ b) : 0 ≤ b - a := by
sorry
example (h: 0 ≤ b - a) : a ≤ b := by
sorry
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
sorry
마지막으로, 예제를 하나 더 살펴보겠습니다. 거리 공간은 임의의 두 원소 쌍을 실수에 대응시키는 거리 개념 dist x y가 주어진 집합으로 이루어집니다. 거리 함수는 다음 공리들을 만족한다고 가정합니다:
variable {X : Type*} [MetricSpace X]
variable (x y z : X)
#check (dist_self x : dist x x = 0)
#check (dist_comm x y : dist x y = dist y x)
#check (dist_triangle x y z : dist x z ≤ dist x y + dist y z)
이 절을 익혔다면, 이 공리들로부터 거리가 항상 음이 아니라는 사실이 따라 나옴을 보일 수 있습니다:
example (x y : X) : 0 ≤ dist x y := by
sorry
짐작하셨겠지만, 이 정리는 Mathlib에서 dist_nonneg라고 불립니다.