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 タクティクスを用いて my_lemma を |a * b| < δ という形のゴールに適用すると、 各仮説を証明するための新たなゴールが残ることが分かるはずです。

このような命題を証明するには、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_right、および one_mul を用いてください。 また、Ctrl-space 補完 (Mac では Cmd-space 補完) を使ってこのような定理を見つけられることを忘れないでください。 さらに、if-and-only-if の命題から2方向 (正方向と逆方向) を抽出するには、.mp と .mpr、または .1 と .2 を使用できることも覚えておいてください。

全焼量化子は定義の中に隠れていることが多く、Lean は必要に応じてそれらを明らかにするために定義を展開します。 たとえば、ここでは2つの述語 FnUb f a と FnLb f a を定義します。 ここで、f は実数から実数への関数で、a は実数です。 最初の述語は、a が関数 f の値に対する上限であることを示し、2番目の述語は、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” の略です。) そのコマンドを削除しても証明は動作します。 Lean は次の apply を意味づけるために、いずれにせよその縮約を行う必要があるからです。 dsimp コマンドは単にゴールをより読みやすくし、次に何をすべきかを判断する助けとなります。 別の方法としては、change タクティクスを使い、change f x + g x ≤ a + b と書く方法があります。 これにより証明がより読みやすくなり、ゴールがどのように変換されるかについて、より細かい制御が可能になります。

証明の残りの部分は定型的なものです。 最後の2つの apply コマンドは、仮説中の FnUb の定義を展開するように Lean に強制します。 同様の証明を他にも試してみてください。

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 を定義したとしても、これらの定義と証明ははるかに一般的なものであることに気づくべきです。 これらの定義は、値域に順序の概念がある任意の2つの型間の関数について意味を持ちます。 定理 add_le_add の型を確認すると、これは「順序付き加法可換モノイド」である任意の構造に対して成り立つことが分かります。 ここでの「順序付き加法可換モノイド」が何を意味するかの詳細は今は問題ではありませんが、自然数、整数、有理数、実数がすべてその例であることを知っておく価値があります。 したがって、そのような一般性のレベルで定理 fnUb_add を証明すれば、これらすべての例に適用できることになります。

variable {α : Type*} {R : Type*} [OrderedCancelAddCommMonoid 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)

これらの角括弧は、セクション Section 2.2 で既に見たことがあるかもしれませんが、その意味についてはまだ説明していません。 具体例としては、ほとんどの例で実数に限定して扱いますが、Mathlib には非常に一般的なレベルで動作する定義や定理が含まれていることを知っておく価値があります。

もう一つの隠れた全称量化子の例として、Mathlib は述語 Monotone を定義しています。 これは、関数がその引数において単調非減少であることを示します。

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

Monotone f という性質は、コロンの後にある式と全く同じものとして定義されます。 もしその前に @ 記号を付けなければ、Lean は h の暗黙の引数を展開してプレースホルダーを挿入してしまうため、@ 記号が必要です。

単調性に関する命題を証明するには、intro を用いて2つの変数、例えば 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 Goal ウィンドウを確認するか、波線のエラーマーカーにカーソルを合わせると、残りの式が解決すべきゴールが表示されます。

これらを、タクティクスまたは証明項のいずれかを使って証明してみてください。

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

以下は、いくつかの例です。 実数から実数への関数 \(f\) が、すべての \(x\) に対して \(f(-x) = f(x)\) を満たすとき、これを 偶関数 と呼び、 すべての \(x\) に対して \(f(-x) = -f(x)\) を満たすとき、これを 奇関数 と呼びます。 次の例では、これら2つの概念を形式的に定義し、さらにそれらに関する一つの事実を示します。 他の部分の証明は、あなた自身で完成させてみてください。

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 が正しく定義された命題として受け入れない」ということです。 これは、例えば Zermelo-Fraenkel 集合論では、任意の数学的対象 a と b に対して a ∈ b は正しく定義された命題となり、たとえば sin ∈ cos という表現も ZF では正しく扱われます。 しかし、この集合論的基礎の欠点は、意味のない表現を検出して支援することを目的とした証明支援システムにとっては大きな問題となるため、Lean ではこのような状況を避けています。 Lean においては、sin は型 ℝ → ℝ を持ち、cos も同様に型 ℝ → ℝ を持つため、これらは Set (ℝ → ℝ) とは等しくなく、結果として命題 sin ∈ cos は意味をなさないのです。 なお、Lean を用いて集合論そのものを扱うことも可能です。 例えば、Zermelo-Fraenkel の公理系から連続体仮説の独立性が形式化されています。 しかし、そのような集合論のメタ理論は、本書の範囲をはるかに超えています。

もし 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 を定義したのと同様に、SetUb s a は、型に順序が付随する集合 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

最後に、この節を締めくくる重要な例をひとつ示します。 関数 \(f\) が、任意の \(x₁\) と \(x₂\) に対して、もし \(f(x₁) = f(x₂)\) ならば \(x₁ = x₂\) となるとき、単射 であると言います。 Mathlib では、Function.Injective f として定義され、ここでの x₁ と x₂ は暗黙に扱われます。 次の例では、実数において、任意の定数を加える関数が単射であることを示しています。 その後、例で示された補題名を参考に、非零定数による乗法も単射であることを示すよう求められます。 補題名の先頭を推測した後、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

最後に、2つの単射関数の合成が単射であることを示してください。

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 の間に実数が存在することを示しています。 (論理積記号 ∧ については Section 3.4 で説明します。) このような命題を証明する標準的な方法は実数を具体的に示し、その数が述べられた性質を満たすことを示すことです。 Lean が文脈から実数を推論できない場合は 5 / 2 または (5 : ℝ) / 2 と入力することで表せる 2.5 がその性質を満たし、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 の 匿名構成子 (anonymous constructor) 記法を用いて、存在量化子の証明を構築することもできます。

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⟩ のような注釈は パターン (patterns) と呼ばれ、メインの引数を展開したときに見つかると期待される情報を記述します。 例えば、関数 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 は式や証明項におけるパターンマッチング機能もサポートしています。

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 すると言われますが、わずかな違いがあります。 すなわち、rcases は処理が終わると ubf を文脈から消去するのに対し、obtain は消去せずに文脈に残したままとなります。

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 の後ろに置くと、タクティクスが1つのゴールを生成していることが分かります。 このゴールは Lean によって intro とタグ付けされています。(ここで選ばれた名前は、存在命題の証明を構成する公理的プリミティブの内部名に由来します。) case タクティクスはその後で各構成要素に名前を付けます。 2番目の例は同様ですが、case の代わりに next を使用することで intro を明示する必要を回避できます。 最後の2つの例における単語 match はここで行っていることがコンピュータサイエンティストにおける「パターンマッチング」と呼ぶものであることを強調しています。 なお、3番目の証明は by で始まり、その後にタクティクス版の match が矢印の右側にタクティクス証明を期待します。 最後の例は証明項による証明であり、タクティクスは一切用いられていません。

本書の残りでは、存在量化子を扱う際の好ましい方法として rcases、rintro、および obtain を使います。 しかし、別の構文も知っておくと、特にコンピュータサイエンティストと共に作業する機会があれば、有用かもしれません。

rcases の一つの利用方法を示すために古典的な数学の命題、すなわち「2つの整数 x と y がそれぞれ2つの平方数の和として表されるならば、その積 x * y もまた2つの平方数の和として表される」という命題を証明します。 実際、この命題は整数に限らず、任意の可換環について成り立ちます。 次の例では、rcases を用いて2つの存在量化子を一度に展開します。 その後、x * y を2つの平方数の和として表すために必要な魔法の値をリストとして 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

この証明は多くの洞察を与えるものではありませんが、以下のような動機付けができます。 ガウス整数 (Gaussian integer) とは、\(a + bi\) の形の数であり、ここで \(a\) と \(b\) は整数、\(i = \sqrt{-1}\) です。 ガウス整数 \(a + bi\) の ノルム (norm) は定義により \(a^2 + b^2\) となります。 したがって、ガウス整数のノルムは平方数の和であり、任意の平方数の和はこの形で表せます。 上記の定理は、ガウス整数の積のノルムが、それぞれのガウス整数のノルムの積に等しいという事実を反映しています。 すなわち、もし \(x\) が \(a + bi\) のノルムで、\(y\) が \(c + di\) のノルムならば、\(xy\) は \((a + bi) (c + di)\) のノルムとなります。 このやや難解な証明は形式化しやすい証明が必ずしも最も明瞭なものではないという事実を示しています。 Section 6.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\) のある \(x\) が存在し、かつ \(f(x) = y\) となるとき、*全射 (surjective)*であると言います。 この命題は、全称量化子と存在量化子の両方を含んでいることに注意してください。 これが、次の例で intro と use の両方が使用される理由です。

example {c : ℝ} : Surjective fun x ↦ x + c := by
  intro x
  use x - 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 が矛盾を導くという意味で捉えることができます。 実際には ¬ A を証明するには仮定 h : A を導入し、False を証明すればよく、また、もし h : ¬ A と h' : A がある場合、h に h' を適用すると False が得られます。

例として、狭義順序における反自明性の原理 lt_irrefl を考えます。 これは、任意の a に対して ¬ a < a が成り立つことを示しています。 また、非対称性の原理 lt_asymm は、a < b → ¬ b < a であると言います。 ここでは、lt_irrefl から lt_asymm が導かれることを示してみましょう。

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

この例では、いくつか新しいテクニックが紹介されています。 まず、ラベルを指定せずに have を使うと、Lean は自動的にその証明項に this という名前を付け、後で参照するのに便利な方法を提供します。 証明が非常に短いため、ここでは明示的な証明項を示しています。 しかし、この証明で本当に注目すべき点は intro タクティクスの結果として残るゴールが False であること、そして最終的に 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)

Monotone f という述語は、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 タクティクスが導入され、文脈に 局所定義 (local definition) が追加されます。 もしカーソルを 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 を持たない」と同値であるということが挙げられます。 つまり、次の4つの含意はすべて有効です (ただし、そのうちの1つは、ここまで説明した内容だけでは証明できません)。

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

最初、2番目、および4番目の含意は、これまでに見た手法を用いれば容易に証明できます。 ぜひ試してみてください。 しかし、3番目はより困難です。 なぜなら、存在しないということが矛盾しているという事実から、ある対象が存在することを結論付けるからです。 これは、古典的 (classical) な数学的推論の一例です。 この3番目の含意は背理法を用いて次のように証明できます。

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 を使ってこの等価性の順方向 (すなわち ¬ ¬ Q → Q) を証明できることを確認し、逆方向は通常の否定の規則から導かれることも確認してください。

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

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

背理法を用いて、上で証明した含意の1つの逆を確立するために、次の命題を証明してください。(ヒント: 最初に intro を使用してください。)

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

複合命題の先頭に否定があると扱うのが面倒な場合が多く、そのような命題は否定が内側に押し込まれた同値な形に置き換えるというのが一般的な数学的パターンです。 これを容易にするために、Mathlib はこの方法でゴールを再記述する push_neg タクティクスを提供しています。 コマンド push_neg at h は仮定 h を同様に再記述します。

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

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

第二の例では、FnHasUb と FnUb の定義を展開するために dsimp を使用しています。（FnUb は量化子のスコープ内に現れるため、展開には rw ではなく dsimp を用いる必要があります。） 上記の例、すなわち ¬∃ x, P x や ¬∀ x, P x において、push_neg タクティクスが期待通りの動作をすることを確認できるはずです。 論理積記号の使い方すら知らなくても、push_neg を使って次の命題を証明できるはずです。

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! を使うと、ゴールと該当する仮定に対して push_neg も適用されます。

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 を成立させます。 一見奇妙な原理に思えるかもしれませんが、かなり頻繁に現れます。 多くの場合、定理を場合分けして証明し、その中の一つのケースが矛盾していることを示すことがあります。 その場合、その矛盾がゴールを成立させることを主張し、次のケースに進む必要があります。（論理和における場合分けによる推論の事例は、Section 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. Conjunction and Iff

You have already seen that the conjunction symbol, ∧, is used to express “and.” The constructor tactic allows you to prove a statement of the form A ∧ B by proving A and then proving B.

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

In this example, the assumption tactic tells Lean to find an assumption that will solve the goal. Notice that the final rw finishes the goal by applying the reflexivity of ≤. The following are alternative ways of carrying out the previous examples using the anonymous constructor angle brackets. The first is a slick proof-term version of the previous proof, which drops into tactic mode at the keyword 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⟩

Using a conjunction instead of proving one involves unpacking the proofs of the two parts. You can use the rcases tactic for that, as well as rintro or a pattern-matching fun, all in a manner similar to the way they are used with the existential quantifier.

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')

In analogy to the obtain tactic, there is also a pattern-matching have:

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

In contrast to rcases, here the have tactic leaves h in the context. And even though we won’t use them, once again we have the computer scientists’ pattern-matching syntax:

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₁

In contrast to using an existential quantifier, you can also extract proofs of the two components of a hypothesis h : A ∧ B by writing h.left and h.right, or, equivalently, h.1 and 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')

Try using these techniques to come up with various ways of proving of the following:

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

You can nest uses of ∃ and ∧ with anonymous constructors, rintro, and 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

You can also use the use tactic:

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')

In the first example, the semicolon after the constructor command tells Lean to use the norm_num tactic on both of the goals that result.

In Lean, A ↔ B is not defined to be (A → B) ∧ (B → A), but it could have been, and it behaves roughly the same way. You have already seen that you can write h.mp and h.mpr or h.1 and h.2 for the two directions of h : A ↔ B. You can also use cases and friends. To prove an if-and-only-if statement, you can use constructor or angle brackets, just as you would if you were proving a conjunction.

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₁)⟩

The last proof term is inscrutable. Remember that you can use underscores while writing an expression like that to see what Lean expects.

Try out the various techniques and gadgets you have just seen in order to prove the following:

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

For a more interesting exercise, show that for any two real numbers x and y, x^2 + y^2 = 0 if and only if x = 0 and y = 0. We suggest proving an auxiliary lemma using linarith, pow_two_nonneg, and pow_eq_zero.

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

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

In Lean, bi-implication leads a double-life. You can treat it like a conjunction and use its two parts separately. But Lean also knows that it is a reflexive, symmetric, and transitive relation between propositions, and you can also use it with calc and rw. It is often convenient to rewrite a statement to an equivalent one. In the next example, we use abs_lt to replace an expression of the form |x| < y by the equivalent expression - y < x ∧ x < y, and in the one after that we use Nat.dvd_gcd_iff to replace an expression of the form m ∣ Nat.gcd n k by the equivalent expression 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

See if you can use rw with the theorem below to provide a short proof that negation is not a nondecreasing function. (Note that push_neg won’t unfold definitions for you, so the rw [Monotone] in the proof of the theorem is needed.)

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

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

The remaining exercises in this section are designed to give you some more practice with conjunction and bi-implication. Remember that a partial order is a binary relation that is transitive, reflexive, and antisymmetric. An even weaker notion sometimes arises: a preorder is just a reflexive, transitive relation. For any pre-order ≤, Lean axiomatizes the associated strict pre-order by a < b ↔ a ≤ b ∧ ¬ b ≤ a. Show that if ≤ is a partial order, then a < b is equivalent to a ≤ b ∧ a ≠ b:

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

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

Beyond logical operations, you do not need anything more than le_refl and le_trans. Show that even in the case where ≤ is only assumed to be a preorder, we can prove that the strict order is irreflexive and transitive. In the second example, for convenience, we use the simplifier rather than rw to express < in terms of ≤ and ¬. We will come back to the simplifier later, but here we are only relying on the fact that it will use the indicated lemma repeatedly, even if it needs to be instantiated to different values.

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

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

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

3.5. Disjunction

The canonical way to prove a disjunction A ∨ B is to prove A or to prove B. The left tactic chooses A, and the right tactic chooses 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]

We cannot use an anonymous constructor to construct a proof of an “or” because Lean would have to guess which disjunct we are trying to prove. When we write proof terms we can use Or.inl and Or.inr instead to make the choice explicitly. Here, inl is short for “introduction left” and inr is short for “introduction right.”

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

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

It may seem strange to prove a disjunction by proving one side or the other. In practice, which case holds usually depends on a case distinction that is implicit or explicit in the assumptions and the data. The rcases tactic allows us to make use of a hypothesis of the form A ∨ B. In contrast to the use of rcases with conjunction or an existential quantifier, here the rcases tactic produces two goals. Both have the same conclusion, but in the first case, A is assumed to be true, and in the second case, B is assumed to be true. In other words, as the name suggests, the rcases tactic carries out a proof by cases. As usual, we can tell Lean what names to use for the hypotheses. In the next example, we tell Lean to use the name h on each branch.

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

Notice that the pattern changes from ⟨h₀, h₁⟩ in the case of a conjunction to h₀ | h₁ in the case of a disjunction. Think of the first pattern as matching against data the contains both an h₀ and a h₁, whereas second pattern, with the bar, matches against data that contains either an h₀ or h₁. In this case, because the two goals are separate, we have chosen to use the same name, h, in each case.

The absolute value function is defined in such a way that we can immediately prove that x ≥ 0 implies |x| = x (this is the theorem abs_of_nonneg) and x < 0 implies |x| = -x (this is abs_of_neg). The expression le_or_gt 0 x establishes 0 ≤ x ∨ x < 0, allowing us to split on those two cases.

Lean also supports the computer scientists’ pattern-matching syntax for disjunction. Now the cases tactic is more attractive, because it allows us to name each case, and name the hypothesis that is introduced closer to where it is used.

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

The names inl and inr are short for “intro left” and “intro right,” respectively. Using case has the advantage that you can prove the cases in either order; Lean uses the tag to find the relevant goal. If you don’t care about that, you can use next, or match, or even a pattern-matching 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

In the case of match, we need to use the full names Or.inl and Or.inr of the canonical ways to prove a disjunction. In this textbook, we will generally use rcases to split on the cases of a disjunction.

Try proving the triangle inequality using the first two theorems in the next snippet. They are given the same names they have in Mathlib.

namespace MyAbs

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

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

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

In case you enjoyed these (pun intended) and you want more practice with disjunction, try these.

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

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

You can also use rcases and rintro with nested disjunctions. When these result in a genuine case split with multiple goals, the patterns for each new goal are separated by a vertical bar.

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

You can still nest patterns and use the rfl keyword to substitute equations:

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

See if you can prove the following with a single (long) line. Use rcases to unpack the hypotheses and split on cases, and use a semicolon and linarith to solve each branch.

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

On the real numbers, an equation x * y = 0 tells us that x = 0 or y = 0. In Mathlib, this fact is known as eq_zero_or_eq_zero_of_mul_eq_zero, and it is another nice example of how a disjunction can arise. See if you can use it to prove the following:

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

Remember that you can use the ring tactic to help with calculations.

In an arbitrary ring \(R\), an element \(x\) such that \(x y = 0\) for some nonzero \(y\) is called a left zero divisor, an element \(x\) such that \(y x = 0\) for some nonzero \(y\) is called a right zero divisor, and an element that is either a left or right zero divisor is called simply a zero divisor. The theorem eq_zero_or_eq_zero_of_mul_eq_zero says that the real numbers have no nontrivial zero divisors. A commutative ring with this property is called an integral domain. Your proofs of the two theorems above should work equally well in any integral domain:

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

In fact, if you are careful, you can prove the first theorem without using commutativity of multiplication. In that case, it suffices to assume that R is a Ring instead of an CommRing.

Sometimes in a proof we want to split on cases depending on whether some statement is true or not. For any proposition P, we can use em P : P ∨ ¬ P. The name em is short for “excluded middle.”

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

Alternatively, you can use the by_cases tactic.

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

Notice that the by_cases tactic lets you specify a label for the hypothesis that is introduced in each branch, in this case, h' : P in one and h' : ¬ P in the other. If you leave out the label, Lean uses h by default. Try proving the following equivalence, using by_cases to establish one direction.

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

3.6. Sequences and Convergence

We now have enough skills at our disposal to do some real mathematics. In Lean, we can represent a sequence \(s_0, s_1, s_2, \ldots\) of real numbers as a function s : ℕ → ℝ. Such a sequence is said to converge to a number \(a\) if for every \(\varepsilon > 0\) there is a point beyond which the sequence remains within \(\varepsilon\) of \(a\), that is, there is a number \(N\) such that for every \(n \ge N\), \(| s_n - a | < \varepsilon\). In Lean, we can render this as follows:

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

The notation ∀ ε > 0, ... is a convenient abbreviation for ∀ ε, ε > 0 → ..., and, similarly, ∀ n ≥ N, ... abbreviates ∀ n, n ≥ N →  .... And remember that ε > 0, in turn, is defined as 0 < ε, and n ≥ N is defined as N ≤ n.

In this section, we’ll establish some properties of convergence. But first, we will discuss three tactics for working with equality that will prove useful. The first, the ext tactic, gives us a way of proving that two functions are equal. Let \(f(x) = x + 1\) and \(g(x) = 1 + x\) be functions from reals to reals. Then, of course, \(f = g\), because they return the same value for every \(x\). The ext tactic enables us to prove an equation between functions by proving that their values are the same at all the values of their arguments.

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

We’ll see later that ext is actually more general, and also one can specify the name of the variables that appear. For instance you can try to replace ext with ext u v in the above proof. The second tactic, the congr tactic, allows us to prove an equation between two expressions by reconciling the parts that are different:

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

Here the congr tactic peels off the abs on each side, leaving us to prove a = a - b + b.

Finally, the convert tactic is used to apply a theorem to a goal when the conclusion of the theorem doesn’t quite match. For example, suppose we want to prove a < a * a from 1 < a. A theorem in the library, mul_lt_mul_right, will let us prove 1 * a < a * a. One possibility is to work backwards and rewrite the goal so that it has that form. Instead, the convert tactic lets us apply the theorem as it is, and leaves us with the task of proving the equations that are needed to make the goal match.

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

This example illustrates another useful trick: when we apply an expression with an underscore and Lean can’t fill it in for us automatically, it simply leaves it for us as another goal.

The following shows that any constant sequence \(a, a, a, \ldots\) converges.

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 has a tactic, simp, which can often save you the trouble of carrying out steps like rw [sub_self, abs_zero] by hand. We will tell you more about it soon.

For a more interesting theorem, let’s show that if s converges to a and t converges to b, then fun n ↦ s n + t n converges to a + b. It is helpful to have a clear pen-and-paper proof in mind before you start writing a formal one. Given ε greater than 0, the idea is to use the hypotheses to obtain an Ns such that beyond that point, s is within ε / 2 of a, and an Nt such that beyond that point, t is within ε / 2 of b. Then, whenever n is greater than or equal to the maximum of Ns and Nt, the sequence fun n ↦ s n + t n should be within ε of a + b. The following example begins to implement this strategy. See if you can finish it off.

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

As hints, you can use le_of_max_le_left and le_of_max_le_right, and norm_num can prove ε / 2 + ε / 2 = ε. Also, it is helpful to use the congr tactic to show that |s n + t n - (a + b)| is equal to |(s n - a) + (t n - b)|, since then you can use the triangle inequality. Notice that we marked all the variables s, t, a, and b implicit because they can be inferred from the hypotheses.

Proving the same theorem with multiplication in place of addition is tricky. We will get there by proving some auxiliary statements first. See if you can also finish off the next proof, which shows that if s converges to a, then fun n ↦ c * s n converges to c * a. It is helpful to split into cases depending on whether c is equal to zero or not. We have taken care of the zero case, and we have left you to prove the result with the extra assumption that c is nonzero.

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

The next theorem is also independently interesting: it shows that a convergent sequence is eventually bounded in absolute value. We have started you off; see if you can finish it.

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

In fact, the theorem could be strengthened to assert that there is a bound b that holds for all values of n. But this version is strong enough for our purposes, and we will see at the end of this section that it holds more generally.

The next lemma is auxiliary: we prove that if s converges to a and t converges to 0, then fun n ↦ s n * t n converges to 0. To do so, we use the previous theorem to find a B that bounds s beyond some point N₀. See if you can understand the strategy we have outlined and finish the proof.

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

If you have made it this far, congratulations! We are now within striking distance of our theorem. The following proof finishes it off.

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

For another challenging exercise, try filling out the following sketch of a proof that limits are unique. (If you are feeling bold, you can delete the proof sketch and try proving it from scratch.)

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

We close the section with the observation that our proofs can be generalized. For example, the only properties that we have used of the natural numbers is that their structure carries a partial order with min and max. You can check that everything still works if you replace ℕ everywhere by any linear order α:

variable {α : Type*} [LinearOrder α]

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

In Section 10.1, we will see that Mathlib has mechanisms for dealing with convergence in vastly more general terms, not only abstracting away particular features of the domain and codomain, but also abstracting over different types of convergence.