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이라 하고, 지역 문맥과 대상을 합친 것을 goal(목표)이라 부르기도 합니다. 실제로는 의도한 의미가 대체로 명확합니다.
이 항등식들을 증명해 보십시오. 각각의 경우 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
대괄호 안에 관련 항등식들을 쉼표로 구분하여 나열하면, 여러 재작성 명령을 하나의 명령으로 수행할 수 있습니다.
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]
재작성 목록에서 쉼표 뒤에 커서를 놓으면 여전히 점진적인 진행 상황을 볼 수 있습니다.
또 다른 요령은 example이나 정리 밖에서 변수를 한 번에 선언해 두는 것입니다. 그러면 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라는 사실의 증명이라고 생각할 수 있습니다. 하지만 a, b, c를 명시적으로 적는 것은 중복임에 주목하십시오. 가설 h만으로도 우리가 염두에 둔 대상이 무엇인지 분명해지기 때문입니다. 이 경우에는 몇 글자 더 입력하는 것이 그리 부담스럽지 않지만, 더 복잡한 식에 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. 정리와 보조정리 사용하기
재작성(rewriting)은 방정식을 증명하는 데는 훌륭하지만, 다른 종류의 정리는 어떻습니까? 예를 들어, \(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)
le_trans의 명제에 있는 암묵적 괄호는 오른쪽으로 결합하며, 이는 제 3.1 절에서 더 자세히 설명하는 바와 같이 a ≤ b → (b ≤ c → a ≤ c)로 해석해야 함을 의미합니다. 라이브러리 설계자들은 le_trans의 인자 a, b, c를 암시적으로 설정해 두었으므로, Lean은 (나중에 논의할 것처럼 정말로 고집하지 않는 한) 여러분이 그것들을 명시적으로 제공하도록 허용하지 않습니다. 대신, 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같은 일부 정리는 “~일 필요충분조건”이라는 어구를 나타내는 쌍조건을 사용합니다. (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 문서를 사용할 수 있습니다.
패턴으로 Lean과 Mathlib의 정의와 정리를 검색하려면 Loogle <https://loogle.lean-lang.org>을 사용할 수 있습니다.
에디터에서 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의 이름을 따서 커링이라고 합니다.
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를 사용하는 반면, 두 번째 것은 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보다 작다고 말하는 것은 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
이 예시에서 기호 ∧는 “그리고”를 나타내고, 기호 ¬는 “아님”을 나타내며, 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를 사용하여 이들을 입력할 수 있습니다. 이 기호들은 종종 하한과 상한으로도 불리며, Mathlib에서는 정리 이름에서 이들을 inf와 sup로 표기합니다. 문제를 더 복잡하게 하자면, 이들은 종종 meet과 join으로도 불립니다. 따라서 격자를 다룰 때는 다음 대응표를 염두에 두어야 합니다:
⊓는 최대 하한, 하한, 또는 meet입니다.⊔는 최소 상한, 상한, 또는 join입니다.
격자의 몇 가지 예로는 다음이 있습니다:
≤를 갖는 정수나 실수와 같은 임의의 전순서에서의min과max어떤 정의역의 부분집합들의 모임에서 순서
⊆를 갖는∩와∪x가 거짓이거나y가 참이면x ≤ y라는 순서를 갖는 불(boolean) 진리값에서의∧와∨나눗셈 순서
∣를 갖는 자연수(또는 양의 자연수)에서의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)
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라고 불립니다.