3. 논리

지난 장에서는 등식, 부등식, 그리고 “\(x\)가 \(y\)를 나눈다”와 같은 기본적인 수학적 명제를 다루었습니다. 복잡한 수학적 명제는 이러한 단순한 명제들로부터 “그리고”, “또는”, “아니다”, “만약 … 이면”, “모든”, “어떤”과 같은 논리적 용어를 사용하여 구성됩니다. 이 장에서는 이렇게 구성된 명제를 다루는 방법을 보여드립니다.

3.1. 함의와 전칭 기호

#check 다음에 나오는 명제를 살펴보십시오:

#check ∀ x : ℝ, 0 ≤ x → |x| = x

말로 표현하면 “모든 실수 x에 대해 0 ≤ x이면 x의 절댓값은 x와 같습니다”라고 할 수 있습니다. 다음과 같이 더 복잡한 명제도 가능합니다:

#check ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε

말로 풀어보면 “모든 x, y, ε에 대해, 0 < ε ≤ 1이고 x의 절댓값이 ε보다 작고 y의 절댓값이 ε보다 작으면, x * y의 절댓값은 ε보다 작습니다.”라고 할 수 있습니다. Lean에서 함의의 수열에는 오른쪽으로 묶이는 암묵적 괄호가 있습니다. 따라서 위 식은 “0 < ε이면, ε ≤ 1이면, |x| < ε이면 …”을 의미합니다. 결과적으로 이 식은 모든 가정이 함께 결론을 함의한다는 것을 말합니다.

이 명제에서 전칭 기호는 대상 전체에 걸쳐 있고 함의 화살표는 가정을 도입하지만, Lean은 이 둘을 매우 비슷하게 다룬다는 것을 이미 보았습니다. 특히 그러한 형태의 정리를 증명했다면, 대상과 가정 모두에 같은 방식으로 그 정리를 적용할 수 있습니다. 잠시 후 증명하는 것을 도와드릴 다음 명제를 예시로 사용하겠습니다:

theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)

#check my_lemma a b δ
#check my_lemma a b δ h₀ h₁
#check my_lemma a b δ h₀ h₁ ha hb

end

또한 한정된 변수가 이후의 가정으로부터 추론될 수 있을 때, Lean에서는 중괄호를 사용해 이를 암묵적으로 만드는 것이 흔하다는 것도 이미 보았습니다. 그렇게 하면 대상을 언급하지 않고도 가정에 보조정리를 적용할 수 있습니다.

theorem my_lemma2 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
  sorry

section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)

#check my_lemma2 h₀ h₁ ha hb

end

이 시점에서, apply 택틱을 사용해 |a * b| < δ 형태의 목표에 my_lemma를 적용하면, 각 가정을 증명해야 하는 새로운 목표들이 남는다는 것도 알고 있습니다.

이러한 명제를 증명하려면 intro 택틱을 사용합니다. 이 예제에서 이것이 무엇을 하는지 살펴보십시오.

theorem my_lemma3 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  sorry

전칭 한정된 변수에는 원하는 이름을 자유롭게 사용할 수 있으며, 반드시 x, y, ε일 필요는 없습니다. 변수가 암묵적으로 표시되어 있더라도 이를 도입해야 한다는 점에 유의하십시오. 변수를 암묵적으로 만든다는 것은 my_lemma를 사용하는 표현식을 작성할 때 이를 생략한다는 의미이지만, 그럼에도 이들은 우리가 증명하고 있는 명제의 필수적인 부분입니다. intro 명령 이후의 목표는, 지난 절에서 했던 것처럼 모든 변수와 가정을 콜론 앞에 나열했다면 처음에 있었을 목표와 같습니다. 잠시 후, 증명이 시작된 뒤에 변수와 가정을 도입해야 하는 경우가 왜 생기는지 살펴보겠습니다.

보조정리 증명을 돕기 위해 시작 부분을 제공하겠습니다.

theorem my_lemma4 :
    ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  calc
    |x * y| = |x| * |y| := sorry
    _ ≤ |x| * ε := sorry
    _ < 1 * ε := sorry
    _ = ε := sorry

abs_mul, mul_le_mul, abs_nonneg, mul_lt_mul_of_pos_right, one_mul 정리를 사용하여 증명을 완성하십시오. Ctrl-스페이스 자동완성(맥에서는 Cmd-스페이스 자동완성)을 사용하면 이러한 정리들을 찾을 수 있다는 점을 기억하십시오. 또한 필요충분조건 명제의 두 방향을 추출하는 데 .mp와 .mpr, 또는 .1과 .2를 사용할 수 있다는 점도 기억하십시오.

전칭 기호는 정의 안에 숨겨져 있는 경우가 많으며, Lean은 필요할 때 정의를 펼쳐서 이를 드러냅니다. 예를 들어, 두 술어 FnUb f a와 FnLb f a를 정의해 봅시다. 여기서 f는 실수에서 실수로 가는 함수이고 a는 실수입니다. 첫 번째는 a가 f의 값들의 상계임을 말하고, 두 번째는 a가 f의 값들의 하계임을 말합니다.

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

다음 예제에서 fun x ↦ f x + g x는 x를 f x + g x로 대응시키는 함수입니다. 식 f x + g x에서 이 함수로 넘어가는 것을 타입 이론에서는 람다 추상화라고 부릅니다.

example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by
  intro x
  dsimp
  apply add_le_add
  apply hfa
  apply hgb

목표 FnUb (fun x ↦ f x + g x) (a + b)에 intro를 적용하면 Lean은 FnUb의 정의를 펼치고 전칭 기호에 대해 x를 도입할 수밖에 없습니다. 그러면 목표는 (fun (x : ℝ) ↦ f x + g x) x ≤ a + b가 됩니다. 하지만 (fun x ↦ f x + g x)를 x에 적용하면 f x + g x가 나와야 하며, dsimp 명령이 바로 그 단순화를 수행합니다. (“d”는 “definitional(정의적)”을 뜻합니다.) 이 명령을 삭제해도 증명은 여전히 작동합니다. 다음 apply를 이해하려면 Lean이 어차피 그 축약을 수행해야 하기 때문입니다. dsimp 명령은 단순히 목표를 더 읽기 쉽게 만들어 주고 다음에 무엇을 할지 파악하는 데 도움을 줍니다. 다른 방법은 change f x + g x ≤ a + b라고 작성하여 change 택틱을 사용하는 것입니다. 이는 증명을 더 읽기 쉽게 만들어 주고, 목표가 어떻게 변환되는지에 대해 더 많은 제어권을 제공합니다.

증명의 나머지 부분은 일상적입니다. 마지막 두 apply 명령은 Lean이 가설에 있는 FnUb의 정의를 펼치도록 강제합니다. 이것들에 대해 비슷한 증명을 수행해 보십시오:

example (hfa : FnLb f a) (hgb : FnLb g b) : FnLb (fun x ↦ f x + g x) (a + b) :=
  sorry

example (nnf : FnLb f 0) (nng : FnLb g 0) : FnLb (fun x ↦ f x * g x) 0 :=
  sorry

example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
    FnUb (fun x ↦ f x * g x) (a * b) :=
  sorry

실수에서 실수로 가는 함수에 대해 FnUb와 FnLb를 정의했지만, 이 정의와 증명이 훨씬 더 일반적이라는 것을 알아두어야 합니다. 이 정의는 공역에 순서 개념이 있는 임의의 두 타입 사이의 함수에 대해 의미가 있습니다. 정리 add_le_add의 타입을 확인해 보면, 이것이 관련 순서를 존중하는 임의의 모노이드 구조에 대해 성립함을 알 수 있습니다. 그것이 정확히 무엇을 의미하는지에 대한 세부 사항은 지금은 중요하지 않지만, 자연수, 정수, 유리수, 실수가 모두 그 예시라는 것은 알아둘 가치가 있습니다. 따라서 정리 fnUb_add를 그러한 일반성 수준에서 증명한다면, 이 모든 예시에 적용될 것입니다.

variable {α : Type*} {R : Type*} [AddCommMonoid R] [PartialOrder R] [IsOrderedCancelAddMonoid R]

#check add_le_add

def FnUb' (f : α → R) (a : R) : Prop :=
  ∀ x, f x ≤ a

theorem fnUb_add {f g : α → R} {a b : R} (hfa : FnUb' f a) (hgb : FnUb' g b) :
    FnUb' (fun x ↦ f x + g x) (a + b) := fun x ↦ add_le_add (hfa x) (hgb x)

이런 대괄호는 제 2.2 절 절에서 이미 본 적이 있지만, 아직 그 의미를 설명하지는 않았습니다. 구체성을 위해 대부분의 예시에서 실수만 다루겠지만, Mathlib이 높은 수준의 일반성에서 작동하는 정의와 정리를 포함하고 있다는 것은 알아둘 가치가 있습니다.

숨겨진 전칭 기호의 또 다른 예로, Mathlib은 함수가 그 인자에 대해 비감소함을 나타내는 술어 Monotone을 정의합니다:

example (f : ℝ → ℝ) (h : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b :=
  @h

속성 Monotone f는 콜론 뒤의 식과 정확히 같도록 정의됩니다. h 앞에 @ 기호를 붙여야 하는데, 그렇게 하지 않으면 Lean이 h에 대한 암묵적 인자를 펼쳐서 자리표시자를 삽입하기 때문입니다.

단조성에 대한 명제를 증명하는 것은 intro를 사용하여 두 변수, 예를 들어 a와 b, 그리고 가정 a ≤ b를 도입하는 과정을 포함합니다. 단조성 가정을 사용하려면, 적절한 인자와 가정에 그것을 적용한 다음, 그 결과로 나온 식을 목표에 적용하면 됩니다. 또는 그것을 목표에 적용하여, Lean이 남은 가정들을 새로운 하위 목표로 표시함으로써 거꾸로 작업하는 것을 돕게 할 수도 있습니다.

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by
  intro a b aleb
  apply add_le_add
  apply mf aleb
  apply mg aleb

증명이 이렇게 짧을 때는, 대신 증명 항을 제시하는 것이 흔히 더 편리합니다. 객체 a와 b, 그리고 가정 aleb를 일시적으로 도입하는 증명을 기술하기 위해, Lean은 fun a b aleb ↦ ... 표기법을 사용합니다. 이는 fun x ↦ x^2와 같은 식이 객체 x에 일시적으로 이름을 붙인 다음, 그것을 사용하여 값을 기술함으로써 함수를 기술하는 방식과 유사합니다. 따라서 이전 증명의 intro 명령은 다음 증명 항의 람다 추상화에 대응합니다. 그러면 apply 명령들은 정리를 그 인자들에 적용하는 것을 구성하는 것에 대응합니다.

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x :=
  fun _a _b aleb ↦ add_le_add (mf aleb) (mg aleb)

여기 유용한 요령이 하나 있습니다: 식의 나머지 부분이 들어갈 자리에 밑줄을 사용하여 증명 항 fun a b aleb ↦ _를 작성하기 시작하면, Lean은 그 식의 값을 추측할 수 없음을 나타내는 오류를 표시합니다. VS Code에서 Lean InfoView 창을 확인하거나 물결선 오류 표시 위에 마우스를 올리면, Lean은 남은 식이 풀어야 할 목표를 보여줍니다.

Lean이 위 증명에 대해 a와 b가 함수 본문에서 사용되지 않는다는 경고를 출력하는 것을 확인하실 수 있습니다. 이는 정리에서 불필요한 가정을 두지 않도록 하는 데 유용한 일반적인 메커니즘입니다. 여기서는 딱히 유용한 정보를 알려주지 않습니다. set_option linter.unusedVariables false를 작성하여 현재 절이 끝날 때까지 이 경고를 비활성화하거나, 예제 위에 set_option linter.unusedVariables false in을 작성하여 해당 예제에서만 비활성화할 수 있습니다.

또한 a와 b를 밑줄로 바꾸어 Lean에게 이름을 붙이고 싶지 않다고 알릴 수도 있습니다. 그러면 Lean은 x✝와 같이 자동 생성된 접근 불가능한 이름을 사용합니다. 또는 이름 앞에 밑줄을 붙여 Lean에게 그 이름을 사용할 의도가 없음을 알릴 수 있습니다.

택틱이나 증명 항 중 하나를 사용하여 다음 예제들을 증명해 보십시오.

example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
  sorry

example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) :=
  sorry

여기 예제를 몇 가지 더 소개합니다. 실수 \(\Bbb R\)에서 실수 \(\Bbb R\)로 가는 함수 \(f\)는 모든 \(x\)에 대해 \(f(-x) = f(x)\)이면 짝함수라 하고, 모든 \(x\)에 대해 \(f(-x) = -f(x)\)이면 홀함수라 합니다. 다음 예제는 이 두 개념을 형식적으로 정의하고 그중 한 가지 사실을 증명합니다. 나머지 증명은 직접 완성하실 수 있습니다.

def FnEven (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

def FnOdd (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = -f (-x)

example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
  intro x
  calc
    (fun x ↦ f x + g x) x = f x + g x := rfl
    _ = f (-x) + g (-x) := by rw [ef, eg]


example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
  sorry

example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
  sorry

첫 번째 증명은 람다 추상화를 제거하기 위해 dsimp나 change를 사용하여 줄일 수 있습니다. 하지만 람다 추상화를 명시적으로 제거하지 않으면 이어지는 rw가 작동하지 않는다는 것을 확인할 수 있는데, 그렇지 않으면 식에서 패턴 f x와 g x를 찾을 수 없기 때문입니다. 다른 일부 택틱과 달리, rw는 구문적 수준에서 작동하므로, 정의를 펼치거나 축약을 적용해 주지 않습니다(이 방향으로 조금 더 애쓰는 erw라는 변형이 있지만, 그다지 많이 애쓰지는 않습니다).

암묵적 전칭 기호를 알아보는 법을 알고 나면, 곳곳에서 그것을 찾을 수 있습니다.

Mathlib은 집합을 다루기 위한 훌륭한 라이브러리를 포함하고 있습니다. Lean은 집합론에 기초한 토대를 사용하지 않는다는 점을 상기하십시오. 따라서 여기서 “집합”이라는 단어는 주어진 어떤 타입 α의 수학적 대상들의 모음이라는 평범한 의미를 갖습니다. x가 타입 α를 갖고 s가 타입 Set α를 가지면, x ∈ s는 x가 s의 원소임을 주장하는 명제입니다. y가 어떤 다른 타입 β를 가지면 표현식 y ∈ s는 무의미합니다. 여기서 “무의미하다”는 “타입을 갖지 않으므로 Lean이 이를 잘 형성된 명제문으로 받아들이지 않는다”는 의미입니다. 이는 예를 들어 체르멜로-프렝켈 집합론과 대조되는데, 그곳에서는 a ∈ b가 두 수학적 대상 a와 b에 대해 잘 형성된 명제문입니다. 예를 들어 sin ∈ cos는 ZF에서 잘 형성된 명제문입니다. 집합론적 토대의 이러한 결함은, 무의미한 표현식을 탐지함으로써 우리를 돕도록 만들어진 증명 보조기에서 이를 사용하지 않는 중요한 동기입니다. Lean에서 sin은 타입 ℝ → ℝ를 갖고 cos는 타입 ℝ → ℝ를 갖는데, 이는 정의를 펼친 후에도 Set (ℝ → ℝ)와 같지 않으므로, sin ∈ cos라는 명제문은 무의미합니다. Lean을 사용하여 집합론 자체를 다룰 수도 있습니다. 예를 들어 체르멜로-프렝켈 공리로부터의 연속체 가설의 독립성이 Lean에서 형식화되었습니다. 하지만 그러한 집합론의 메타이론은 이 책의 범위를 완전히 벗어납니다.

s와 t가 Set α 타입이라면, 부분집합 관계 s ⊆ t는 ∀ {x : α}, x ∈ s → x ∈ t를 의미하는 것으로 정의됩니다. 한정자 안의 변수는 암묵적으로 표시되어 있어서, h : s ⊆ t와 h' : x ∈ s가 주어지면 x ∈ t에 대한 근거로 h h'를 쓸 수 있습니다. 다음 예제는 부분집합 관계의 반사성을 증명하는 택틱 증명과 증명항을 제공하며, 추이성에 대해서도 같은 것을 해볼 것을 요청합니다.

variable {α : Type*} (r s t : Set α)

example : s ⊆ s := by
  intro x xs
  exact xs

theorem Subset.refl : s ⊆ s := fun _x xs ↦ xs

theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
  sorry

함수에 대해 FnUb를 정의했던 것처럼, a가 집합 s의 상계임을 의미하는 SetUb s a를 정의할 수 있는데, 이때 s는 순서가 연관된 어떤 타입의 원소들의 집합이라고 가정합니다. 다음 예제에서는 a가 s의 상계이고 a ≤ b이면 b 역시 s의 상계임을 증명해볼 것을 요청합니다.

variable {α : Type*} [PartialOrder α]
variable (s : Set α) (a b : α)

def SetUb (s : Set α) (a : α) :=
  ∀ x, x ∈ s → x ≤ a

example (h : SetUb s a) (h' : a ≤ b) : SetUb s b :=
  sorry

이 절은 마지막으로 중요한 예제 하나로 마무리하겠습니다. 함수 \(f\)가 모든 \(x_1\)과 \(x_2\)에 대해 \(f(x_1) = f(x_2)\)이면 \(x_1 = x_2\)인 경우 단사라고 합니다. Mathlib은 x₁과 x₂를 암묵적으로 하여 Function.Injective f를 정의합니다. 다음 예제는 실수에서 상수를 더하는 함수는 어떤 것이든 단사임을 보여줍니다. 이어서 0이 아닌 상수를 곱하는 것 역시 단사임을 보여줄 것을 요청하며, 예제에 나온 보조정리 이름을 영감의 원천으로 삼으십시오. 보조정리 이름의 앞부분을 추측한 뒤에는 Ctrl-Space 완성 기능을 사용해야 한다는 점을 기억하십시오.

open Function

example (c : ℝ) : Injective fun x ↦ x + c := by
  intro x₁ x₂ h'
  exact (add_left_inj c).mp h'

example {c : ℝ} (h : c ≠ 0) : Injective fun x ↦ c * x := by
  sorry

마지막으로, 두 단사 함수의 합성이 단사임을 보이십시오:

variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}

example (injg : Injective g) (injf : Injective f) : Injective fun x ↦ g (f x) := by
  sorry

3.2. 존재 한정사

VS Code에서 \ex로 입력할 수 있는 존재 한정사는 “존재한다”라는 문구를 나타내는 데 사용됩니다. Lean에서 형식적 표현 ∃ x : ℝ, 2 < x ∧ x < 3는 2와 3 사이에 실수가 있다는 것을 말합니다. (논리곱 기호 ∧에 대해서는 제 3.4 절에서 다루겠습니다.) 이러한 명제를 증명하는 정석적인 방법은 실수를 하나 제시하고 그것이 명시된 성질을 가짐을 보이는 것입니다. 숫자 2.5는, Lean이 문맥에서 우리가 실수를 염두에 두고 있음을 추론할 수 없을 때 5 / 2 또는 (5 : ℝ) / 2로 입력할 수 있는데, 요구된 성질을 가지며, norm_num 택틱이 그것이 설명에 부합함을 증명할 수 있습니다.

이 정보를 조합하는 방법에는 몇 가지가 있습니다. 존재 한정사로 시작하는 목표가 주어지면, use 택틱을 사용하여 대상을 제시할 수 있으며, 이후 그 성질을 증명하는 목표가 남습니다.

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  use 5 / 2
  norm_num

use 택틱에는 데이터뿐 아니라 증명도 줄 수 있습니다:

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h1 : 2 < (5 : ℝ) / 2 := by norm_num
  have h2 : (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2, h1, h2

실제로 use 택틱은 사용 가능한 가정도 자동으로 사용해 보려고 시도합니다.

example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  use 5 / 2

대안으로, Lean의 익명 생성자 표기법을 사용하여 존재 한정사의 증명을 구성할 수 있습니다.

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
  ⟨5 / 2, h⟩

여기에는 by가 없다는 점에 유의하십시오. 여기서는 명시적인 증명 항을 제시하고 있습니다. 각각 \<와 \>로 입력할 수 있는 왼쪽 및 오른쪽 꺾쇠괄호는, 현재 목표에 적합한 구성이 무엇이든 그것을 사용하여 주어진 데이터를 조합하라고 Lean에 지시합니다. 먼저 택틱 모드로 들어가지 않고도 이 표기법을 사용할 수 있습니다:

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
  ⟨5 / 2, by norm_num⟩

이제 우리는 exists 문을 어떻게 증명하는지 알게 되었습니다. 하지만 그것을 어떻게 사용합니까? 특정 속성을 가진 객체가 존재한다는 것을 안다면, 우리는 임의의 하나에 이름을 붙이고 그것에 대해 추론할 수 있어야 합니다. 예를 들어, 지난 절의 술어 FnUb f a와 FnLb f a를 기억해 보십시오. 이들은 각각 a가 f의 상한 또는 하한임을 나타냅니다. 존재 한정사를 사용하면 상계를 구체적으로 명시하지 않고도 “f가 유계이다”라고 말할 수 있습니다:

def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

def FnHasUb (f : ℝ → ℝ) :=
  ∃ a, FnUb f a

def FnHasLb (f : ℝ → ℝ) :=
  ∃ a, FnLb f a

지난 절의 정리 FnUb_add를 사용하여, f와 g가 모두 상계를 가지면 fun x ↦ f x + g x도 상계를 가짐을 증명할 수 있습니다.

variable {f g : ℝ → ℝ}

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  rcases ubf with ⟨a, ubfa⟩
  rcases ubg with ⟨b, ubgb⟩
  use a + b
  apply fnUb_add ubfa ubgb

rcases 택틱은 존재 한정사에 담긴 정보를 풀어냅니다. ⟨a, ubfa⟩처럼 익명 생성자와 동일한 꺾쇠괄호로 작성된 주석은 패턴이라고 하며, 이는 주 논증을 풀어낼 때 우리가 발견하리라 예상하는 정보를 설명합니다. f에 대한 상계가 존재한다는 가설 ubf가 주어지면, rcases ubf with ⟨a, ubfa⟩는 상계에 대한 새로운 변수 a를 지역 문맥에 추가하며, 그것이 주어진 속성을 가진다는 가설 ubfa도 함께 추가합니다. 목표는 변하지 않은 채로 남아 있습니다. 달라진 것은 이제 새로운 객체와 새로운 가설을 사용하여 목표를 증명할 수 있다는 점입니다. 이것은 수학에서 흔히 쓰이는 추론 방법입니다. 즉, 어떤 가설에 의해 존재가 주장되거나 암시되는 객체를 풀어낸 다음, 이를 사용하여 다른 것의 존재를 확립합니다.

이 방법을 사용하여 다음을 증명해 보십시오. fn_ub_add에서 했던 것처럼 지난 절의 예제 중 일부를 이름 붙인 정리로 바꾸면 유용할 수도 있고, 아니면 증명에 직접 인자를 삽입해도 됩니다.

example (lbf : FnHasLb f) (lbg : FnHasLb g) : FnHasLb fun x ↦ f x + g x := by
  sorry

example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
  sorry

rcases의 “r”은 “recursive”(재귀적)를 의미하는데, 이는 중첩된 데이터를 풀어내기 위해 임의로 복잡한 패턴을 사용할 수 있게 해주기 때문입니다. rintro 택틱은 intro와 rcases의 조합입니다:

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
  rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

사실 Lean은 식과 증명 항에서도 패턴 매칭 fun을 지원합니다:

example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x :=
  fun ⟨a, ubfa⟩ ⟨b, ubgb⟩ ↦ ⟨a + b, fnUb_add ubfa ubgb⟩

가설에서 정보를 풀어내는 작업이 매우 중요하기 때문에 Lean과 Mathlib는 이를 수행하는 다양한 방법을 제공합니다. 예를 들어 obtain 택틱은 직관적인 구문을 제공합니다:

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  obtain ⟨a, ubfa⟩ := ubf
  obtain ⟨b, ubgb⟩ := ubg
  exact ⟨a + b, fnUb_add ubfa ubgb⟩

첫 번째 obtain 명령을 ubf의 “내용”을 주어진 패턴과 매칭하여 구성 요소를 이름 붙인 변수에 할당하는 것으로 생각하십시오. rcases와 obtain은 그 인자를 destruct한다고 말합니다.

Lean은 다른 함수형 프로그래밍 언어에서 사용되는 것과 유사한 구문도 지원합니다:

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  cases ubf
  case intro a ubfa =>
    cases ubg
    case intro b ubgb =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  cases ubf
  next a ubfa =>
    cases ubg
    next b ubgb =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
  match ubf, ubg with
    | ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
      exact ⟨a + b, fnUb_add ubfa ubgb⟩

example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x :=
  match ubf, ubg with
    | ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
      ⟨a + b, fnUb_add ubfa ubgb⟩

첫 번째 예제에서 cases ubf뒤에 커서를 놓으면, 이 택틱이 Lean이 intro라고 표시한 단일 목표를 생성한다는 것을 볼 수 있습니다. (선택된 특정 이름은 존재 명제의 증명을 구성하는 공리적 원시 요소의 내부 이름에서 유래합니다.) 그런 다음 case 택틱이 구성 요소들의 이름을 지정합니다. 두 번째 예제도 비슷하지만, case 대신 next를 사용하면 intro를 언급하지 않아도 된다는 점이 다릅니다. 마지막 두 예제에 나오는 match라는 단어는 여기서 하는 작업이 컴퓨터 과학자들이 “패턴 매칭”이라고 부르는 것임을 보여줍니다. 세 번째 증명은 by로 시작하며, 그 뒤에 나오는 택틱 버전의 match는 화살표 오른쪽에 택틱 증명이 오기를 기대한다는 점에 주목하십시오. 마지막 예제는 증명 항입니다: 택틱은 전혀 보이지 않습니다.

이 책의 나머지 부분에서는 존재 한정사를 사용하는 선호되는 방법으로 rcases, rintro, obtain을 계속 사용하겠습니다. 하지만 대안 구문을 살펴보는 것도 나쁠 것 없습니다. 특히 컴퓨터 과학자들과 함께 있게 될 가능성이 있다면 더욱 그렇습니다.

rcases를 사용하는 한 가지 방법을 보여주기 위해, 오래된 수학적 정리를 증명해 보겠습니다: 두 정수 x와 y가 각각 두 제곱수의 합으로 표현될 수 있다면, 그 곱 x * y도 그렇게 표현될 수 있습니다. 사실 이 명제는 정수뿐만 아니라 임의의 가환환에 대해서도 참입니다. 다음 예제에서 rcases는 두 개의 존재 한정사를 한 번에 풀어냅니다. 그런 다음 x * y를 제곱수의 합으로 표현하는 데 필요한 마법의 값들을 목록으로 만들어 use 문에 제공하고, ring을 사용하여 그것들이 작동함을 확인합니다.

variable {α : Type*} [CommRing α]

def SumOfSquares (x : α) :=
  ∃ a b, x = a ^ 2 + b ^ 2

theorem sumOfSquares_mul {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
    SumOfSquares (x * y) := by
  rcases sosx with ⟨a, b, xeq⟩
  rcases sosy with ⟨c, d, yeq⟩
  rw [xeq, yeq]
  use a * c - b * d, a * d + b * c
  ring

이 증명은 큰 통찰을 주지는 않지만, 증명의 동기를 설명하는 한 가지 방법을 소개하겠습니다. 가우스 정수는 \(a\)와 \(b\)가 정수이고 \(i = \sqrt{-1}\)인 \(a + bi\) 형태의 수입니다. 가우스 정수 \(a + bi\)의 노름은 정의상 \(a^2 + b^2\)입니다. 따라서 가우스 정수의 노름은 제곱의 합이며, 임의의 제곱의 합은 이런 방식으로 표현될 수 있습니다. 위 정리는 가우스 정수의 곱의 노름이 각 노름의 곱이라는 사실을 반영합니다. 즉, \(x\)가 \(a + bi\)의 노름이고 \(y\)가 \(c + di\)의 노름이라면, \(xy\)는 \((a + bi) (c + di)\)의 노름입니다. 우리의 난해한 증명은 형식화하기 가장 쉬운 증명이 항상 가장 명료한 증명은 아니라는 사실을 보여줍니다. 이후 제 7.3 절에서는 가우스 정수를 정의하고 이를 이용한 대안적 증명을 제시하겠습니다.

존재 한정자 안의 방정식을 풀어내어 목표의 식을 다시 쓰는 데 사용하는 패턴은 자주 등장하기 때문에, rcases 택틱은 이를 위한 축약형을 제공합니다. 새 식별자 대신 rfl 키워드를 사용하면 rcases가 자동으로 다시 쓰기를 수행합니다(이 방법은 패턴 매칭 람다에는 적용되지 않습니다).

theorem sumOfSquares_mul' {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
    SumOfSquares (x * y) := by
  rcases sosx with ⟨a, b, rfl⟩
  rcases sosy with ⟨c, d, rfl⟩
  use a * c - b * d, a * d + b * c
  ring

전칭 한정자와 마찬가지로, 존재 한정자도 알아보는 방법을 알면 곳곳에 숨어 있는 것을 찾을 수 있습니다. 예를 들어 나누어떨어짐은 암묵적으로 “존재한다”는 명제입니다.

example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
  rcases divab with ⟨d, beq⟩
  rcases divbc with ⟨e, ceq⟩
  rw [ceq, beq]
  use d * e; ring

다시 한번, 이것은 rcases를 rfl과 함께 사용하기 좋은 상황을 제공합니다. 위 증명에서 시도해 보십시오. 꽤 괜찮게 느껴집니다!

그런 다음 다음을 증명해 보십시오:

example (divab : a ∣ b) (divac : a ∣ c) : a ∣ b + c := by
  sorry

또 다른 중요한 예로, 함수 \(f : \alpha \to \beta\)는 공역 \(\beta\)의 모든 \(y\)에 대해, 정의역 \(\alpha\)에 \(f(x) = y\)를 만족하는 \(x\)가 존재하면 전사라고 합니다. 이 명제가 전칭 기호와 존재 기호를 모두 포함한다는 점에 주목하십시오. 이는 다음 예제가 intro와 use를 모두 사용하는 이유를 설명합니다.

example {c : ℝ} : Surjective fun x ↦ x + c := by
  intro y
  use y - c
  dsimp; ring

정리 mul_div_cancel₀을 사용하여 직접 이 예제를 시도해 보십시오.:

example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
  sorry

이 시점에서, 분모를 유용한 방식으로 자주 정리해 주는 field_simp라는 택틱이 있다는 점을 언급할 가치가 있습니다. 이는 ring 택틱과 함께 사용할 수 있습니다.

example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
  field_simp [h]
  ring

다음 예제는 전사성 가정을 적절한 값에 적용하여 사용합니다. 가정뿐만 아니라 임의의 식에도 rcases를 사용할 수 있다는 점에 유의하십시오.

example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
  rcases h 2 with ⟨x, hx⟩
  use x
  rw [hx]
  norm_num

전사 함수의 합성이 전사임을 보이는 데 이러한 방법들을 사용할 수 있는지 확인해 보십시오.

variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}

example (surjg : Surjective g) (surjf : Surjective f) : Surjective fun x ↦ g (f x) := by
  sorry

3.3. 부정

기호 ¬는 부정을 표현하기 위한 것으로, ¬ x < y는 x가 y보다 작지 않다는 것을 나타내고, ¬ x = y (또는 동등하게 x ≠ y)는 x가 y와 같지 않다는 것을 나타내며, ¬ ∃ z, x < z ∧ z < y는 x와 y사이에 엄격하게 놓인 z가 존재하지 않는다는 것을 나타냅니다. Lean에서 표기법 ¬ A는 A → False의 약자이며, 이는 A가 모순을 함의한다는 것을 말하는 것으로 생각할 수 있습니다. 실용적으로 말하면, 이는 여러분이 부정을 다루는 방법에 대해 이미 알고 있는 것이 있다는 것을 의미합니다. 즉, 가설 h : A를 도입하고 False를 증명함으로써 ¬ A를 증명할 수 있으며, h : ¬ A와 h' : A를 가지고 있다면 h를 h'에 적용하면 False가 나옵니다.

예시로, 엄격한 순서에 대한 비반사성 원리 lt_irrefl을 생각해 보면, 이는 모든 a에 대해 ¬ a < a가 성립한다는 것을 나타냅니다. 비대칭성 원리 lt_asymm은 a < b → ¬ b < a가 성립한다는 것을 나타냅니다. lt_asymm이 lt_irrefl로부터 따라 나온다는 것을 보입시다.

example (h : a < b) : ¬b < a := by
  intro h'
  have : a < a := lt_trans h h'
  apply lt_irrefl a this

이 예제는 몇 가지 새로운 요령을 소개합니다. 먼저, 레이블을 제공하지 않고 have를 사용하면, Lean은 이름 this를 사용하여 이를 다시 참조할 수 있는 편리한 방법을 제공합니다. 증명이 매우 짧기 때문에, 명시적인 증명 항을 제공합니다. 그러나 이 증명에서 여러분이 정말로 주목해야 할 것은 False라는 목표를 남기는 intro 택틱의 결과와, a < a의 증명에 lt_irrefl을 적용함으로써 결국 False를 증명한다는 사실입니다.

여기 또 다른 예제가 있는데, 이는 이전 절에서 정의한 술어 FnHasUb를 사용하며, 이는 함수가 상계를 가진다는 것을 나타냅니다.

example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
  intro fnub
  rcases fnub with ⟨a, fnuba⟩
  rcases h a with ⟨x, hx⟩
  have : f x ≤ a := fnuba x
  linarith

목표가 지역 문맥에 있는 선형 방정식과 부등식으로부터 따라 나올 때 linarith를 사용하는 것이 흔히 편리하다는 것을 기억하십시오.

이것들을 비슷한 방식으로 증명할 수 있는지 살펴보십시오.

example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f :=
  sorry

example : ¬FnHasUb fun x ↦ x :=
  sorry

Mathlib은 순서와 부정을 연관 짓는 데 유용한 여러 정리를 제공합니다.

#check (not_le_of_gt : a > b → ¬a ≤ b)
#check (not_lt_of_ge : a ≥ b → ¬a < b)
#check (lt_of_not_ge : ¬a ≥ b → a < b)
#check (le_of_not_gt : ¬a > b → a ≤ b)

f가 비감소함을 말하는 술어 Monotone f를 상기하십시오. 방금 나열한 정리 중 일부를 사용하여 다음을 증명하십시오.

example (h : Monotone f) (h' : f a < f b) : a < b := by
  sorry

example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
  sorry

<를 ≤로 바꾸면 마지막 코드 조각의 첫 번째 예제를 증명할 수 없음을 보일 수 있습니다. 반례를 제시함으로써 전칭 양화된 명제의 부정을 증명할 수 있다는 점에 주목하십시오. 증명을 완성하십시오.

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f := fun x : ℝ ↦ (0 : ℝ)
  have monof : Monotone f := by sorry
  have h' : f 1 ≤ f 0 := le_refl _
  sorry

이 예제는 지역 문맥에 지역 정의를 추가하는 let 택틱을 소개합니다. let 명령 뒤에 커서를 놓으면, 목표 창에서 정의 f : ℝ → ℝ := fun x ↦ 0이 지역 문맥에 추가되었음을 볼 수 있습니다. Lean은 필요할 때 f의 정의를 펼칩니다. 특히 le_refl로 f 1 ≤ f 0을 증명할 때, Lean은 f 1과 f 0을 0으로 축약합니다.

다음을 증명하는 데 le_of_not_gt를 사용하십시오:

example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
  sorry

방금 수행한 여러 증명에는 다음과 같은 사실이 암묵적으로 내포되어 있습니다: P가 임의의 속성일 때, 속성 P를 가진 것이 없다고 말하는 것은 모든 것이 속성 P를 가지지 못한다고 말하는 것과 같으며, 모든 것이 속성 P를 가지는 것은 아니라고 말하는 것은 속성 P를 가지지 못하는 어떤 것이 있다고 말하는 것과 동치입니다. 다시 말해, 다음 네 가지 함의가 모두 성립합니다(다만 그중 하나는 지금까지 설명한 내용만으로는 증명할 수 없습니다):

variable {α : Type*} (P : α → Prop) (Q : Prop)

example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
  sorry

example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
  sorry

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  sorry

example (h : ∃ x, ¬P x) : ¬∀ x, P x := by
  sorry

첫 번째, 두 번째, 네 번째는 이미 살펴본 방법들을 사용하여 간단하게 증명할 수 있습니다. 직접 시도해 보기를 권장합니다. 하지만 세 번째는 더 어려운데, 대상이 존재하지 않는다는 것이 모순임을 근거로 그 대상이 존재한다는 결론을 내리기 때문입니다. 이는 고전적 수학적 추론의 한 사례입니다. 다음과 같이 귀류법을 사용하여 세 번째 함의를 증명할 수 있습니다.

example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
  by_contra h'
  apply h
  intro x
  show P x
  by_contra h''
  exact h' ⟨x, h''⟩

이것이 어떻게 작동하는지 반드시 이해하시기 바랍니다. by_contra 택틱을 사용하면 ¬ Q를 가정하고 모순을 이끌어 냄으로써 목표 Q를 증명할 수 있습니다. 사실 이는 동치 관계 not_not : ¬ ¬ Q ↔ Q를 사용하는 것과 동일합니다. by_contra를 사용하여 이 동치 관계의 순방향을 증명할 수 있음을 확인하십시오. 반면 역방향은 부정에 관한 일반적인 규칙으로부터 도출됩니다.

example (h : ¬¬Q) : Q := by
  sorry

example (h : Q) : ¬¬Q := by
  sorry

귀류법을 사용하여 다음을 증명하십시오. 이는 위에서 증명한 함의 중 하나의 역입니다. (힌트: 먼저 intro를 사용하십시오.)

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  sorry

앞에 부정이 붙은 복합 명제를 다루는 것은 종종 번거로우며, 이러한 명제를 부정이 안쪽으로 밀려 들어간 동치 형태로 바꾸는 것은 흔한 수학적 패턴입니다. 이를 돕기 위해 Mathlib은 등록된 보조정리를 사용하여 적용을 밀어 넣을 수 있는 push 택틱을 제공합니다. 여기서는 부정을 재서술하기 위해 push Neg를 사용할 것입니다(¬ ¬A를 A로 단순화하는 것도 여기에 포함됩니다). push Not at h 명령은 가정 h를 재서술합니다.

example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
  push Not at h
  exact h

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  dsimp only [FnHasUb, FnUb] at h
  push Not at h
  exact h

두 번째 예제에서는 FnHasUb와 FnUb의 정의를 전개하기 위해 dsimp를 사용합니다. (FnUb는 한정사의 범위 안에 나타나므로 이를 전개하려면 rw 대신 dsimp를 사용해야 합니다.) 위의 예제에서 ¬∃ x, P x와 ¬∀ x, P x에 대해 push 택틱이 예상대로 동작함을 확인할 수 있습니다. 연언 기호를 사용하는 법을 몰라도, push Not을 사용하여 다음을 증명할 수 있어야 합니다.

example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
  sorry

Mathlib에는 목표 A → B를 ¬B → ¬A로 변환하는 contrapose라는 택틱도 있습니다. 마찬가지로 가정 h : A로부터 B를 증명하는 목표가 주어졌을 때, contrapose h를 사용하면 가정 ¬B로부터 ¬A를 증명하는 목표가 남게 됩니다. contrapose 대신 contrapose!를 사용하면 목표뿐 아니라 관련 가정에도 push Not이 적용됩니다.

example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
  contrapose! h
  exact h

example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by
  contrapose! h
  use x / 2
  constructor <;> linarith

아직 constructor 명령이나 그 뒤에 오는 세미콜론의 사용법을 설명하지 않았지만, 다음 절에서 설명하겠습니다.

이 절은 모순으로부터 무엇이든 따라 나온다는 ex falso 원리로 마무리합니다. Lean에서 이는 False.elim으로 표현되며, 이는 임의의 명제 P에 대해 False → P를 증명합니다. 이는 이상한 원리처럼 보일 수 있지만, 실제로는 꽤 자주 등장합니다. 우리는 흔히 경우를 나누어 정리를 증명하며, 때로는 그 경우 중 하나가 모순임을 보일 수 있습니다. 이 경우에는 모순이 목표를 증명한다고 주장하여 다음 경우로 넘어갈 수 있도록 해야 합니다. (경우에 따른 추론의 예는 제 3.5 절에서 살펴보겠습니다.)

Lean은 모순에 도달했을 때 목표를 닫는 여러 방법을 제공합니다.

example (h : 0 < 0) : a > 37 := by
  exfalso
  apply lt_irrefl 0 h

example (h : 0 < 0) : a > 37 :=
  absurd h (lt_irrefl 0)

example (h : 0 < 0) : a > 37 := by
  have h' : ¬0 < 0 := lt_irrefl 0
  contradiction

exfalso 택틱은 현재 목표를 False를 증명하는 목표로 대체합니다. h : P와 h' : ¬ P가 주어지면, 항 absurd h h'는 임의의 명제를 증명합니다. 마지막으로, contradiction 택틱은 h : P와 h' : ¬ P 같은 형태의 쌍처럼 가정에서 모순을 찾아 목표를 닫으려고 시도합니다. 물론, 이 예제에서는 linarith도 통합니다.

3.4. 논리곱과 필요충분조건

논리곱 기호 ∧는 “그리고”를 나타내는 데 사용된다는 것을 이미 보았습니다. constructor 택틱을 사용하면 A를 증명한 다음 B를 증명하여 A ∧ B 형태의 명제를 증명할 수 있습니다.

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
  constructor
  · assumption
  intro h
  apply h₁
  rw [h]

이 예제에서 assumption 택틱은 Lean에게 목표를 해결할 가정을 찾으라고 지시합니다. 마지막 rw가 ≤의 반사성을 적용하여 목표를 완료한다는 점에 주목하십시오. 다음은 익명 생성자 꺾쇠괄호를 사용하여 앞의 예제들을 수행하는 대안적인 방법들입니다. 첫 번째는 앞의 증명을 매끄러운 증명항 버전으로 나타낸 것으로, 키워드 by에서 택틱 모드로 진입합니다.

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
  ⟨h₀, fun h ↦ h₁ (by rw [h])⟩

example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
  have h : x ≠ y := by
    contrapose! h₁
    rw [h₁]
  ⟨h₀, h⟩

논리곱을 증명하는 대신 사용하는 것은 두 부분의 증명을 풀어내는 일을 수반합니다. 이를 위해 rcases 택틱을 사용할 수 있으며, rintro나 패턴 매칭 fun도 사용할 수 있는데, 이는 모두 존재 한정사와 함께 사용되는 방식과 비슷합니다.

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  rcases h with ⟨h₀, h₁⟩
  contrapose! h₁
  exact le_antisymm h₀ h₁

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩ h'
  exact h₁ (le_antisymm h₀ h')

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x :=
  fun ⟨h₀, h₁⟩ h' ↦ h₁ (le_antisymm h₀ h')

obtain 택틱과 유사하게, 패턴 매칭 have도 있습니다:

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  have ⟨h₀, h₁⟩ := h
  contrapose! h₁
  exact le_antisymm h₀ h₁

rcases와 달리, 여기서는 have 택틱이 h를 지역 문맥에 남겨둡니다. 사용하지는 않겠지만, 여기서도 컴퓨터 과학자들의 패턴 매칭 구문이 있습니다:

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  cases h
  case intro h₀ h₁ =>
    contrapose! h₁
    exact le_antisymm h₀ h₁

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  cases h
  next h₀ h₁ =>
    contrapose! h₁
    exact le_antisymm h₀ h₁

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  match h with
    | ⟨h₀, h₁⟩ =>
        contrapose! h₁
        exact le_antisymm h₀ h₁

존재 한정사를 사용하는 것과 달리, h.left와 h.right, 또는 이와 동등하게 h.1과 h.2를 작성하여 가설 h : A ∧ B의 두 구성 요소의 증명을 추출할 수도 있습니다.

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
  intro h'
  apply h.right
  exact le_antisymm h.left h'

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x :=
  fun h' ↦ h.right (le_antisymm h.left h')

이 기법들을 사용하여 다음을 증명하는 다양한 방법을 찾아보십시오:

example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m :=
  sorry

익명 생성자, rintro, rcases를 사용하여 ∃와 ∧의 사용을 중첩할 수 있습니다.

example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
  ⟨5 / 2, by norm_num, by norm_num⟩

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
  rintro ⟨z, xltz, zlty⟩
  exact lt_trans xltz zlty

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y :=
  fun ⟨_z, xltz, zlty⟩ ↦ lt_trans xltz zlty

z 앞에 밑줄을 붙이는 것이 z를 사용할 의도가 없음을 Lean에 알린다는 것을 기억하십시오. 그렇지 않으면 Lean은 z가 사용되지 않았다는 경고를 출력할 것입니다.

use 택틱을 사용할 수도 있습니다:

example : ∃ x : ℝ, 2 < x ∧ x < 4 := by
  use 5 / 2
  constructor <;> norm_num

example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
  use 5
  use 7
  norm_num

example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
  rintro ⟨h₀, h₁⟩
  use h₀
  exact fun h' ↦ h₁ (le_antisymm h₀ h')

첫 번째 예제에서 constructor 명령 뒤에 오는 <;>는 결과로 나오는 두 목표 모두에 norm_num 택틱을 사용하도록 Lean에 지시합니다.

Lean에서 A ↔ B는 (A → B) ∧ (B → A)로 정의되어 있지는 않지만, 그렇게 정의될 수도 있었고, 대략 같은 방식으로 동작합니다. h : A ↔ B의 두 방향에 대해 h.mp와 h.mpr, 또는 h.1과 h.2를 쓸 수 있다는 것을 이미 보았습니다. cases와 그 유사한 것들을 사용할 수도 있습니다. 필요충분조건 명제를 증명하려면, 논리곱을 증명할 때와 마찬가지로 constructor나 꺾쇠괄호를 사용할 수 있습니다.

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
  constructor
  · contrapose!
    rintro rfl
    rfl
  contrapose!
  exact le_antisymm h

example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y :=
  ⟨fun h₀ h₁ ↦ h₀ (by rw [h₁]), fun h₀ h₁ ↦ h₀ (le_antisymm h h₁)⟩

마지막 증명항은 이해하기 어렵습니다. 그런 표현을 작성할 때 밑줄을 사용하여 Lean이 무엇을 기대하는지 확인할 수 있다는 것을 기억하십시오.

방금 살펴본 다양한 기법과 도구들을 활용하여 다음을 증명해 보십시오.

example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y :=
  sorry

더 흥미로운 연습 문제로, 임의의 두 실수 x와 y에 대해 x^2 + y^2 = 0인 것과 x = 0이고 y = 0인 것이 동치임을 보이십시오. linarith, pow_two_nonneg, eq_zero_of_pow_eq_zero를 사용하여 보조정리를 하나 증명해 볼 것을 제안합니다.

theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
  have h' : x ^ 2 = 0 := by sorry
  eq_zero_of_pow_eq_zero h'

example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 :=
  sorry

Lean에서 쌍방향 함의(bi-implication)는 두 가지 역할을 합니다. 이를 논리곱처럼 다루어 두 부분을 따로 사용할 수 있습니다. 하지만 Lean은 이를 명제 사이의 반사적이고 대칭적이며 추이적인 관계로도 알고 있으므로, calc와 rw도 함께 사용할 수 있습니다. 명제를 동치인 다른 명제로 다시 쓰는 것이 종종 편리합니다. 다음 예제에서는 abs_lt를 사용하여 |x| < y 형태의 식을 동치인 식 - y < x ∧ x < y로 바꾸고, 그다음 예제에서는 Nat.dvd_gcd_iff를 사용하여 m ∣ Nat.gcd n k 형태의 식을 동치인 식 m ∣ n ∧ m ∣ k로 바꿉니다.

example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
  rw [abs_lt]
  intro h
  constructor <;> linarith

example : 3 ∣ Nat.gcd 6 15 := by
  rw [Nat.dvd_gcd_iff]
  constructor <;> norm_num

아래 정리와 함께 rw를 사용하여 부정(negation)이 비감소 함수가 아님을 짧게 증명할 수 있는지 확인해 보십시오. (push Not은 정의를 펼쳐 주지 않으므로, 정리의 증명에서 rw [Monotone]이 필요하다는 점에 유의하십시오.)

theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
  rw [Monotone]
  push Not
  rfl

example : ¬Monotone fun x : ℝ ↦ -x := by
  sorry

이 절의 남은 연습문제들은 논리곱과 쌍조건문(bi-implication)을 좀 더 연습할 수 있도록 설계되었습니다. 부분순서는 추이적이고, 반사적이며, 반대칭적인 이항 관계임을 기억하십시오. 더 약한 개념도 종종 등장합니다: 준순서는 그저 반사적이고 추이적인 관계일 뿐입니다. 임의의 준순서 ≤에 대해, Lean은 a < b ↔ a ≤ b ∧ ¬ b ≤ a로 연관된 엄격 준순서를 공리화합니다. ≤가 부분순서라면, a < b는 a ≤ b ∧ a ≠ b와 동치임을 보이십시오:

variable {α : Type*} [PartialOrder α]
variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b := by
  rw [lt_iff_le_not_ge]
  sorry

논리 연산 외에는 le_refl, le_trans, le_antisymm만 있으면 됩니다. ≤가 준순서라고만 가정된 경우에도, 엄격 순서가 비반사적이고 추이적임을 증명할 수 있음을 보이십시오. 두 번째 예제에서는 편의를 위해 rw 대신 단순화기(simplifier)를 사용하여 <를 ≤와 ¬로 표현합니다. 단순화기에 대해서는 나중에 다시 다루겠지만, 여기서는 단순화기가 지정된 보조정리를 서로 다른 값으로 인스턴스화해야 하더라도 반복적으로 사용한다는 사실에만 의존합니다.

variable {α : Type*} [Preorder α]
variable (a b c : α)

example : ¬a < a := by
  rw [lt_iff_le_not_ge]
  sorry

example : a < b → b < c → a < c := by
  simp only [lt_iff_le_not_ge]
  sorry

3.5. 논리합

논리합 A ∨ B를 증명하는 표준적인 방법은 A를 증명하거나 B를 증명하는 것입니다. left 택틱은 A를 선택하고, right 택틱은 B를 선택합니다.

variable {x y : ℝ}

example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
  left
  linarith [pow_two_nonneg x]

example (h : -y > x ^ 2 + 1) : y > 0 ∨ y < -1 := by
  right
  linarith [pow_two_nonneg x]

우리가 어느 논리합 항을 증명하려는지 Lean이 추측해야 하기 때문에, “or”의 증명을 구성하는 데 익명 생성자를 사용할 수 없습니다. 증명 항을 작성할 때는 대신 Or.inl과 Or.inr을 사용하여 선택을 명시적으로 할 수 있습니다. 여기서 inl은 “introduction left”(왼쪽 도입)의 줄임말이고, inr은 “introduction right”(오른쪽 도입)의 줄임말입니다.

example (h : y > 0) : y > 0 ∨ y < -1 :=
  Or.inl h

example (h : y < -1) : y > 0 ∨ y < -1 :=
  Or.inr h

한쪽이나 다른 쪽을 증명함으로써 선언(disjunction)을 증명하는 것이 이상하게 보일 수 있습니다. 실제로는 어느 경우가 성립하는지가 대개 가정과 데이터에 암묵적이거나 명시적으로 존재하는 경우 구분에 달려 있습니다. rcases 택틱을 사용하면 A ∨ B 형태의 가정을 활용할 수 있습니다. 논리곱이나 존재 한정사와 함께 rcases를 사용하는 것과 달리, 여기서는 rcases 택틱이 두 개의 목표를 생성합니다. 두 목표 모두 결론은 같지만, 첫 번째 경우에는 A가 참이라고 가정되고, 두 번째 경우에는 B가 참이라고 가정됩니다. 다시 말해, 이름이 시사하듯이 rcases 택틱은 경우를 나누는 증명을 수행합니다. 평소와 마찬가지로, 가정에 사용할 이름을 Lean에게 알려 줄 수 있습니다. 다음 예제에서는 각 분기에서 이름 h를 사용하도록 Lean에 지시합니다.

example : x < |y| → x < y ∨ x < -y := by
  rcases le_or_gt 0 y with h | h
  · rw [abs_of_nonneg h]
    intro h; left; exact h
  · rw [abs_of_neg h]
    intro h; right; exact h

패턴이 논리곱의 경우 ⟨h₀, h₁⟩에서 선언의 경우 h₀ | h₁로 바뀌는 것에 주목하십시오. 첫 번째 패턴은 h₀와 h₁ 둘 다를 포함하는 데이터와 매칭되는 것으로, 반면 막대가 있는 두 번째 패턴은 h₀또는 h₁ 둘 중 하나를 포함하는 데이터와 매칭되는 것으로 생각하십시오. 이 경우에는 두 목표가 분리되어 있으므로, 각 경우에 동일한 이름인 h를 사용하기로 했습니다.

절댓값 함수는 x ≥ 0이 |x| = x를 함의한다는 것(이것이 정리 abs_of_nonneg입니다)과 x < 0이 |x| = -x를 함의한다는 것(이것이 abs_of_neg입니다)을 바로 증명할 수 있도록 정의되어 있습니다. 표현식 le_or_gt 0 x는 0 ≤ x ∨ x < 0을 증명하여, 이 두 경우로 나눌 수 있게 해줍니다.

Lean은 컴퓨터 과학자들의 선언(disjunction)에 대한 패턴 매칭 구문도 지원합니다. 이제 cases 택틱이 더 매력적인데, 각 case에 이름을 붙이고, 사용되는 곳에 더 가까이서 도입되는 가설에 이름을 붙일 수 있기 때문입니다.

example : x < |y| → x < y ∨ x < -y := by
  cases le_or_gt 0 y
  case inl h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  case inr h =>
    rw [abs_of_neg h]
    intro h; right; exact h

inl과 inr이라는 이름은 각각 “intro left”와 “intro right”의 줄임말입니다. case를 사용하면 경우들을 어느 순서로든 증명할 수 있다는 장점이 있습니다. Lean은 태그를 사용하여 관련 목표를 찾습니다. 그것이 신경 쓰이지 않는다면 next나 match, 또는 패턴 매칭 have를 사용할 수도 있습니다.

example : x < |y| → x < y ∨ x < -y := by
  cases le_or_gt 0 y
  next h =>
    rw [abs_of_nonneg h]
    intro h; left; exact h
  next h =>
    rw [abs_of_neg h]
    intro h; right; exact h

example : x < |y| → x < y ∨ x < -y := by
  match le_or_gt 0 y with
    | Or.inl h =>
      rw [abs_of_nonneg h]
      intro h; left; exact h
    | Or.inr h =>
      rw [abs_of_neg h]
      intro h; right; exact h

match의 경우에는 선언을 증명하는 표준적인 방법의 전체 이름인 Or.inl과 Or.inr을 사용해야 합니다. 이 교재에서는 일반적으로 선언의 경우들을 나누기 위해 rcases를 사용하겠습니다.

다음 코드 조각에 나오는 처음 두 정리를 사용하여 삼각 부등식을 증명해 보십시오. 이 정리들은 Mathlib에서와 같은 이름이 붙어 있습니다.

namespace MyAbs

theorem le_abs_self (x : ℝ) : x ≤ |x| := by
  sorry

theorem neg_le_abs (x : ℝ) : -x ≤ |x| := by
  sorry

theorem abs_add_le (x y : ℝ) : |x + y| ≤ |x| + |y| := by
  sorry

이 문제들이 마음에 들었고(말장난 의도) 선언에 대한 연습을 더 하고 싶다면 다음 문제들을 풀어 보십시오.

theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
  sorry

theorem abs_lt : |x| < y ↔ -y < x ∧ x < y := by
  sorry

중첩된 논리합에 대해서도 rcases와 rintro를 사용할 수 있습니다. 이것들이 여러 목표를 갖는 진정한 케이스 분리로 이어지는 경우, 각 새 목표에 대한 패턴은 세로선으로 구분됩니다.

example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
  rcases lt_trichotomy x 0 with xlt | xeq | xgt
  · left
    exact xlt
  · contradiction
  · right; exact xgt

여전히 패턴을 중첩할 수 있으며, 방정식을 치환하기 위해 rfl 키워드를 사용할 수 있습니다:

example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
  rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
  · rw [mul_assoc]
    apply dvd_mul_right
  · rw [mul_comm, mul_assoc]
    apply dvd_mul_right

다음 명제를 한 줄(긴 줄)로 증명할 수 있는지 확인해 보십시오. 가설을 풀어헤치고 케이스를 나누기 위해 rcases를 사용하고, 각 분기를 해결하기 위해 <;> linarith를 사용하십시오.

example {z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
  sorry

실수에서, 방정식 x * y = 0은 x = 0 또는 y = 0임을 말해 줍니다. Mathlib에서 이 사실은 eq_zero_or_eq_zero_of_mul_eq_zero로 알려져 있으며, 논리합이 어떻게 나타날 수 있는지를 보여 주는 또 다른 좋은 예시입니다. 이를 사용하여 다음을 증명할 수 있는지 확인해 보십시오:

example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  sorry

example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
  sorry

계산을 돕기 위해 ring 택틱을 사용할 수 있음을 기억하십시오.

임의의 환 \(R\)에서, 어떤 0이 아닌 \(y\)에 대해 \(x y = 0\)을 만족하는 원소 \(x\)를 왼쪽 영인자라 하고, 어떤 0이 아닌 \(y\)에 대해 \(y x = 0\)을 만족하는 원소 \(x\)를 오른쪽 영인자라 하며, 왼쪽 또는 오른쪽 영인자인 원소를 단순히 영인자라 합니다. 정리 eq_zero_or_eq_zero_of_mul_eq_zero는 실수에는 자명하지 않은 영인자가 없음을 말해 줍니다. 이 성질을 만족하는 가환환은 정역이라고 합니다. 위 두 정리에 대한 증명은 어떤 정역에서도 마찬가지로 작동해야 합니다:

variable {R : Type*} [CommRing R] [IsDomain R]
variable (x y : R)

example (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  sorry

example (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
  sorry

사실 주의를 기울이면, 곱셈의 가환성을 사용하지 않고도 첫 번째 정리를 증명할 수 있습니다. 그 경우에는 R이 CommRing 대신 Ring이라고 가정하는 것으로 충분합니다.

때로는 증명 중에 어떤 명제가 참인지 거짓인지에 따라 경우를 나누고 싶을 때가 있습니다. 임의의 명제 P에 대해, em P : P ∨ ¬ P를 사용할 수 있습니다. em이라는 이름은 “배중률”(excluded middle)을 줄인 것입니다.

example (P : Prop) : ¬¬P → P := by
  intro h
  cases em P
  · assumption
  · contradiction

또는 by_cases 택틱을 사용할 수도 있습니다.

example (P : Prop) : ¬¬P → P := by
  intro h
  by_cases h' : P
  · assumption
  contradiction

by_cases 택틱을 사용하면 각 분기에 도입되는 가설의 이름을 지정할 수 있음에 유의하십시오. 이 경우 한쪽은 h' : P이고 다른 한쪽은 h' : ¬ P입니다. 이름을 생략하면 Lean은 기본값으로 h를 사용합니다. by_cases를 사용해 한쪽 방향을 증명함으로써 다음 동치를 증명해 보십시오.

example (P Q : Prop) : P → Q ↔ ¬P ∨ Q := by
  sorry

3.6. 수열과 수렴

이제 실제 수학을 할 만큼 충분한 기술을 갖추었습니다. Lean에서는 실수의 수열 \(s_0, s_1, s_2, \ldots\)를 함수 s : ℕ → ℝ로 나타낼 수 있습니다. 이러한 수열은 모든 \(\varepsilon > 0\)에 대해, 그 지점 이후로는 수열이 \(a\)로부터 \(\varepsilon\) 이내에 머무르는 지점이 존재할 때, 즉 모든 \(n \ge N\)에 대해 \(| s_n - a | < \varepsilon\)을 만족하는 수 \(N\)이 존재할 때 \(a\)에 수렴한다고 합니다. Lean에서는 이를 다음과 같이 나타낼 수 있습니다.

def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

표기 ∀ ε > 0, ...는 ∀ ε, ε > 0 → ...의 편리한 축약형이며, 마찬가지로 ∀ n ≥ N, ...은 ∀ n, n ≥ N →  ...의 축약형입니다. 그리고 ε > 0은 결국 0 < ε로 정의되며, n ≥ N은 N ≤ n으로 정의된다는 점을 기억하십시오.

이 절에서는 수렴의 몇 가지 성질을 증명하겠습니다. 하지만 먼저, 유용하게 쓰일 등식을 다루는 세 가지 택틱에 대해 논의하겠습니다. 첫 번째인 ext 택틱은 두 함수가 같음을 증명하는 방법을 제공합니다. 실수에서 실수로 가는 함수로서 \(f(x) = x + 1\)과 \(g(x) = 1 + x\)를 생각해봅시다. 그러면 이들은 모든 \(x\)에 대해 같은 값을 반환하므로 물론 \(f = g\)입니다. ext 택틱을 사용하면 인자의 모든 값에서 두 함수의 값이 같음을 증명함으로써 두 함수 사이의 등식을 증명할 수 있습니다.

example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
  ext
  ring

나중에 살펴보겠지만 ext는 실제로 더 일반적이며, 나타나는 변수의 이름을 지정할 수도 있습니다. 예를 들어 위 증명에서 ext를 ext u v로 바꿔볼 수 있습니다. 두 번째 택틱인 congr 택틱은 서로 다른 부분을 조정함으로써 두 식 사이의 등식을 증명할 수 있게 해줍니다:

example (a b : ℝ) : |a| = |a - b + b| := by
  congr
  ring

여기서 congr 택틱은 양쪽에서 abs를 벗겨내어, a = a - b + b를 증명하도록 남겨둡니다.

마지막으로, convert 택틱은 정리의 결론이 목표와 정확히 일치하지 않을 때 정리를 목표에 적용하는 데 사용됩니다. 예를 들어, 1 < a로부터 a < a * a를 증명하고 싶다고 가정해 봅시다. 라이브러리에 있는 정리인 mul_lt_mul_iff_left₀는 1 * a < a * a를 증명할 수 있게 해줍니다. 한 가지 방법은 거꾸로 작업하여 목표가 그 형태를 갖도록 다시 쓰는 것입니다. 대신, convert 택틱은 정리를 있는 그대로 적용할 수 있게 해주고, 목표를 일치시키는 데 필요한 방정식들을 증명하는 과제를 남겨둡니다. convert! 변형은 결과로 생긴 목표들을 해결하려 할 때 정의를 더 적극적으로 펼칩니다.

example {a : ℝ} (h : 1 < a) : a < a * a := by
  convert! (mul_lt_mul_iff_left₀ _).2 h
  · rw [one_mul]
  exact lt_trans zero_lt_one h

이 예제는 또 다른 유용한 요령을 보여줍니다: 밑줄이 있는 표현식을 적용할 때 Lean이 자동으로 채울 수 없으면, 단순히 그것을 다른 목표로 남겨둡니다.

다음은 임의의 상수 수열 \(a, a, a, \ldots\)가 수렴함을 보여줍니다.

theorem convergesTo_const (a : ℝ) : ConvergesTo (fun _x : ℕ ↦ a) a := by
  intro ε εpos
  use 0
  intro n nge
  rw [sub_self, abs_zero]
  apply εpos

Lean에는 simp라는 택틱이 있는데, 이는 종종 rw [sub_self, abs_zero]와 같은 단계를 손으로 수행하는 수고를 덜어줄 수 있습니다. 곧 이에 대해 더 알려드리겠습니다.

더 흥미로운 정리로, s가 a로 수렴하고 t가 b로 수렴하면 fun n ↦ s n + t n이 a + b로 수렴함을 보여봅시다. 형식적인 증명을 작성하기 전에 명확한 종이와 펜 증명을 마음속에 가지고 있는 것이 도움이 됩니다. 0보다 큰 ε이 주어지면, 아이디어는 가정을 사용해 그 지점을 넘으면 s가 a로부터 ε / 2 이내에 있게 되는 Ns를, 그리고 그 지점을 넘으면 t가 b로부터 ε / 2 이내에 있게 되는 Nt를 얻는 것입니다. 그러면 n이 Ns와 Nt의 최댓값보다 크거나 같을 때마다 수열 fun n ↦ s n + t n은 a + b로부터 ε 이내에 있어야 합니다. 다음 예제는 이 전략을 구현하기 시작합니다. 끝까지 완성할 수 있는지 확인해 보십시오.

theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n + t n) (a + b) := by
  intro ε εpos
  dsimp -- this line is not needed but cleans up the goal a bit.
  have ε2pos : 0 < ε / 2 := by linarith
  rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
  rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
  use max Ns Nt
  sorry

힌트로, le_of_max_le_left와 le_of_max_le_right를 사용할 수 있으며, norm_num은 ε / 2 + ε / 2 = ε을 증명할 수 있습니다. 또한 |s n + t n - (a + b)|가 |(s n - a) + (t n - b)|,와 같음을 보이기 위해 congr 택틱을 사용하는 것이 도움이 되는데, 그러면 삼각 부등식을 사용할 수 있기 때문입니다. 모든 변수 s, t, a, b를 암묵적으로 표시했는데, 이는 가정으로부터 추론될 수 있기 때문임을 주목하십시오.

덧셈 대신 곱셈을 사용해 같은 정리를 증명하는 것은 까다롭습니다. 먼저 몇 가지 보조 명제를 증명함으로써 그 목표에 도달하겠습니다. s가 a로 수렴하면 fun n ↦ c * s n도 c * a로 수렴함을 보이는 다음 증명도 끝낼 수 있는지 확인해 보십시오. c가 0과 같은지 아닌지에 따라 경우를 나누는 것이 도움이 됩니다. 0인 경우는 이미 처리해 두었으며, c가 0이 아니라는 추가 가정 하에 결과를 증명하는 것은 여러분의 몫으로 남겨 두었습니다.

theorem convergesTo_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : ConvergesTo s a) :
    ConvergesTo (fun n ↦ c * s n) (c * a) := by
  by_cases h : c = 0
  · convert convergesTo_const 0
    · rw [h]
      ring
    rw [h]
    ring
  have acpos : 0 < |c| := abs_pos.mpr h
  sorry

다음 정리도 그 자체로 흥미롭습니다: 수렴하는 수열은 결국 절댓값이 유계임을 보입니다. 시작 부분은 저희가 작성해 두었으니, 나머지를 끝낼 수 있는지 확인해 보십시오.

theorem exists_abs_le_of_convergesTo {s : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) :
    ∃ N b, ∀ n, N ≤ n → |s n| < b := by
  rcases cs 1 zero_lt_one with ⟨N, h⟩
  use N, |a| + 1
  sorry

사실 이 정리는 모든 n의 값에 대해 성립하는 상계 b가 존재한다는 더 강한 형태로 주장할 수 있습니다. 하지만 이 버전은 우리의 목적에 충분히 강하며, 이 절 끝에서 이것이 더 일반적으로 성립함을 보게 될 것입니다.

다음 보조정리는 보조적인 것으로, s가 a로 수렴하고 t가 0으로 수렴하면 fun n ↦ s n * t n도 0으로 수렴함을 증명합니다. 이를 위해 앞의 정리를 사용하여 어떤 지점 N₀이후로 s를 유계로 만드는 B를 찾습니다. 저희가 개략적으로 설명한 전략을 이해하고 증명을 끝낼 수 있는지 확인해 보십시오.

theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t 0) :
    ConvergesTo (fun n ↦ s n * t n) 0 := by
  intro ε εpos
  dsimp
  rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
  have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
  have pos₀ : ε / B > 0 := div_pos εpos Bpos
  rcases ct _ pos₀ with ⟨N₁, h₁⟩
  sorry

여기까지 왔다면, 축하합니다! 우리는 이제 정리에 거의 다다랐습니다. 다음 증명이 이를 마무리합니다.

theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ}
      (cs : ConvergesTo s a) (ct : ConvergesTo t b) :
    ConvergesTo (fun n ↦ s n * t n) (a * b) := by
  have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
    apply aux cs
    convert convergesTo_add ct (convergesTo_const (-b))
    ring
  have := convergesTo_add h₁ (convergesTo_mul_const b cs)
  convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
  · ext; ring
  ring

또 다른 도전적인 연습 문제로, 극한이 유일하다는 증명의 다음 스케치를 완성해 보십시오. (대담하게 도전하고 싶다면, 증명 스케치를 지우고 처음부터 증명해 볼 수 있습니다.)

theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ}
      (sa : ConvergesTo s a) (sb : ConvergesTo s b) :
    a = b := by
  by_contra abne
  have : |a - b| > 0 := by sorry
  let ε := |a - b| / 2
  have εpos : ε > 0 := by
    change |a - b| / 2 > 0
    linarith
  rcases sa ε εpos with ⟨Na, hNa⟩
  rcases sb ε εpos with ⟨Nb, hNb⟩
  let N := max Na Nb
  have absa : |s N - a| < ε := by sorry
  have absb : |s N - b| < ε := by sorry
  have : |a - b| < |a - b| := by sorry
  exact lt_irrefl _ this

이 절을 우리의 증명이 일반화될 수 있다는 관찰로 마무리합니다. 예를 들어, 우리가 자연수에 대해 사용한 유일한 성질은 그 구조가 min과 max를 갖춘 부분 순서를 지닌다는 것입니다. ℕ을 어디서나 임의의 선형 순서 α로 바꾸더라도 모든 것이 여전히 작동함을 확인할 수 있습니다:

variable {α : Type*} [LinearOrder α]

def ConvergesTo' (s : α → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε

뒤의 제 11.1 절에서 살펴보겠지만, Mathlib에는 정의역과 공역의 특정 성질뿐 아니라 서로 다른 종류의 수렴까지 추상화하여 훨씬 일반적으로 수렴을 다루는 메커니즘이 있습니다.