2. 基礎
この章では，Leanにおける数学的推論の基本を紹介します．計算や補題・定理の適用，一般的な構造についての推論を扱います．
2.1. 計算
私たちは通常，数学的な計算のことを証明と考えずに行うよう学びます．しかし，計算の各ステップを正当化する必要があるLeanの要件に従うと，計算はつまるところ左辺が右辺に等しいという証明であるという結論に行き着きます．
Leanにおいて，定理を述べるということは，その定理を証明するというゴールを述べることと同等です．Leanには，ゴールの左辺をそれと等しい右辺に置き換えるタクティクである rw が存在します．a ， b， c が実数の時， mul_assoc a b c は a * b * c = a * (b * c) という恒等式であり， mul_comm a b は a * b = b * a という恒等式を表しています．Lean には自動化の仕組みがあるので，こうして明示的に事実を参照する必要はないのですが，説明のためには rw が便利です．Leanにおいて，掛け算は左側から計算されます．よって左側にある mul_assoc は (a * b) * c と書くことも可能です．しかしながら，一般的にはLeanの表記規則に倣い，Leanが括弧を省略する場合は括弧を省略するのが良いとされるスタイルです．
rw を試してみましょう！
example (a b c : ℝ) : a * b * c = b * (a * c) := by
rw [mul_comm a b]
rw [mul_assoc b a c]
例題ファイルの先頭にある import 行は，Mathlib から実数の理論や便利なオートメーションをインポートします．簡潔のため，本書では一般的にこのような情報は省略します．自由に変更して，何が起こるのか確認してみてください．VSCodeでは ℝ を \R または \real で入力することができます． ℝ 記号はスペースかタブキーを押すまで表示されません．Leanファイルを読むときに記号の上にカーソルを置くと，VSCodeはその記号を入力するために使用できる構文を表示します．使用可能な略語をすべて見たい場合は，Ctrl+Shift+P を押した後に abbreviations と入力すれば， Lean 4: Show all abbreviations コマンドにアクセスできます．キーボードにバックスラッシュがない場合は， lean4.input.leader の設定を変更することで，先頭の文字を変更することができます．
カーソルがタクティクスタイルの証明の途中にあるとき，Lean は現在の証明の状態を Lean infoview ウィンドウに表示します．カーソルを動かすと，状態が変化するのがわかります．Leanの典型的な証明の状態は以下のようになります：
1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4
⊢ で始まる行の前の行は コンテキスト を表しています．この例では，2つの変数 x と y が含まれており，それぞれが自然数です．また， h₁ ， h₂ ， h₃ とラベル付けされた3つの仮定も含まれます．Leanでは，コンテキスト内のすべてのものに h\1, h\2 などのような識別子が付きます．文法的に正しい識別子であればどのような識別子でも使用することができます．代わりに h\3，\h1 ， \h2 ， \h3 ， h1 ， h2， h3 や foo ， bar ， baz などを使うことが可能です．最後の行はゴール，つまり証明されるべき事実を表しています．証明されるべき事実を target ，コンテキストとゴールの組み合わせを goal と呼ぶこともあります．実際には，意図する意味はたいてい明らかです．それぞれのケースで sorry をタクティクを用いた証明に置き換えて，以下の恒等式を証明してみましょう． rw タクティクを使う際に，左矢印 ( \l ) を使うことで右辺を左辺に書き換えることができます．例えば， rw [← mul_assoc a b c] は現在のゴールを a * (b * c) から a * b * c に置き換えます．左向きの矢印 ← は mul_assoc が提供する等式の向きを変えることを意味し，ゴールの左辺や右辺に影響を与えないことに注意してください．
example (a b c : ℝ) : c * b * a = b * (a * c) := by
sorry
example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
sorry
mul_assoc や mul_comm のような恒等式を引数なしで使うことも可能です．この場合， rw タクティクは最初に見つけたパターンを使って，左辺とゴールの式をマッチさせようとします．
example (a b c : ℝ) : a * b * c = b * c * a := by
rw [mul_assoc]
rw [mul_comm]
部分的な情報 を提供することも可能です．例えば， mul_comm a は a * ? という形の全てのパターンにマッチして，それを ? * a に書き換えます．1個めの例は1つも引数を使用せずに，2個めの例は1つの引数のみを使用して証明してみましょう．
example (a b c : ℝ) : a * (b * c) = b * (c * a) := by
sorry
example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
sorry
ローカルコンテキストにある事実を rw で使用することも可能です．
example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
rw [h']
rw [← mul_assoc]
rw [h]
rw [mul_assoc]
2番目の命題には sub_self を使用してみてください．
example (a b c d e f : ℝ) (h : b * c = e * f) : a * b * c * d = a * e * f * d := by
sorry
example (a b c d : ℝ) (hyp : c = b * a - d) (hyp' : d = a * b) : c = 0 := by
sorry
関連する等式を角括弧の中にカンマで区切って列挙すると，複数の書き換えコマンドを1つのコマンドで実行することが可能です．
example (a b c d e f : ℝ) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
rw [h', ← mul_assoc, h, mul_assoc]
書き換えのリストのカンマの後にカーソルを置くと，次の段階が表示されます．もう1つの小技として，例や定理の外側で変数を一度に宣言できます． そうすると Lean がそれを自動的に取り込みます．
variable (a b c d e f : ℝ)
example (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
rw [h', ← mul_assoc, h, mul_assoc]
上記の証明の最初にあるタクティクの状態を調べると，Leanが確かにすべての変数を取り込んでいることがわかります．宣言のスコープは section ... end ブロックに入れることで区切ることができます．最後に， introduction でご紹介した式の型を決定するコマンドを思い出してください：
section
variable (a b c : ℝ)
#check a
#check a + b
#check (a : ℝ)
#check mul_comm a b
#check (mul_comm a b : a * b = b * a)
#check mul_assoc c a b
#check mul_comm a
#check mul_comm
end
checkコマンドはモノとコトの両方に使用することができます．#check a を実行すると，Lean は a が ℝ 型であることを報告します．#check mul_comm a b を実行すると，Lean は mul_comm a b が a * b = b * a という事実の証明であることを報告します．#check (a : ℝ) は a の型が ℝ であることを確認するもので，もしそうでなければエラーになります．最後の3つの #check コマンドの出力については後ほど説明します．それまで自由に上記のコマンド例を確認したり， 自分で #check コマンドを試したりしてみてください．
もう少し例を挙げてみましょう．定理 two_mul a は 2 * a = a + a を表しています．定理 add_mul と mul_add は足し算に対する掛け算の分配性を表し，定理 add_assoc は足し算の結合則を表しています．正確な記述を見るには #check コマンドを使ってください．
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
rw [mul_add, add_mul, add_mul]
rw [← add_assoc, add_assoc (a * a)]
rw [mul_comm b a, ← two_mul]
この証明で何が起こっているのかをエディター上で読み進めて理解することもできなくはないですが，これだけでは読みにくいことでしょう．Leanでは calc というキーワードを使用して,このような証明をより構造的に書くことができます．
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
(a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
rw [mul_add, add_mul, add_mul]
_ = a * a + (b * a + a * b) + b * b := by
rw [← add_assoc, add_assoc (a * a)]
_ = a * a + 2 * (a * b) + b * b := by
rw [mul_comm b a, ← two_mul]
この証明が by で始まっていないことに注意してください．calc で始まる式は証明項です．calc 式はタクティクスタイルの証明の中で使うこともできますが，Leanはそれを，結果として得られる証明項を使ってゴールを証明するという指示として解釈します．calc の構文は制約の多いものです．下線と空白の入れ方は上記の形式でなければなりません．インデントを使って，タクティクのブロックや calc ブロックの始まりと終わりを決定しています．上の証明のインデントを変えてみてどうなるか見てみましょう．
calc による証明の書き方の一例として，まず各式変形の証明を sorry タクティクで置いて式変形の概要を書き，これをLeanが受け入れることを確認してから sorry としていた各式変形をタクティクで証明していく，というものがあります．
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
(a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
sorry
_ = a * a + (b * a + a * b) + b * b := by
sorry
_ = a * a + 2 * (a * b) + b * b := by
sorry
純粋な rw による証明と，より構造化された calc による証明の両方を使用して，以下の等式を証明してください.
example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
sorry
この後の演習は少し難しいです．下に挙げた定理を使用すると良いでしょう．
example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
sorry
#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a
また，コンテキストにある仮定に対して書き換えを行うことも可能です．例えば， rw [mul_comm a b] at hyp は hyp という仮定の中の a * b を b * a に置き換えます．
example (a b c d : ℝ) (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
rw [hyp'] at hyp
rw [mul_comm d a] at hyp
rw [← two_mul (a * d)] at hyp
rw [← mul_assoc 2 a d] at hyp
exact hyp
最後のステップで exact タクティクで hyp を使ってゴールを達成することができます．なぜなら，その時点で hyp はゴールと完全に一致するからです．
このセクションの最後に，Mathlibが ring タクティクという便利なオートメーションを提供していることに触れておきます．ring は，ローカルの仮定を用いずに純粋に環の公理だけから導かれるような，任意の可換環における恒等式を証明できるように設計されています．
example : c * b * a = b * (a * c) := by
ring
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by
ring
example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
ring
example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
rw [hyp, hyp']
ring
ring タクティクは Mathlib.Data.Real.Basic をインポートしたときに間接的にインポートされています．しかし，次章では実数以外の構造体の計算にも ring タクティクが使用できることを解説していきます． ring は import Mathlib.Tactic コマンドを使用して明示的にインポートすることができます．他の代数的対象にも同様のタクティクがあることを今後見ていきます． nth_rewrite と呼ばれる rw の亜種が存在し，それを使用するとゴール(証明したい命題)の中にある表現のうち特定のものだけを置換することができます．ありうる置換対象は1から順番に列挙されます．次の例では nth_rewrite 2 h は2番目に出現する a + b を c に置換しています．
example (a b c : ℕ) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by
nth_rw 2 [h]
rw [add_mul]
2.2. 代数的構造における等式の証明
数学的に，環は対象の集まりである \(R\) と演算子 \(+\) \(\times\)，定数 \(0\)，\(1\)，そして演算子 \(x \mapsto -x\) の集まりであって，以下を満たすようなものです:
\(R\) は \(+\) に関して \(0\) を加法の単位元，減算を逆元とする アーベル群 ．
乗法に関して結合法則が成り立ち， \(1\) が単位元になる．また乗法と加法に関して分配法則が成り立つ．
Leanでは環の対象の集まりは 型 R として表すことができます．環の公理は以下のようになります．
variable (R : Type*) [Ring R]
#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
#check (add_comm : ∀ a b : R, a + b = b + a)
#check (zero_add : ∀ a : R, 0 + a = a)
#check (add_left_neg : ∀ a : R, -a + a = 0)
#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
#check (mul_one : ∀ a : R, a * 1 = a)
#check (one_mul : ∀ a : R, 1 * a = a)
#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)
上記の1行目に出てきた角括弧については後ほど学びますが，今のところはこの宣言で型 R に対して環の構造が与えられることさえ理解していただければ十分です．これによりLean上で R の元について環の一般的な記法を使うことが可能になり，ライブラリ中の環についての定理も使えるようになります．
これらの定理の名前の中には見覚えがあるものもあるでしょう．それもそのはずで，これらはまさに前章で実数について示したものと同じだからです．Leanは自然数や整数のような具体的な数学的構造についての証明だけでなく，環のような公理的に特徴づけられた抽象的構造についての証明にも長けています．さらに，Leanは抽象的な構造または具体的な構造のどちらに対しても 一般的な推論(generic reasoning) をサポートしており，適切なインスタンスを認識できます．そのため環についての定理を整数 ℤ や有理数 ℚ ，複素数 ℂ のような具体的な環に適用することができます．またさらに順序環や体などの環より特殊な抽象的構造の任意のインスタンスに適用することもできます．
しかし，実数のすべての重要な性質が任意の環で成り立つわけではありません．例えば実数の乗算は可換ですが，これは一般の環では成り立ちません．線形代数の講義を受けたことがある人ならご存じだと思いますが，実数の \(n\) × \(n\) 行列全体は環をなし，この環では通常可換性が成り立ちません．もし R を 可換 環であると宣言すれば，実際に ℝ を R に置き換えても，前節の定理はすべて成り立ちます．
variable (R : Type*) [CommRing R]
variable (a b c d : R)
example : c * b * a = b * (a * c) := by ring
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring
example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring
example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
rw [hyp, hyp']
ring
他のすべての証明が変更なしで通ることを確認するのは読者にお任せします．by ring や by linarith や by sorry のように証明が短い場合，証明は by と同じ行に書くのが一般的です（また文法的にも問題ありません）．簡潔さと読みやすさのバランスを取ることが，証明のスタイルを整えるコツです．
この節のゴールは，前節で身につけたスキルを強化し，環についての公理的推論に応用することです．上に挙げた公理から始め，それを使って他の事実を導きます．本書で証明する事実のほとんどは既にMathlibにあります．Mathlibの内容と命名規則を学ぶのに役立つように，本書で証明するものにも同じ名前を付けます．
Leanは一般的なプログラミング言語で使われるものと同様の 名前空間 によるコードの組織化のメカニズムを提供します．例えば定義や定理 foo が名前空間 bar に導入されると，その完全な名前は bar.foo となります．コマンド open bar で名前空間を 開く ことができ，より短い名前 foo を使えるようになります．名前の衝突によるエラーを避けるために，次の例ではライブラリの定理を MyRing という新しい名前空間に置きます．
次の例は，add_zero や add_right_neg が他の公理から従うことから，環の公理として必要ないことを示しています．
namespace MyRing
variable {R : Type*} [Ring R]
theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]
theorem add_right_neg (a : R) : a + -a = 0 := by rw [add_comm, add_left_neg]
#check MyRing.add_zero
#check add_zero
end MyRing
このように名前空間を分けることの正味の効果は，ライブラリにある定理を一時的に再定義できることです．その後はライブラリにあるバージョンを使い続けることができます．しかし，ごまかしは禁物です！この後の練習問題では，この節で前もって証明する環に関する一般的な事実だけを使うように注意してください．
(注意深い読者なら，(R : Type*) の丸括弧を {R : Type*} の中括弧に変更したことに気づかれたかもしれません．これは R が 暗黙の引数 であることを宣言しています．これが何を意味するかは後ほど説明しますが，ひとまずは気にしないでください)
以下に便利な定理を示します．
theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
rw [← add_assoc, add_left_neg, zero_add]
類似した以下の定理を証明してください:
theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
sorry
これらを以下の証明に用いてください:
theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
sorry
theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
sorry
この2つの証明はそれぞれ3回の書き換えにまとめることが可能です．
ここで中括弧の使い方について説明しましょう．例えば証明のコンテキストに a ， b ， c ，仮定 h : a + b = a + c があり，結論 b = c を導きたいとしましょう．Leanでは，定理を a や b 等の対象に適用するのと同じように仮定や事実に適用することができるため，add_left_cancel a b c h が b = c の証明になると思われるかもしれません．しかし， a ， b ， c を明示的に書くことは引数の与え過ぎであることに注意してください．なぜなら，仮定 h を見るだけで，どういう対象を想定しているか判断できるからです．今回の場合，数文字書くかどうか程度ですので大した負担にはなりませんが，add_left_cancel をさらに複雑な式に適用していく場合には面倒になることでしょう．このような場合のためにLeanでは引数を 暗黙 のものとしてマークすることができます．つまり，その引数は省略され，それを用いている後続の引数や仮定などから推測されるということです．これがまさに {a b c : R} で中括弧にしている理由です．よって，上記の定理の内容から考えると正しい式は add_left_cancel h とシンプルなものとなります．
このことを説明するために，環の公理から a * 0 = 0 が成り立つことを示しましょう．
theorem mul_zero (a : R) : a * 0 = 0 := by
have h : a * 0 + a * 0 = a * 0 + 0 := by
rw [← mul_add, add_zero, add_zero]
rw [add_left_cancel h]
ここでは新しいワザを使っています！ステップごとにinfoviewを見ていけば，この証明で何が起こっているかわかるでしょう．ここで have タクティクは元のゴールと同じコンテキストに新しいゴール a * 0 + a * 0 = a * 0 + 0 を導入しています．この次の行でインデントが1段深くなっていますが，そこにタクティクのブロックを続けると，その内容が新しいゴールの証明と解釈されます．このインデントにより，証明のモジュール化が促進されます．つまり，インデントされた部分が have で導入されたゴールの証明になります．インデントを抜けると，新しい仮定 h が追加され，自由に利用できる状態で元のゴールの証明が再開します．この時点で，ゴールはちょうど add_left_cancel h が使える状態となります．
上記の証明の終わりに rw を用いていますが，代わりに apply add_left_cancel h もしくは exact add_left_cancel h で証明を終えることもできます．exact タクティクは引数として与えられた証明項をそのまま使って現在のゴールを証明しようとします．新たなゴールを生成することはありません．これに対し apply タクティクの引数は完全な証明である必要はありません．証明の足りない部分はLeanにより自動的に推測されるか，新たなゴールとなります． exact は apply よりも真に弱いので， exact を使うのは技術的には冗長です． しかし exact を使うことで証明のコードが少し読みやすくなりますし，ライブラリが変更されたときの保守も容易になります．
ところで乗算は可換であるとは仮定されていないことを思い出してください．このため次の定理は公理から直接導かれず，証明にもひと工夫必要になります．
theorem zero_mul (a : R) : 0 * a = 0 := by
sorry
ここまでくれば，次の演習問題でも各 sorry を証明に置き換えることができるでしょう．この節で示した環に関する事実だけを用います．
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
sorry
theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
sorry
theorem neg_zero : (-0 : R) = 0 := by
apply neg_eq_of_add_eq_zero
rw [add_zero]
theorem neg_neg (a : R) : - -a = a := by
sorry
ここで3つ目の定理においては単に 0 とするのではなく， (-0 : R) と注釈をつける必要があります．なぜなら R を指定しなければLeanはどの環での 0 を念頭においているかを推測することができず，結果デフォルトの挙動として 0 を自然数として解釈してしまうからです．
環においての引き算は加法の逆元との足し算と等しいことがLeanで証明できます．
example (a b : R) : a - b = a + -b :=
sub_eq_add_neg a b
実数においてはまさにそのように 定義されています ．
example (a b : ℝ) : a - b = a + -b :=
rfl
example (a b : ℝ) : a - b = a + -b := by
rfl
証明項 rfl は「反射性（reflexivity）」の略です．これを a - b = a + -b の証明として提示すると，Leanはその定義を展開し，両辺が同じであることを認識します．rfl タクティクもこれと同様です．これは definitional equality(定義からの等価性) として知られているLeanの基礎にある論理の一例です．つまり sub_eq_add_neg を用いて等式 a - b = a + -b を示せるだけでなく，実数を扱うときなど文脈によってはこの等式の両辺を同じ意味で使うことができます．ここまでの情報で，例えば前節の定理 self_sub はもう証明できます:
theorem self_sub (a : R) : a - a = 0 := by
sorry
rw を用いて証明してみましょう．また R を任意の環ではなく実数とすれば， apply または exact を使っても証明することができます．
Leanはどんな環でも 1 + 1 = 2 が成り立つことを知っています．そしてさらに少し努力すれば，この事実を使って前節の定理 two_mul を証明することができます:
theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
norm_num
theorem two_mul (a : R) : 2 * a = a + a := by
sorry
本節を締めくくるにあたって，上で証明した加算と減算に関する事実の中には，環の公理のすべてを必要とするわけではないものや，加算の可換性さえも必要としないものがあることについて見ていきましょう．この環よりも弱い概念である 群 は次のように公理化できます:
variable (A : Type*) [AddGroup A]
#check (add_assoc : ∀ a b c : A, a + b + c = a + (b + c))
#check (zero_add : ∀ a : A, 0 + a = a)
#check (add_left_neg : ∀ a : A, -a + a = 0)
群の演算が可換な場合は加法的表記を使い，そうでない場合は乗法的表記を使うのが一般的です．そのためLeanは加法バージョンの群と同様に乗法バージョンの群も定義しています．（またこれらのアーベリアンなバリエーションである AddCommGroup と CommGroup についても定義しています．）
variable {G : Type*} [Group G]
#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (mul_left_inv : ∀ a : G, a⁻¹ * a = 1)
もし腕に自信があるならこれらの公理だけを用いて群に関する以下の事実を証明してみましょう．その過程でいくつか補助的な補題を証明する必要があります．また本節でこれまで行ってきた証明がヒントになります．
theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := by
sorry
theorem mul_one (a : G) : a * 1 = a := by
sorry
theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
sorry
これらの補題を明示的に呼び出すのは面倒であるため，Mathlibには上記の補題のほとんどのケースをカバーするような ring に似たタクティクがあります: group は非可換乗法群， abel は加法群，そして noncomm_ring は非可換環をカバーします．代数的構造が Ring や CommRing と呼ばれている一方で，タクティクが noncomm_ring と ring と名付けられているのは奇妙に感じられるかもしれません．これには歴史的な理由もありますが，可換環を扱う場合のほうが多いため，可換環を扱うタクティクにより短い名前を付けた方が便利だからという理由もあります．
2.3. 定理と補題を使う
書き換えは等式を証明するのには良いですが，それ以外の定理についてはどうでしょうか？例えば， \(b \le c\) であるときに \(a + e^b \le a + e^c\) という不等式はどのように証明できるでしょうか？これまで見てきたように，定理は仮定や変数を引数に取ることができ， apply や exact タクティクと組み合わせてゴールを解決することができます．この節では，これらのツールをうまく使っていきましょう．
Mathlibにある定理 le_refl と le_trans について考えてみましょう．
#check (le_refl : ∀ a : ℝ, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
詳しくは Section 3.1 で説明しますが， → は右結合であるため命題 le_trans は a ≤ b → (b ≤ c → a ≤ c) と解釈されます．ライブラリの設計上 le_trans において a ， b ， c は暗黙の引数として設定されているため， le_trans にこれらの引数を（後述するように，意図的に要求する場合を除いて）明示的に渡すことは できません ．その代わり，Leanはこれらの引数を使用されている文脈から推測しようとします．例えば，仮定 h : a ≤ b と h' : b ≤ c が文脈にある場合，以下のコードはすべて通ります:
variable (h : a ≤ b) (h' : b ≤ c)
#check (le_refl : ∀ a : Real, a ≤ a)
#check (le_refl a : a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (le_trans h : b ≤ c → a ≤ c)
#check (le_trans h h' : a ≤ c)
apply タクティクは一般的な命題や含意の証明を受け取り，結論を現在のゴールにマッチさせようとし，もし仮定が残る場合はそれを新しいゴールとします．もし与えられた証明がゴールに正確に一致する場合（ 定義上 等しい変形が残っている場合も含みます），apply の代わりに exact タクティクを使うことができます．したがって次のように書けます:
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
apply le_trans
· apply h₀
. apply h₁
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
apply le_trans h₀
apply h₁
example (x y z : ℝ) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
le_trans h₀ h₁
example (x : ℝ) : x ≤ x := by
apply le_refl
example (x : ℝ) : x ≤ x :=
le_refl x
最初の例では， le_trans を apply することで2つのゴールが作成され，それぞれの証明がどこから始まるかをドット [1] で表しています．ここでドットは必須ではありませんが，ドットを使用することで特定のゴールに 焦点があてられます :ドットに続くブロック内ではinfoviewにゴールは一つしか表示されず，かつこのゴールはブロックが終わるまでに完了しなければなりません．ここでは,最初のブロックは2つめのドットから新しいブロックが始まることによって終了しています．インデントすることなく証明することも可能です．4つ目と最後の例では完全にタクティクモードを避けています: le_trans h₀ h₁ と le_refl x が必要な証明項です．
ここでさらにいくつかライブラリの定理を紹介しましょう:
#check (le_refl : ∀ a, a ≤ a)
#check (le_trans : a ≤ b → b ≤ c → a ≤ c)
#check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
#check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
#check (lt_trans : a < b → b < c → a < c)
上記の命題と apply と exact を用いることで以下を証明しましょう:
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
sorry
実は，Leanにはこのようなことを自動的に行うタクティクがあります:
example (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by
linarith
linarith タクティクは 線形算術 を扱えるように設計されています．
example (h : 2 * a ≤ 3 * b) (h' : 1 ≤ a) (h'' : d = 2) : d + a ≤ 5 * b := by
linarith
コンテキスト中にある等式と不等式に加えて， linarith は引数として渡した追加の不等式を使用します．次の例ではこのあとすぐ説明するように， exp_le_exp.mpr h' が exp b ≤ exp c の証明です．Leanでは引数 x に関数 f を適用した結果を表すために f x と記載しますが，これは引数 x に事実や定理 h を適用した結果を表すために h x と書くのと全く同じです．関数適用に括弧は基本的に不要ですが，f (x + y) のように複合的な引数の場合には必要となります．この場合括弧がないと， f x + y は (f x) + y と解釈されます．
example (h : 1 ≤ a) (h' : b ≤ c) : 2 + a + exp b ≤ 3 * a + exp c := by
linarith [exp_le_exp.mpr h']
ここで実数上の不等式を示すために有用なライブラリの定理をさらに紹介しましょう．
#check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
#check (exp_lt_exp : exp a < exp b ↔ a < b)
#check (log_le_log : 0 < a → 0 < b → (log a ≤ log b ↔ a ≤ b))
#check (log_lt_log : 0 < a → a < b → log a < log b)
#check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
#check (add_le_add_right : a ≤ b → ∀ c, a + c ≤ b + c)
#check (add_lt_add_of_le_of_lt : a ≤ b → c < d → a + c < b + d)
#check (add_lt_add_of_lt_of_le : a < b → c ≤ d → a + c < b + d)
#check (add_lt_add_left : a < b → ∀ c, c + a < c + b)
#check (add_lt_add_right : a < b → ∀ c, a + c < b + c)
#check (add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b)
#check (add_pos : 0 < a → 0 < b → 0 < a + b)
#check (add_pos_of_pos_of_nonneg : 0 < a → 0 ≤ b → 0 < a + b)
#check (exp_pos : ∀ a, 0 < exp a)
#check add_le_add_left
上記の定理の中で， exp_le_exp と exp_lt_exp ， log_le_log は必要十分条件を意味する 双方向の含意 を用いています．（VSCodeでは \lr か \iff で入力することができます）．この論理結合子については次の章で詳しく説明することとします．このような定理は rw と一緒に使うことで，ゴールをそれと等価なものに書き換えることができます:
example (h : a ≤ b) : exp a ≤ exp b := by
rw [exp_le_exp]
exact h
しかし，本節では h : A ↔ B が同値命題の証明である場合， h.mp は順方向の A → B の証明に，h.mpr は逆方向の B → A の証明になるという事実の方を使っていきます．ここで mp は「modus ponens」を表し， mpr は「modus ponens reverse」を表しています．また h.mp と h.mpr の代わりにそれぞれ h.1 と h.2 を使うこともできます．以上から次の証明が成り立ちます:
example (h₀ : a ≤ b) (h₁ : c < d) : a + exp c + e < b + exp d + e := by
apply add_lt_add_of_lt_of_le
· apply add_lt_add_of_le_of_lt h₀
apply exp_lt_exp.mpr h₁
apply le_refl
最初の行の apply add_lt_add_of_lt_of_le では2つのゴールが作られ，ここでもドットを使って1つ目と2つ目の証明を分けています．
次の例は読者自身で試してみてください．真ん中の例では norm_num というタクティクが具体的な数値についてのゴールを解決するために使えることを示しています．
example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by sorry
example : (0 : ℝ) < 1 := by norm_num
example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
have h₀ : 0 < 1 + exp a := by sorry
have h₁ : 0 < 1 + exp b := by sorry
apply (log_le_log h₀ h₁).mpr
sorry
ここまで見てきた例題から明らかなように，ライブラリから必要な定理を見つけられることは形式化において重要です．これに当たって，取りうる手段はたくさんあります:
Mathlibの GitHub repository をブラウザで見ることができます．
Mathlibの web pages にあるAPIのドキュメントから探すこともできます．
Mathlibの定理はある程度命名規則が決まっているのでそれを元に定理名が推測できるほか，ある程度定理名を推理して入力した上でCtrl+スペースキー（MacではCmd+スペース）を押せばエディタで定理名を補完することができます．Leanでは，
A_of_B_of_Cという名前の定理はBとCという形の仮定から何かAという形のことが示せるという主張で，そしてこのA，B，Cはゴールを読み上げたときの文におおよそ近いことが多いです．つまり，例えばx + y ≤ ...というような形の定理はおそらくadd_leで始まる可能性が高いのです．そこでadd_leまで入力し，Ctrl+スペースを押せば有益な選択肢が表示されることでしょう．ここでCtrl+スペースを2回押すとさらに利用可能な補完についての詳細情報が表示されることにも注意してください．VSCode上で既存の定理名を右クリックして出てくるオプション中に，その定理が定義されているファイル中の位置に飛ぶ選択肢があるため，それを利用してその定理の近くにある類似の定理を探すことができます．
apply?タクティクを使うことでライブラリ中の関連する定理を探すことも可能です．
example : 0 ≤ a ^ 2 := by
-- apply?
exact sq_nonneg a
この例で exact の行を削除し，その前の行のコメントアウトを外して apply? の挙動を確認してみてください．これらの便利なツールを使って次の例でも必要な定理が見つかるかどうか試してみましょう:
example (h : a ≤ b) : c - exp b ≤ c - exp a := by
sorry
同じ技法を使って， apply? の代わりに linarith を使って証明を終えることができるか確認してみてください．
以下さらに別の不等式の例を挙げます:
example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
calc
a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
calc
2 * a * b = 2 * a * b + 0 := by ring
_ ≤ 2 * a * b + (a ^ 2 - 2 * a * b + b ^ 2) :=
add_le_add (le_refl _) h
_ = a ^ 2 + b ^ 2 := by ring
Mathlibでは * や ^ のような二項演算子の周りにはスペースを開ける傾向がありますが，ここではそこを詰めることで可読性を上げています．この例では注目すべき点がいくつもあります．まず， s ≥ t は定義上 t ≤ s と等価です．原則としてこの2つは互換性があるべきでしょう．しかし，Leanの自動証明の機構の中にはこの同値性を認識しないものもあるため，Mathlibは ≥ よりも ≤ をより優先する傾向があります．第二に， ring タクティクをかなり多用しています．これはとても時間の節約になります！そして最後に，2番めの calc の証明の2行目で by exact add_le_add (le_refl _) h と書く代わりに，証明項 add_le_add (le_refl _) h をそのまま書けばよいことに注意してください．
実際，上記の証明で唯一ひらめきを要するのは仮定 h を見出すことだけです．それさえわかれば，2つ目の計算は線形演算だけで，これは linarith で処理できます:
example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
calc
a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
linarith
なんて素晴らしいのでしょうか！これらのアイデアをもとに次の定理を証明してみてください．この定理では abs_le'.mpr を使うことができます．
example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
sorry
#check abs_le'.mpr
これをついに解くことができたのなら…おめでとうございます！あなたは形式化の達人への道を順調に歩めています．
2.4. applyとrwをさらに活用する
実数上の関数 min は以下の3つの事実により一意に特徴付けられます:
#check (min_le_left a b : min a b ≤ a)
#check (min_le_right a b : min a b ≤ b)
#check (le_min : c ≤ a → c ≤ b → c ≤ min a b)
これらから max 関数を同じように特徴づける定理の名称が想像つくでしょうか？
ここで min を引数 a と b のペアに適用するにあたり min (a, b) ではなく min a b と書かなければならない点に注意してください．形式的には min は ℝ → ℝ → ℝ 型の関数です．このように複数の矢印を用いた型を記述する場合，この矢印は慣例的に右結合として ℝ → (ℝ → ℝ) と解釈されます．この結果， a と b が ℝ 型の場合， min a は ℝ → ℝ 型となり， min a b は ℝ 型を持つため min は期待通り2引数の関数として振る舞います．このような方法で複数の引数を取り扱うことは，論理学者のHaskell Curryにちなんで カリー化 として知られています．
またLeanの演算子の優先順位についても慣れが必要です．関数適用は中置演算子より強く式と結びつくため， min a b + c という式は (min a b) + c と解釈されます．これらの慣例は時間が経てば自然と身につくでしょう．
le_antisymm を使用することで，2つの実数 a, b が等しいのは a ≤ b かつ a ≥ b の場合であることを示すことができます．これと上記の事実を使えば min が可換であることを示すことができます:
example : min a b = min b a := by
apply le_antisymm
· show min a b ≤ min b a
apply le_min
· apply min_le_right
apply min_le_left
· show min b a ≤ min a b
apply le_min
· apply min_le_right
apply min_le_left
ここでは異なるゴールの証明を区切るためにドットを用いています．ここでのドットの使い方は一貫していません:外側のレベルでは両方のゴールにドットとインデントを用いていますが，入れ子になった証明ではゴールが一つになったらドットは使用していません．どちらの書き方も合理的で有用です．また show タクティクを使って証明を構成し，各ブロックで何を証明したいかを明示的にしています． show コマンドを使わなくても証明は機能しますが，これにより証明が読みやすくなり，保守もしやすくなります．
この証明では同じようなことを繰り返していることが気になるかもしれません．あとで詳しく学びますが，繰り返しを避ける一つの方法として局所的な補題を示して利用する方法を記します:
example : min a b = min b a := by
have h : ∀ x y : ℝ, min x y ≤ min y x := by
intro x y
apply le_min
apply min_le_right
apply min_le_left
apply le_antisymm
apply h
apply h
全称量化子については Section 3.1 で詳しく述べますが，今の時点では仮説 h は任意の x と y に対して目的の不等式が成り立っていて，intro タクティクは任意の x と y を導入して結論を導いていると理解できていれば十分です． le_antisymm のあとの最初の apply は暗黙的に h a b を用いており，2つめでは h b a を使っています．
繰り返しを避ける他の手段として repeat タクティクを用いる方法もあります．これはタクティク（や証明のブロック）をできるだけ繰り返し適用するタクティクです．
example : min a b = min b a := by
apply le_antisymm
repeat
apply le_min
apply min_le_right
apply min_le_left
上記の手法を用いるかどうかは自由ですが，次の演習問題は証明することをおすすめします:
example : max a b = max b a := by
sorry
example : min (min a b) c = min a (min b c) := by
sorry
もちろん， max 関数の結合性を証明してみるのも良いでしょう．
乗法が加法に対して分配法則を満たすように min 関数が max に対して分配法則を満たし，その逆も成り立つというのは興味深い事実です．言い換えれば，実数上において min a (max b c) ≤ max (min a b) (min a c) が成り立ち，この式の max と min を入れ替えた同様の式も成り立つということです．しかし次の節では， ≤ の推移性と反射性，そして上記で示した min と max を特徴付ける性質からこれが 成り立たない ことを見ていきます．この性質を示すには実数上の関係 ≤ が 全順序 であること，つまり ∀ x y, x ≤ y ∨ y ≤ x という性質が成り立つという事実を利用する必要があります．ここで記号 ∨ は選言記号で「または」を表します．最初のケースでは min x y = x となり，2番めのケースでは min x y = y となります．場合分けを使って証明する方法は Section 3.5 で学びますが，現時点では場合分けをする必要のない例で説明します．
以下に一つ例を挙げましょう:
theorem aux : min a b + c ≤ min (a + c) (b + c) := by
sorry
example : min a b + c = min (a + c) (b + c) := by
sorry
ここで等式を示すために必要な2つの不等式のうち aux がその片方を示しているのは明白ですが，適切な値に適用することでもう一方向の不等式も得られます．ヒント: 定理 add_neg_cancel_right と linarith タクティクが役に立つでしょう．
Leanの命名規則はライブラリ中の三角不等式の名前にはっきりと現れています:
#check (abs_add : ∀ a b : ℝ, |a + b| ≤ |a| + |b|)
これを用いて以下の類似の定理を証明しましょう:
example : |a| - |b| ≤ |a - b| :=
sorry
end
この証明を3行以内にできるかどうか試してみましょう．この証明では sub_add_cancel を用いると良いでしょう．
本節で取り上げるもう一つの重要な関係として x ∣ y で表される自然数の整除関係があります．要注意: 整除記号はキーボードにある普通の縦棒 ではありません ．これはVSCodeでは \| で入力されるUnicode文字です．慣例としてMathlibでは定理名の中で整除関係を表すのに dvd を使用します．
example (h₀ : x ∣ y) (h₁ : y ∣ z) : x ∣ z :=
dvd_trans h₀ h₁
example : x ∣ y * x * z := by
apply dvd_mul_of_dvd_left
apply dvd_mul_left
example : x ∣ x ^ 2 := by
apply dvd_mul_left
最後の例では，指数が自然数であり dvd_mul_left を apply することでLeanに x^2 の定義を x * x^1 に展開させています．次の例を証明するのに必要な定理名を推測してみましょう:
example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
sorry
end
整除について 最大公約数 gcd と 最小公倍数 lcm はそれぞれ min と max に対応しています．すべての数は 0 を割り切るため，実際 0 は整除において最大の要素です:
variable (m n : ℕ)
#check (Nat.gcd_zero_right n : Nat.gcd n 0 = n)
#check (Nat.gcd_zero_left n : Nat.gcd 0 n = n)
#check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0)
#check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0)
次の例についても証明に必要な定理名を推測してみましょう:
example : Nat.gcd m n = Nat.gcd n m := by
sorry
ヒント: ここでは dvd_antisymm を使うこともできますが，その場合Leanは一般的な定理と，自然数専用の Nat.dvd_antisymm とどちらを用いるのか曖昧であると文句を言ってきます．どちらでも証明できますが，もし一般的な定理のほうを用いたい場合は _root_.dvd_antisymm で指定可能です．
2.5. 代数構造についての事実の証明
Section 2.2 では，実数上で成り立つ多くの一般的な恒等式が，可換環のようなより一般的な代数的構造のクラスでも成り立つことを確認しました．等式だけでなく，代数的構造を記述するために必要な公理はなんでも表現することができます．例えば 半順序 は実数上の ≤ のような，集合上の反射的で推移的な二項関係のことです．Leanはこの半順序を表現できます:
variable {α : Type*} [PartialOrder α]
variable (x y z : α)
#check x ≤ y
#check (le_refl x : x ≤ x)
#check (le_trans : x ≤ y → y ≤ z → x ≤ z)
ここではMathlibの慣例に則り α や β ， γ （ \a ， \b ， \g と入力します）等の文字で任意の型を表すものとします．Mathlibでは環や群のような代数的構造の台集合を表す際にそれぞれ R や G をよく使いますが，一般的な型，特にその型に構造が入っていない場合にはギリシャ文字が使われます．
一般の半順序 ≤ に関連して，実数上における < のような働きをする 狭義半順序 < も存在します．この順序関係において x が y より小さいというのは y 以下でかつ y と等しくないということと同じです．
#check x < y
#check (lt_irrefl x : ¬x < x)
#check (lt_trans : x < y → y < z → x < z)
#check (lt_of_le_of_lt : x ≤ y → y < z → x < z)
#check (lt_of_lt_of_le : x < y → y ≤ z → x < z)
example : x < y ↔ x ≤ y ∧ x ≠ y :=
lt_iff_le_and_ne
この例では，記号 ∧ は「かつ」を表し， ¬ は「否定」を， x ≠ y は ¬ (x = y) の省略形をそれぞれ表しています．Chapter 3 では，これらの論理結合子を用いて < が上記で示された性質を持っていることを 証明 する方法を学びます．
半順序集合の構造に加えて，実数上の min と max に対応するような演算子 ⊓ と ⊔ を持つ構造を 束 と呼びます:
variable {α : Type*} [Lattice α]
variable (x y z : α)
#check x ⊓ y
#check (inf_le_left : x ⊓ y ≤ x)
#check (inf_le_right : x ⊓ y ≤ y)
#check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)
#check x ⊔ y
#check (le_sup_left : x ≤ x ⊔ y)
#check (le_sup_right : y ≤ x ⊔ y)
#check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z)
⊓ と ⊔ はその特徴からそれぞれ 最大下界 と 最小上界 と呼ばれます．VSCodeでは \glb と \lub と打ち込むことで使用できます．またこれらの記号はしばしば 下限 と 上限 と呼ばれ，Mathlibの定理名では inf や sup と書かれます．さらにややこしいことに，これらは 交わり と 結び とも呼ばれます．そのため，束を扱う際には以下の辞書を頭に入れておく必要があります:
⊓は 最大下界 ， 下限 ， 交わり のこと⊔は 最小上界 ， 上限 ， 結び のこと
束の例としては以下のようなものがあります:
整数や実数上の
≤のような任意の全順序でのminとmax．部分集合のあつまりにおける順序
⊆での∩と∪．真偽値について
x ≤ yをxが偽かyが真である [2] という関係としたときの∧と∨．自然数（やもしくは正の整数）についての整除関係
∣による半順序でのgcdとlcm．ベクトル空間の線形部分空間のあつまりも包含関係を半順序として束になります: 最大下界は共通部分で与えられ，最小上界は2つの空間の和で与えられます．
ある集合（もしくはLeanではTypeのこと）上の位相のあつまりは，包含関係の逆を順序として束になります: 2つの位相の最大下界はその和から生成される位相で，最小上界はその2つの共通部分です．
min / max と gcd / lcm と同様に，下限と上限の可換性と結合性をそれらの公理と le_refl と le_trans を用いて証明することができます．
example : x ⊓ y = y ⊓ x := by
sorry
example : x ⊓ y ⊓ z = x ⊓ (y ⊓ z) := by
sorry
example : x ⊔ y = y ⊔ x := by
sorry
example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) := by
sorry
これらの定理はそれぞれ inf_comm ， inf_assoc ， sup_comm ， sup_assoc という名前でMathlib中に定義されています．
これらの公理のみを用いて 吸収則 を証明するのもまたいい演習となるでしょう:
theorem absorb1 : x ⊓ (x ⊔ y) = x := by
sorry
theorem absorb2 : x ⊔ x ⊓ y = x := by
sorry
これらの定理はMathlib中に inf_sup_self と sup_inf_self という名前で存在します．
束の中でも追加で x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z) と x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) を満たすものを 分配束 と呼びます．Leanはこれらも表現できます:
variable {α : Type*} [DistribLattice α]
variable (x y z : α)
#check (inf_sup_left : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z)
#check (inf_sup_right : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
#check (sup_inf_left : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
#check (sup_inf_right : x ⊓ y ⊔ z = (x ⊔ z) ⊓ (y ⊔ z))
⊓ と ⊔ の可換性を用いることで上記の左と右のバージョンが等価であることは簡単に示せます．ここで有限個の元を持つ分配的ではない束を明示的に記述することで，すべての束が分配的ではないことを示すのは良い演習になります．そして任意の束で ⊓ と ⊔ のどちらかの分配則がもう片方を包含することを示すのも良い演習になるでしょう:
variable {α : Type*} [Lattice α]
variable (a b c : α)
example (h : ∀ x y z : α, x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) := by
sorry
example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
sorry
公理に基づく構造をより大きい構造に組み込むことも可能です．例えば 狭義順序環 は半順序が定義された可換環であり，かつその順序が環の和と積に対して整合的であるという追加の公理を満たすものです:
variable {R : Type*} [StrictOrderedRing R]
variable (a b c : R)
#check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
#check (mul_pos : 0 < a → 0 < b → 0 < a * b)
Chapter 3 では以下の定理を mul_pos と < の定義から導く方法を学びます:
#check (mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b)
ここまでの内容からさらに発展問題として，実数上の算術と順序についての推論に使われるよくある事実の多くが任意の順序環で一般的に成り立つことが示せます．ここでは環と半順序の性質，そして最後の2つの例で使われている事実だけを用いていくつかの例を示しましょう:
example (h : a ≤ b) : 0 ≤ b - a := by
sorry
example (h: 0 ≤ b - a) : a ≤ b := by
sorry
example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
sorry
最後にもう一つ例を挙げましょう． 距離空間 とは，集合とその集合上の距離と呼ばれる，任意の2つの要素 x, y から実数 dist x y を対応させる写像の組のことです．距離関数は以下の公理を満たすものとします:
variable {X : Type*} [MetricSpace X]
variable (x y z : X)
#check (dist_self x : dist x x = 0)
#check (dist_comm x y : dist x y = dist y x)
#check (dist_triangle x y z : dist x z ≤ dist x y + dist y z)
本節をマスターすれば，これらの公理から距離が常に非負であることを示すことができます:
example (x y : X) : 0 ≤ dist x y := by
sorry
この証明を行うに当たって nonneg_of_mul_nonneg_left という定理を利用することをお勧めします．またお察しの通り，上記の定理 0 ≤ dist x y はMathlibでは dist_nonneg と呼ばれています．