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 には、このような事実を明示的に参照する必要を通常はなくす自動化機能が備わっていますが、説明の目的上これらは有用です。

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 から実数の理論や有用な自動化機能をインポートしています。 簡潔さのため、こうした情報は教科書では通常省略されています。

自由に変更して、どのような挙動になるか試してみてください。 VS Code では、ℝ 文字を \R または \real と入力します。 なお、スペースまたはタブキーを押すまでシンボルは表示されません。 Lean ファイルを読む際にシンボルにカーソルを合わせると、そのシンボルを入力するために使用できる構文が VS Code によって表示されます。 利用可能なすべての略記を確認したい場合は Ctrl-Shift-P を押してから「abbreviations」と入力し、 Lean 4: Show all abbreviations コマンドにアクセスしてください。 もしキーボードに容易にアクセスできるバックスラッシュが無い場合は lean4.input.leader 設定を変更することで、先頭文字を変更することができます。

タクティック証明の途中にカーソルが位置していると、Lean は Lean Infoview ウィンドウに現在の 証明状態 (proof state) を報告します。 証明の各ステップをカーソルで移動すると、その状態がどのように変化していくかが確認できます。 Lean における典型的な証明状態は次のように表示されることがあります。

1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4

⊢ から始まる行の前の行は コンテキスト (context) を示しており、現在利用されている対象や仮定を表しています。 この例では、自然数である対象 x と y の二つが含まれており、さらに h₁、h₂、h₃ というラベルの付いた三つの仮定も含まれています。 Lean では、コンテキスト内のすべての項目に識別子が付けられています。添字付きのラベルは、h\1, h\2, h\3 と入力することもできますが、識別子であれば何でも構いません。 たとえば、h1, h2, h3 や foo, bar, baz としてもよいでしょう。 最後の行は ゴール (goal)、すなわち証明すべき事実を表しています。 時として、人々は証明すべき事実を ターゲット (target) と呼び、コンテキストとそのターゲットの組み合わせを ゴール と呼ぶこともありますが、実際には意図する意味は通常明確です。

以下の恒等式を証明してみましょう。 それぞれの場合において 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 といった恒等式は引数を省略して使用することも可能です。 この場合、書き換えタクティックはゴール中で左辺に一致する式を探し、最初に見つかったパターンを用いて適用します。

example (a b c : ℝ) : a * b * c = b * c * a := by
  rw [mul_assoc]
  rw [mul_comm]

部分的な (partial) 情報を指定することも可能です。 たとえば、mul_comm a は a * ? という形の任意のパターンに一致し、それを ? * a に書き換えます。 最初の例は引数を一切指定せずに試し、次の例は引数を 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]

リスト内の任意のカンマの後にカーソルを置くと、その時点での段階的な進捗が確認できます。

もうひとつのテクニックとして、例や定理の外部で変数を一度宣言しておくと、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 ブロックに入れることで限定できます。 最後に、導入部で述べたように Lean は式の型を決定するためのコマンドを提供しています。

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 の型が ℝ であるという我々の期待を明示し、その期待に反する場合、Lean はエラーを発生させます。 後ほど、最後の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 で始まる式は 証明項 (proof term) そのものであり、タクティック証明の内部でも使用できますが、その場合 Lean はその証明項をゴールを解くための指示として解釈します。 calc の構文は非常に厳格で、下線や理由付けの部分は上記で示された形式に従わなければなりません。 Lean はインデントを用いてタクティックのブロックや calc ブロックの開始・終了などを判断します。 実際に、上記の証明のインデントを変更してみて、どのような挙動になるか試してみてください。

calc 証明を書く一つの方法として、まず各段階の理由付けに sorry タクティックを用いて概略を記述し、 その状態で Lean が式を受け入れるか確認してから、各ステップをタクティックで正当化するという手順があります。

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 タクティックが提供されていることに注目してください。 これは、局所的な仮定を使わず、環の公理のみから導かれる任意の可換環における恒等式を証明するために設計されています。

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 をインポートする際に間接的に取り込まれますが、次の節では実数以外の構造に対する計算にも使えることが示されます。 また、明示的には import Mathlib.Tactic と記述することで取り込むことができます。 さらに、他の一般的な代数的構造に対しても同様のタクティックが存在することが確認できるでしょう。

rw の変種として nth_rw というものがあり、これはゴール中の特定の箇所のみを置換することを可能にします。 可能な一致箇所は1から番号付けされるため、以下の例では nth_rw 2 [h] が a + b の 2 番目の出現を 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\) と \(+\) による構造は 可換群 (abelian group) をなす。すなわち、\(0\) が加法の単位元であり、各 \(x \in R\) に対して \(-x\) がその逆元となります。

  • 乗法は結合的で単位元 \(1\) を持ち、さらに乗法は加法に対して分配的です。

Lean では、対象の集合は 型 (type) として表現され、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 (neg_add_cancel : ∀ 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)

後で最初の行の角括弧について詳しく学びますが、とりあえず、この宣言は型 R とその上の環構造を与えるということだけ覚えておけば十分です。 その後、Lean は R の要素に対して一般的な環の記法を使用できるようにし、環に関する定理のライブラリを利用できるようにします。

いくつかの定理の名前は馴染み深く見えるはずです。 それらはまさに前節で実数を使って計算する際に用いたものと全く同じです。 Lean は自然数や整数のような具体的な数学的構造についての事柄を証明するだけでなく、公理的に特徴付けられる抽象的な構造、たとえば環のようなものについての事柄を証明するのにも優れています。 さらに、Lean は抽象的な構造と具体的な構造の両方に対する 一般的な推論 (generic reasoning) をサポートしており、適切なインスタンスを認識するように訓練することができます。 したがって、環に関する任意の定理は整数 ℤ、有理数 ℚ、複素数 ℂ のような具体的な環に適用することができます。 また、順序体や体など、環を拡張する抽象構造の任意のインスタンスにも適用することができます。

しかしながら、実数のすべての重要な性質が任意の環で成り立つわけではありません。 たとえば、実数における乗法は可換ですが、一般にはそうとは限りません。 線形代数学の講義を受けたことがあれば、任意の \(n\) に対して実数の \(n \times 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 に既に存在しています。 私たちは証明するバージョンに同じ名前を付けることで、ライブラリの内容と命名規則の両方を学習できるようにします。

Lean はプログラミング言語で用いられるものと同様の組織化機構を提供します。 たとえば、定義や定理 foo が 名前空間 (namespace) bar 内で導入されると、その完全な名前は bar.foo となります。 その後、コマンド open bar を使うことで名前空間を 開き (opens)、短い名前 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, neg_add_cancel]

#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, neg_add_cancel, 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

十分な計画を立てれば、それぞれを3回の書き換えで証明することができます。

これから波括弧の使い方について説明します。 たとえば、文脈に a、b、c があり、さらに仮定 h : a + b = a + c がある状況を想像してください。 そして結論として b = c を導きたいとします。 Lean では対象に対して定理を適用するのと同じように、仮定や事実に対しても定理を適用することができるため、add_left_cancel a b c h が b = c の証明になると考えるかもしれません。 しかし、a、b、c を明示的に書くのは冗長です。 なぜなら、仮定 h によって、我々が念頭に置いている対象がすでに明確になっているからです。 この場合、余分な文字をいくつか入力するのはそれほど手間ではありませんが、もしより複雑な式に対して add_left_cancel を適用するなら、すべてを書き出すのは面倒です。 このような場合、Lean は引数を 暗黙 (implicit) のものとしてマークすることを許します。 つまり、引数を省略し、後の引数や仮定などから自動的に推論されるようにするのです。 波括弧 {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]

新しいテクニックを使いました！ 証明をステップ実行してみると、何が起こっているかが分かります。 have タクティックは元のゴールと同じコンテキストを持つ新しいゴール a * 0 + a * 0 = a * 0 + 0 を導入します。 次の行がインデントされているという事実は、Lean がこの新しいゴールを証明するためのタクティックのブロックを期待していることを示しています。 このインデントはモジュラーな証明スタイルを促進します。 すなわち、インデントされた部分証明が have によって導入されたゴールを確立し、その後、元のゴールの証明に戻ります。 ただし、新たに仮定 h が追加されており、それを証明したので、今後は自由に利用できるようになります。 この時点で、ゴールはまさに add_left_cancel h の結果と一致しています。

同様に、証明を apply add_left_cancel h または exact add_left_cancel h で閉じることもできます。 exact タクティックは、現在のゴールを完全に証明する証明項を引数として取り、新たなゴールを生成しません。 一方、apply タクティックは、その引数が必ずしも完全な証明である必要がない変種です。 不足している部分は Lean によって自動的に推論されるか、新たなゴールとして現れます。 厳密には、exact タクティックは apply よりも能力が低いため技術的には冗長ですが、証明スクリプトが人間にとってやや明確になり、ライブラリが進化した際の保守性も向上します。

乗法が可換であると仮定していないことを忘れないでください。 そのため、以下の定理の証明にもいくらかの作業が必要となります。

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

第三の定理では、単に 0 と書くのではなく (-0 : R) と注釈を付ける必要がありました。 なぜなら R を指定しなければ、Lean はどの 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 の証明として rfl を提示することで、Lean は定義を展開し、両辺が同一であると認識します。 rfl タクティックも同様の働きをします。 これは Lean の基礎論理における 定義的等価 (definitional equality) の一例です。 つまり、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 (neg_add_cancel : ∀ 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 (inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1)

もし自信満々ならば、これらの公理のみを用いて群に関する以下の事実を証明してみてください。 その途中で、いくつかの補助補題を証明する必要があります。 本節で行った証明がいくつかのヒントを提供しています。

theorem mul_inv_cancel (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 タクティクスを使ってゴールを解決できることを見てきました。 この節ではこれらのツールを十分に活用していきます。

ライブラリの定理 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 を暗黙の引数に設定しているので、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 を適用すると2つのゴールが生成され、各ゴールの証明が始まる箇所を示すためにドットを使っています。 ドットは任意ですが、ゴールを 集中 させる役割を果たします。 つまり、ドットで導入されたブロック内では1つのゴールのみが表示され、そのブロックの終わりまでにそのゴールを完成させなければなりません。 ここでは、最初のブロックを終了させるために、別のドットで新しいブロックを開始しています。 インデントを減らしても同じ効果が得られたでしょう。 3番目の例と最後の例では、タクティクスモードに入ることを全く避け、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 では、関数 f を引数 x に適用する場合は f x と書きます。 これは、事実や定理 h を引数 x に適用して得られる結果を示すために 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 → a ≤ b → log a ≤ log 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 は「if and only if」を意味する 双方向の含意 を用いています。 (VS Code では \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」を h.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
  apply log_le_log h₀
  sorry

これらの例から、必要なライブラリ定理を見つける能力が形式化の重要な要素であることは明らかです。 利用できる戦略はいくつかあります。

  • Mathlib は GitHub repository で閲覧できます。

  • Mathlib の API ドキュメントは Mathlib の web pages で利用できます。

  • Mathlib の命名規則とエディタの Ctrl-space 補完機能 (Mac の場合は Cmd-space) を活用して、定理名を推測することができます。 Lean では、定理が A_of_B_of_C という名前であれば、これは仮定が B と C という形で与えられたときに、何かしらの形の A を導く定理であることを示しています (A, B, C は、ゴールを口に出して読むときの表現に近いものです)。 例えば、x + y ≤ ... のようなことを示す定理はおそらく add_le で始まるでしょう。 そこで、add_le と入力して Ctrl-space を押すと、有用な候補が表示されます。なお、Ctrl-space を2回押すと、利用可能な補完候補に関するより詳細な情報が表示されることに注意してください。

  • VS Code で既存の定理名を右クリックすると、エディタはその定理が定義されているファイルへジャンプするオプションが含まれたメニューを表示します。 そこで、近くにある類似の定理を見つけることができます。

  • apply? タクティクスを使うことができます。 これは、ライブラリ内から関連する定理を見つけ出そうと試みます。

example : 0 ≤ a ^ 2 := by
  -- apply?
  exact sq_nonneg a

この例で apply? を試すには、exact コマンドを削除し、前の行のコメントアウトを解除してください。 これらのテクニックを使って、次の例で必要なものを見つけられるか試してみましょう。

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 と同値です。 原理的には、これらは互いに置き換えて使用できるはずですが、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 を利用することができます。 また、論理積を2つのゴールに分割するために、constructor タクティクスが必要となります (詳しくは Section 3.4 を参照してください)。

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 は二引数の関数として振る舞います。 このように複数の引数を扱う方法は、論理学者 Haskell Curry にちなんで カリー化 と呼ばれます。

Lean における演算子の優先順位にも慣れる必要があります。 関数適用は中置演算子よりも強く結合するため、式 min a b + c は (min a b) + c と解釈されます。 やがて、これらの規則は自然と身につくでしょう。

le_antisymm という定理を用いると、2つの実数が互いに小なりイコールであるならば、それらは等しいことが示せます。 これと上記の事実を利用して、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番目の apply は 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 となり、第二の場合、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

aux は、等式を証明するために必要な2つの不等式のうちの1つを提供していることは明らかですが、適切な値に適用することで、もう一方の不等式も得られます。 ヒントとして、定理 add_neg_cancel_right と linarith タクティクスを利用できます。

Lean の命名規則は、ライブラリでの三角不等式の名前において顕著に表れています。

#check (abs_add : ∀ a b : ℝ, |a + b| ≤ |a| + |b|)

これを使って、さらに add_sub_cancel_right を用いながら、次の変形版を証明してください。

example : |a| - |b| ≤ |a - b| :=
  sorry
end

これを3行以内で実現できるか試してみてください。 定理 sub_add_cancel を利用しても構いません。

今後の節で利用するもう一つの重要な関係は、自然数における整除関係 x ∣ y です。 注意してください: この整除記号は、キーボード上の通常のバーでは ありません 。 代わりに、VS Code で \| と入力して得られる 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 を適用することで Lean は x^2 の定義を x^1 * x に展開させます。 以下の命題を証明するために必要な定理の名前を推測できるか、試してみてください。

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)
#check (le_antisymm : x ≤ y → y ≤ x → x = y)

ここでは、任意の型に対して α, β, γ (それぞれ \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)

⊓ と ⊔ の特徴づけにより、これらはそれぞれ greatest lower bound (最大下限)と least upper bound (最小上限) と呼ばれることが正当化されます。 VS Code では、これらを \glb と \lub と入力することで得られます。 また、これらの記号はしばしば infimum (下限) および supremum (上限) と呼ばれ、Mathlib では定理名中でそれぞれ inf と sup として参照されます。 さらに、これらは meet と join とも呼ばれることが多いです。 したがって、束 (lattice) を扱う際には、以下の用語の対応関係を念頭に置く必要があります。

  • ⊓ は greatest lower bound (最大下限)、infimum (下限)、または meet と呼ばれます。

  • ⊔ は least upper bound (最小上限)、supremum (上限)、または join と呼ばれます。

いくつかの束の例として、以下が挙げられます。

  • 任意の全順序上での min と max (例えば、整数や実数における ≤ を伴うもの)

  • ある集合の部分集合全体の集合における ∩ と ∪ (順序関係 ⊆ を伴うもの)

  • ブール真理値に対する ∧ と ∨ (x が偽または y が真である場合に x ≤ y とする順序

  • 自然数 (または正の自然数) 上の gcd と lcm (整除関係 ∣ による順序)

  • ベクトル空間の線形部分空間全体の集合で、最大下限は交わりによって与えられ、最小上限は2つの空間の和によって与えられ、順序は包含関係です。

  • 集合上の位相全体 (または Lean における型上の位相全体)では、2つの位相の最大下限は、それらの和集合によって生成される位相となり、最小上限はそれらの交わりとなります。 また、順序は逆包含関係に基づいて定められます。

min / max や gcd / lcm と同様に、infimum と supremum の可換性および結合性は、 それらの特徴づける公理と le_refl および le_trans のみを用いて証明できることを確認できます。

apply le_trans を使ってゴールが x ≤ z のときに証明を進めるのはあまり良い考えではありません。 実際、Lean は中間の要素 y をどれにするかを推測する方法を持っていないからです。 そのため、apply le_trans を使うと、x ≤ ?a、?a ≤ z、そして最後に型 α のゴールが生成されます。 ここで、?a (おそらくもっと複雑な自動生成された名前になるでしょう) は謎の y を表しています。 最後のゴール (型 α のもの) は、y の値を提供するためのものです。 これは、Lean が最初のゴール x ≤ ?a の証明から自動的に中間項 y の値を推論することを期待しているため、最後に残るのです。 この望ましくない状況を避けるために、calc タクティクスを使って明示的に y を指定する方法があります。 または、trans タクティクスを使うこともできます。trans は引数として y を受け取り、 期待されるゴール x ≤ y と y ≤ z を生成します。 もちろん、exact le_trans inf_le_left inf_le_right のように完全な証明を直接与えることでこの問題を回避することもできますが、その場合はかなりの計画が必要になります。

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

これらの定理は Mathlib 内でそれぞれ inf_comm、inf_assoc、sup_comm、および sup_assoc として見つけることができます。

また、これらの公理のみを用いて 吸収則 を証明するという良い演習もあります。

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 ⊔ z) = x ⊓ y ⊔ x ⊓ z)
#check (inf_sup_right x y z : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
#check (sup_inf_left x y z : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
#check (sup_inf_right x y z : 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つの例で列挙された事実のみを用いて試せるいくつかの例を示します。 (ただし、これらの環は可換であると仮定していないため、ring タクティクスは使用できません。)

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要素を実数に写す距離の概念、すなわち 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 を利用することをお勧めします。 ご想像のとおり、この定理は Mathlib では dist_nonneg と呼ばれています。