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-space 자동 완성(Mac에서는 Cmd-space 자동 완성)으로 찾을 수 있다는 점을 기억하십시오. 또한 .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가 올바른 형식의 명제입니다. 예를 들어 ZF에서는 sin ∈ cos도 올바른 형식의 명제입니다. 집합론적 기초가 가진 이러한 결함은, 무의미한 표현식을 찾아내어 우리를 돕도록 만들어진 증명 보조기에서 집합론적 기초를 사용하지 않는 중요한 동기가 됩니다. 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를 정의했던 것과 마찬가지로, s가 순서가 주어진 어떤 타입의 원소들의 집합이라고 가정하면 a가 집합 s의 상계라는 것을 의미하도록 SetUb s a를 정의할 수 있습니다. 다음 예제에서는 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

마지막으로 중요한 예제 하나를 보며 이 절을 마무리하겠습니다. 모든 \(x_1\)과 \(x_2\)에 대해 \(f(x_1) = f(x_2)\)이면 \(x_1 = x_2\)일 때, 함수 \(f\)를 단사라고 합니다. 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는 5 / 2로 입력할 수 있고, 우리가 실수를 염두에 두고 있다는 것을 Lean이 문맥에서 추론하지 못할 때는 (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⟩

이제 존재 명제를 증명하는 방법을 알게 되었습니다. 그렇다면 존재 명제는 어떻게 사용합니까? 어떤 성질을 가진 대상이 존재한다는 것을 안다면, 그중 임의의 하나에 이름을 붙이고 그것에 대해 추론할 수 있어야 합니다. 예를 들어, 지난 절에서 본 술어 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 + bi\) 꼴의 수이며, 여기서 \(a\)와 \(b\)는 정수이고 \(i = \sqrt{-1}\)입니다. 가우스 정수 \(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\)에 대해 \(f(x) = y\)를 만족하는 \(x\)가 정의역 \(\alpha\)에 존재할 때 전사라고 합니다. 이 명제에는 전칭 한정기호와 존재 한정기호가 모두 포함되어 있다는 점에 주목하십시오. 다음 예제에서 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

두 번째 예제에서는 dsimp를 사용하여 FnHasUb와 FnUb의 정의를 펼칩니다. (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 : A ∧ B의 두 성분에 대한 증명은 h.left와 h.right, 또는 같은 의미로 h.1과 h.2를 써서 꺼낼 수도 있습니다.

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

이 절의 나머지 연습 문제는 논리곱과 쌍방 함의를 좀 더 연습할 수 있도록 구성되어 있습니다. 부분 순서는 추이적이고 반사적이며 반대칭적인 이항 관계라는 점을 기억하십시오. 때로는 이보다 더 약한 개념이 등장하기도 합니다. 준순서는 단지 반사적이고 추이적인 관계입니다. 임의의 준순서 ≤에 대해, 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 대신 단순화기를 사용하여 <를 ≤와 ¬로 표현합니다. 단순화기는 나중에 다시 다루겠지만, 여기서는 지정된 보조정리를 서로 다른 값으로 인스턴스화해야 하더라도 단순화기가 그 보조정리를 반복해서 사용한다는 사실에만 의존합니다.

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.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

한쪽 또는 다른 쪽을 증명함으로써 논리합을 증명한다는 것이 이상하게 보일 수도 있습니다. 실제로는 어느 경우가 성립하는지가 대개 가정과 데이터에 암묵적으로 또는 명시적으로 들어 있는 경우 구분에 달려 있습니다. 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은 논리합에 대해 컴퓨터 과학자들이 쓰는 패턴 매칭 구문도 지원합니다. 이제 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이 그 자리를 자동으로 채우지 못하면, 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 = ε을 증명할 수 있습니다. 또한 congr 택틱을 사용하여 |s n + t n - (a + b)|가 |(s n - a) + (t n - b)|,와 같음을 보이면 도움이 됩니다. 그러면 삼각 부등식을 사용할 수 있기 때문입니다. 변수 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이 훨씬 더 일반적인 방식으로 수렴을 다루는 메커니즘을 갖추고 있음을 살펴봅니다. 이 메커니즘은 정의역과 공역의 특정한 성질을 추상화할 뿐 아니라, 서로 다른 종류의 수렴까지 추상화합니다.