不等式の型と証明パターン

数学では \(a \le b\) を 1 つの文として読みます． Lean でも同じく，a ≤ b は命題です． より正確には，a b : α のとき，a ≤ b は Prop 型の項です． ≤ という notation は LE.le に対応し，< は LT.lt に対応します． したがって，不等式は実数専用の構文ではありません． どの型 α の上の順序を使っているかによって，不等式の意味が決まります．

順序の基本性質は型クラスで与えられます． 推移律などを使うには Preorder α，反対称性も使うには PartialOrder α，任意の 2 元が比較できることを使うには LinearOrder α が必要です． さらに，足し算や掛け算と順序の相性を使うには，IsOrderedAddMonoid，IsOrderedRing，IsStrictOrderedRing などの構造が関わります． たとえば実数 ℝ には線形順序，体，順序環の構造が入っているので，通常の不等式計算ができます．

#check LE.le
#check LT.lt
#check Preorder
#check PartialOrder
#check LinearOrder
#check IsOrderedAddMonoid
#check IsOrderedRing
#check IsStrictOrderedRing

#check ((3 : ℝ) ≤ 5)
#check ((3 : ℝ) < 5)

#synth LE ℝ
#synth LT ℝ
#synth LinearOrder ℝ
#synth IsOrderedAddMonoid ℝ
#synth IsStrictOrderedRing ℝ

≤ や < は型によって意味が変わります． たとえば ℝ 上の 0 ≤ x と，ℝ≥0 上の 0 ≤ x は見た目が似ていますが，別々の型の上の順序です． x : ℝ≥0 は内部的には非負実数なので，実数へ coercion すれば 0 ≤ (x : ℝ) が取り出せます．

#check (fun x : ℝ => 0 ≤ x)
#check (fun x : ℝ≥0 => (0 : ℝ) ≤ (x : ℝ))
#check (fun x : ℝ≥0 => (0 : ℝ≥0) ≤ x)

example (x : ℝ≥0) : (0 : ℝ) ≤ (x : ℝ) := by
  exact x.property

また，≤ は数値の大小だけでなく，順序一般を表す記号です． 集合や部分構造では，≤ が包含関係を表すことがあります． 証明中に不等号が現れたら，まず両辺の型を確認するのが安全です．

#check (fun s t : Set ℝ => s ≤ t)
#check (fun s t : Set ℝ => s ⊆ t)
#check (fun S T : AddSubgroup ℤ => S ≤ T)

不等式の基本的な証明は，推移律や変形補題を使って進めます． 数学で「a ≤ b ≤ c だから a ≤ c」と書く部分は，Lean では le_trans や calc で表せます．

example (a b c : ℝ) (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := by
  exact le_trans h₁ h₂

example (a b c : ℝ) (h₁ : a < b) (h₂ : b ≤ c) : a < c := by
  exact lt_of_lt_of_le h₁ h₂

example (a b : ℝ) (h : a < b) : ¬ b ≤ a := by
  exact not_le_of_gt h

example (a b c d : ℝ) (hab : a ≤ b) (hbc : b ≤ c) (hcd : c ≤ d) : a ≤ d :=
  calc
    a ≤ b := hab
    _ ≤ c := hbc
    _ ≤ d := hcd

数値だけの不等式は norm_num が得意です． 仮定を含む一次不等式は linarith が強く，二次式などの多項式不等式は nlinarith が有効なことがあります． nlinarith は，平方非負性のような補助補題を渡すと使いやすくなります．

example : (3 : ℝ) / 2 < 2 := by
  norm_num

example (x y : ℝ) (hx : x ≤ 3) (hy : y ≤ 4) : x + y ≤ 7 := by
  linarith

example (x : ℝ) : 0 ≤ x ^ 2 := by
  nlinarith [sq_nonneg x]

example (x : ℝ) : 0 < x ^ 2 + 1 := by
  nlinarith [sq_nonneg x]

非負性を積み上げる証明では，既存補題を直接使うのが読みやすいことも多いです． mul_nonneg は「非負数同士の積は非負」，mul_le_mul_of_nonneg_left は「非負数を左から掛けても不等式の向きは変わらない」という補題です． 補題名では，le が ≤，lt が <，nonneg が 0 ≤ ...，pos が 0 < ... を表すことが多いです．

#check add_le_add
#check mul_nonneg
#check mul_le_mul_of_nonneg_left
#check abs_nonneg
#check sq_nonneg

example (a b c d : ℝ) (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d := by
  exact add_le_add hab hcd

example (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : 0 ≤ x * y := by
  exact mul_nonneg hx hy

example (x y c : ℝ) (hxy : x ≤ y) (hc : 0 ≤ c) : c * x ≤ c * y := by
  exact mul_le_mul_of_nonneg_left hxy hc

単調性に従う変形は gcongr が便利です． 次の例では，両辺に同じ正の項を足す単調性を使っています． 非負性・正値性を自動で示したいときは positivity が役に立つことがあります．

example (x y : ℝ) (hxy : x ≤ y) : x + 1 ≤ y + 1 := by
  gcongr

example (x : ℝ) : 0 ≤ x ^ 2 + 1 := by
  positivity

実際の証明では，次のように切り分けると方針を立てやすくなります．

• 具体的な数値計算なら norm_num
• 線形不等式なら linarith
• 多項式不等式なら nlinarith と sq_nonneg など
• 単調性なら gcongr，または add_le_add，mul_le_mul_of_nonneg_left など
• 長い連鎖なら calc
• 型が混ざるなら，coercion と変換補題を #check で確認する

数学者にとって重要なのは，不等式そのものを「文」ではなく「ある型の上の順序関係から作られた命題」と読むことです． これが分かると，エラーメッセージに出る型クラス仮定や，le，lt，nonneg，pos を含む補題名が読みやすくなります．

演習

不等式の型と証明パターンを確認してください．

#check LE.le
#check LT.lt
#synth LinearOrder ℝ
#synth IsStrictOrderedRing ℝ

example (x y : ℝ) (hx : x ≤ 3) (hy : y ≤ 4) : x + y ≤ 7 := by
  -- 解答例:
  --   linarith
  sorry

example (x : ℝ) : 0 ≤ x ^ 2 := by
  -- 解答例:
  --   positivity
  sorry

example (x y c : ℝ) (hxy : x ≤ y) (hc : 0 ≤ c) : c * x ≤ c * y := by
  -- 解答例:
  --   exact mul_le_mul_of_nonneg_left hxy hc
  sorry

ここまでで，よく使う具体的な対象と，それらの上に入っている構造を見ました． 以降は，それらの対象について実際に証明を書くときによく使う補助 tactic と検索の考え方を整理します．