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はこの2つを非常に似た方法で扱っています．特に，このような構造の定理を証明した場合，その定理をモノにもコトにも同じように適用することができます．この事の例として，少しあとで証明する以下の命題を用いましょう:

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

また既に見てきたように，量化された変数が後続の仮定から推測できる場合，波括弧を使って暗黙の変数にすることが一般的です．このようにすると，対象について言及することなく仮定に補題を適用することができます．

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| < δ に適用すると， 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_right を使ってください．Ctrl+スペース（MacではCmd+スペース）での補完を使えば，これらの定理を見つけることができることも覚えてください．また， .mp と .mpr ，または .1 と .2 を使って，同値性を主張する文の十分性の方向と必要性の方向を取り出せることも覚えておきましょう．

全称量化は定義に隠されていることが多く，Leanは必要に応じて定義を展開しそれらの変数を明示します．例えば， FnUb f a と FnLb f a という2つの述語を定義しましょう．ここで 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（定義上）」の略です．）この dsimp コマンドを削除しても証明は機能します; Leanは次の行の apply の意味を理解するために，いずれにせよこの単純化を行います．dsimp コマンドは単にゴールを読みやすくし，次に何をすべきかを考える手助けをしてくれます．別の方法として， change タクティクを用いて change f x + g x ≤ a + b と書くこともできます．これは証明をより読みやすくし，ゴールがどのように変換されるかをコントロールできるようにします．

残りの証明はルーチンワークです．最後の2つの 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 を実数から実数への関数に対して定義しましたが，この定義と証明はもっと一般的です．これらは終域に順序の概念があれば，任意の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 はコロンの後ろの式と全く同じように定義されています．ここで h の前に @ を置く必要があります．こうしないと，Leanは暗黙の引数を h に展開し，プレースホルダーを挿入してしまうからです．

単調性の証明には， intro を使って2つの変数，例えば a と b を導入し， a ≤ b と仮定します．単調性の仮定を 用いる には，適切な引数や仮定に適用し，その結果得られた式をゴールに適用すればよいです．あるいは，直接ゴールに適用すれば，残りの仮定が新しいサブゴールとして表示されて，後方推論のサポートを得ることができます．

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はその式の値を推測できないというエラーを出します．VSCodeのゴールウィンドウを見るか，エラーマーカーの波線にカーソルを合わせると，残っている未解決のゴールが表示されます．

ここで次の定理をタクティクか証明項のどちらかを用いて証明してみましょう:

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\) が 偶関数 （even）であるとはすべての \(x\) に対して \(f(-x) = f(x)\) となることを指し， 奇関数 （odd）であるとはすべての \(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

1つ目の証明は dsimp か change を用いてラムダ抽象を取り除くことで短くすることができます．ここで明示的にラムダ抽象を取り除いておかないと後続の証明で rw がうまく機能しないことが分かります．これは式中に f x や g x のパターンを見つけられなくなるからです．他のいくつかのタクティクとは異なり， rw は構文レベルで動作し定義の展開や式の簡約は行ってくれません．（この方向性に関してもう少し頑張ってくれる erw というタクティクもありますが、これもさほど頑張ってはくれません．）

さて，一度見付け方さえわかれば暗黙の全称量化子はいたるところで見つけることができます．

Mathlibには集合の操作に関する優れたライブラリがあります．Leanは集合論を基礎に置いていないので，ここで言うところの「集合」は何かしらの型 α の数学的対象のあつまりという素朴な意味合いになります．もし x が型 α で， s が Set α 型であるとき， x ∈ s は x が s の要素であることを主張する命題となります．別の型 β の y については，式 y ∈ s は意味をなしません．ここでいう「意味をなさない」とは「型を持たないため，Leanとして合法な（well-formed）命題として受け入れられない」という意味です．これは例えばツェルメロ-フレンケル集合論（ZF）では a ∈ b がすべての数学的対象 a と b に対して合法であることと対照的です．例えば sin ∈ cos もZFでは合法です．集合論のこの欠点が，無意味な式を検知して証明を支援することを意図した証明支援系が集合論を基礎に置かない，大きな理由となっています．Leanにおいて sin は ℝ → ℝ の型を持ち，cos も ℝ → ℝ の型であり，これはたとえ定義を展開したとしても Set (ℝ → ℝ) とは等しくないため，sin ∈ cos という命題は意味をなしません．一方でLeanを使って集合論そのものに取り組むこともできます．例えばZFの公理から連続体仮定が独立していることは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

最後にもう一つ重要な例を挙げて本節を締めくくりましょう．関数 \(f\) が 単射（injective） であるとはすべての \(x_1\) と \(x_2\) について， \(f(x_1) = f(x_2)\) なら \(x_1 = x_2\) であることを指します．Mathlibはこの関係を x₁ と x₂ を暗黙の引数として Function.Injective f という名前で定義しています．次の例は実数上で定数を加える関数が単射であることを示しています．この例中の補題名をヒントに0ではない定数を掛ける関数も単射であることを示しましょう．補題名の先頭を推測したらCtrl+スペースによる補完を使えることに注意してください．

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. 存在量化子

VSCodeで \ex で入力できる存在量化子は「存在する」というフレーズを表現するために使用されます．Leanにおいて ∃ x : ℝ, 2 < x ∧ x < 3 という形式的な式は2と3の間に実数が存在するということを表しています．（連言の記号 ∧ については Section 3.4 にて説明します．）このような命題を証明する標準的な方法は一つ実数を示し，その実数が指定された性質を持つことを示すことです．ここでその実数として2.5を指定し， norm_num タクティクによってこの数が必要な性質を満たしていることを証明できます．ところでこの2.5は実数のつもりで書いていますが，Leanがこれを文脈から推測できない場合は 5 / 2 または (5 : ℝ) / 2 と入力することもできます．

この実際の値とその性質の証明の2つをまとめる方法はいくつかあります．まず1つ目として，存在量化子で始まるゴールがある場合， 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⟩

これで存在についての命題を 証明をする 方法がわかりました．しかしこのような命題はどのように 使う のでしょうか？ある性質を持つ対象が存在することがわかっていれば，その対象の詳細がわからなくても名前を付けて推論することができます．例えば，前節で a が f の上界または下界であることをそれぞれ表していた FnUb f a と FnLb f a という述語を思い出してください．存在量化子を使えば具体的な上界・下界を指定せずに「 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⟩ のような構文は パターン （pattern）と呼ばれ，メインの引数を展開した結果として期待される情報を記述します． 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⟩

1つ目の 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⟩

1つ目の例にて cases ubf の後ろにカーソルを置くと，このタクティクによって intro というタグを付けられた1つのゴールが生成されていることがわかるでしょう．（この intro という名前は存在命題を表すLeanの公理的プリミティブの内部的な名前に由来しています．）これに続く case タクティクがこのコンポーネントに名前を付けています．2つ目の例も似ていますが， case の代わりに next を使うことで， intro に言及することを避けることができます．最後の2つの例の match という単語はここで行っていることが計算機科学において「パターンマッチ」と呼ばれているものであることを強調しています．3つ目の証明は by で始まっていることに注目してください．タクティクバージョンの match の矢印の右側にはタクティクによる証明が来ることが期待されます．最後の例は証明項です: ここではタクティクは一つも見当たりません．

本書ではこれ以降 rcases と rintro ， obtain を存在量化子を扱う好ましい方法として使います．しかし別の構文を見ておいても損はないでしょう．特に計算機科学者と一緒に作業をする可能性があるならなおさらです．

rcases の使い方を例示するにあたって，数学においてすでに語り尽くされてきた事実を証明しましょう: もし2つの整数 x と y がそれぞれ2乗の和として表すことができる場合，その積 x * y も同様に表すことができます．実際にはこの命題は整数に限らず，任意の可換環に対しても成り立ちます．次の例で， 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\) に一致します．したがってガウス整数のノルムは2乗の和で，逆にどんな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\) が 全射 （surjective）であるとは終域 \(\beta\) のすべての \(y\) について， \(f(x) = y\) を満たす始域 \(\alpha\) にある \(x\) が存在することです．この命題では全称量化子と存在量化子の両方を含むことに注目してください．これが次の例で 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_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 という名前を使用します．これはこの対象を後から参照するにあたって便利です．今回の証明はとても短いため，明示的な証明項を用意しています．しかしこの証明において最も注目すべきなのは intro タクティクによってゴールが False となっていること，そして lt_irrefl を a < a に適用することで最終的に 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

もし < を ≤ で置き換えると，すぐ上の1つ目の例の否定が証明できます．全称量化子のついた命題の否定は，反例を示すことで証明できることに注意してください．この証明を完成させてみましょう．

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

この例では 局所的な定義 （local definition）をローカルコンテキストに追加する let タクティクを導入しています． let コマンドの後ろにカーソルを置くと，ゴールウィンドウに f : ℝ → ℝ := fun x ↦ 0 という定義が追加されていることがわかるでしょう．Leanは必要なときに f の定義を展開します．特に f 1 ≤ f 0 を le_refl で証明するとき，Leanは f 1 と f 0 を 0 に展開します．

le_of_not_gt を用いて以下を証明しましょう:

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

今までの証明の中で暗黙のうちに用いてきた事実として，次の2つがあります．任意の性質 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

1つ目と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 を使って証明することができ，逆方向は通常の否定のルールから導かれることを確認しましょう．

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

2つ目の例では， 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には contrapose というタクティクもあり，これは A → B というゴールを ¬B → ¬A に変換します．同様に，仮定 h : A から B を証明するというゴールがある場合， contrapose h を使うと仮定 ¬B から ¬A を証明するというゴールになります． contrapose の代わりに 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. 連言と必要十分条件

「かつ」を表すのに使われている連言の記号 ∧ はもうすでに見てきました． 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 で ≤ の反射性を適用してゴールを終了させていることに注意してください．以下は先程の例を無名コンストラクタを用いて解いた別解です．1つ目の例では証明項中で 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⟩

連言を証明するのではなく 使う には，その連言の証明を2つに展開する必要があります．これは存在量化子に対するのと同じように 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 の2つの構成要素を取り出すために 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

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

1つ目の例では， constructor の後ろのセミコロン <;> によってLeanに2つのゴールのどちらにも norm_num タクティクを用いるように指示しています．

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

さらに興味深い演習問題として，任意の2つの実数 x と y に対して， x^2 + y^2 = 0 が x = 0 と y = 0 の場合にのみ成り立つことを示しましょう．ここでは linarith ， pow_two_nonneg ， 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

Leanでは，双方向の含意には二面性があります．まず，連言のように2つの部分を別々に使うことができます．しかしその一方で，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 を使って，-1 倍する関数が単調増加関数ではないことを簡単に証明できるか試してみましょう．（ push_neg が定義を展開してくれないため，定理の証明には rw [Monotone] が必要であることに注意してください．）

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

本節での最後の演習問題は連言と双方向の含意を練習するためのものです． 半順序 （partial order）は推移的で反射的で反対称的な二項関係であることを思い出してください．これに対してより弱い概念である 前順序 （preorder）は単に反射的で推移的な関係のことです．任意の前順序 ≤ について，Leanは対応する狭義の前順序 a < b を 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_le]
  sorry

論理演算以外では le_refl と le_trans 以外は必要ではありません．ここで ≤ が前順序であることだけを仮定したとしても狭義の順序が非反射的で推移的であることを示しましょう．2つ目の例では， < を ≤ と ¬ を用いて表現するために便宜上 rw ではなく単純化のコマンドを用います．この単純化については後ほど説明しますが，ここでは単純化によって指定された補題はたとえ異なる値についてインスタンス化する必要がある場合でも繰り返し使用されるという事実のみを用います．

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

選言 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 は 2つの ゴールを生成します．どちらのゴールも結論は同じですが，1つ目のケースでは A が真だと仮定され，2つ目のケースでは B が真だと仮定されます．つまり，名前の通り， rcases タクティクは場合分けによる証明を行ってくれます．いつものように，この仮定についてどのような名前を使うかをLeanに指示することができます．次の例では，各ブランチで h という名前を使っています．

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₁ の 両方 を含むデータに対してのマッチングだったのに対して，2つ目の縦棒を用いたパターンは h₀ か h₁ の どちらか を含むデータに対してのマッチングであると考えてください．この場合，2つのゴールは別々になるため，両方で同じ名前 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 を用いると，任意の順番で証明ができるという利点があります．この場合，タグに一致するゴールが選択されます．これらの利点が必要でなければ， 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 を使うことにします．

次のコードの最初の2つの定理を使って三角不等式を証明してみましょう．これらは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

場合分けによる証明を楽しめましたか？もっと練習をすることができます．以下を試してみてください．

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

以下を（長い）1行で証明できるか試してみましょう． 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\) において，あるゼロではない要素 \(y\) に対して \(x y = 0\) を満たすような元 \(x\) を 左零因子 （left zero divisor）と呼び，またあるゼロではない要素 \(y\) に対して \(y x = 0\) を満たすような元 \(x\) を 右零因子 （right zero divisor）と呼び，左零因子または右零因子である要素を単に 零因子 （zero divisor）と呼びます．定理 eq_zero_or_eq_zero_of_mul_eq_zero は実数には0以外に零因子がないことを述べています．この性質を持つ可換環は 整域 （integral domain）と呼ばれます．上の2つの定理の証明はどのような整域でも同じようにうまくいくはずです:

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 タクティクでは各分岐で導入される仮定のラベルを指定できることに注意してください．この場合，1つは h' : P で，もう1つは h' : ¬ P です．ラベルを省略した場合，デフォルトで 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 > 0\) 以内の範囲に収まる場合，この数列は \(a\) に 収束 （converge）すると言います．つまり，すべての \(n \ge N\) に対して \(| s_n - a | < \varepsilon\) となるような数 \(N\) が存在するということです．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 としてそれぞれ定義されるということも覚えておきましょう．

本節では，収束に関していくつかの性質を証明します．しかしその前に，等式を扱う際に役立つ3つのタクティクについて説明しましょう．まず初めに， ext タクティクは2つの関数が等しいことを証明するのに役立ちます．例えば \(f(x) = x + 1\) と \(g(x) = 1 + x\) を実数から実数への関数とします．このとき当たり前ですが，2つの関数はすべての \(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 に置き換えることができます．2つ目のタクティクは congr タクティクで，これは2つの式が等しいということの証明を式中の異なる部分が実は等しいという証明に帰着するものです．

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_right という定理があり，これを使えば 1 * a < a * a を証明することができます．これを用いる方法の一つは，逆算してその形になるようにゴールを書き直すことでしょう．この代わりに convert タクティクは定理をそのまま適用でき，ゴールと定理の差分を埋めるのに必要な等式を，新たな証明すべきゴールとします．

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

この例ではまた別の便利な技法を示しています．アンダースコアを含む式を apply すると，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 に収束することを示しましょう．形式的な証明を始める前に，紙とペンでどう証明するか明確にイメージしておくと良いでしょう．証明の方針は正の数 ε が与えられたとき， s の添え字でそれ以降 s が常に a から ε / 2 以内に収まるような Ns と， t の添え字でそれ以降 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| < ε

Section 10.1 では，Mathlibには収束をより一般的に扱うためのメカニズムが用意されていることを見ていきます．フィルタは始域と終域の特定の特徴を抽象化するだけではなく，様々なタイプの収束を抽象化します．