omega

omega タクティクは，「The omega test: a fast and practical integer programming algorithm for dependence analysis」に基づいて実装されたタクティクで，整数や自然数の線形制約を扱う能力を持ちます．

似たタクティクに linarith がありますが, linarith が有理数や実数を扱うのに長けているのに対して，omega は自然数や整数を扱うのに長けています．

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring

example (n m : Nat) : n * m = ((n + m) ^ 2 - n ^ 2 - m ^ 2 ) / 2 := by
  -- `(n + m) ^ 2` を展開する
  ring_nf

  -- `n * m` の部分は，一般の `x` に置き換えて証明してもよい
  generalize n * m = x

  -- つまり，以下を示せばよい
  show x = (x * 2 + n ^ 2 + m ^ 2 - n ^ 2 - m ^ 2) / 2

  -- これは `linarith` では示せない
  fail_if_success linarith

  -- `omega` では示せる
  omega

Lean では自然数同士の引き算は整数同士の引き算とは異なる結果になって厄介なのですが，omega はこの問題を上手く処理します．たとえば，以下は linarith では示すことができない線形な命題です．

variable (a b : Nat)

example (h : (a - b : Int) ≤ 0) : (a - b = 0) := by
  -- `linarith` では示すことができません
  fail_if_success linarith

  -- `omega` では示すことができます
  omega

example (h : a > 0) : (a - 1) + 1 = a := by
  fail_if_success linarith
  omega

example (h : a / 2 < b) : a < 2 * b := by
  fail_if_success linarith
  omega

example : (a - b) - b = a - 2 * b := by
  fail_if_success linarith
  omega

omega は整数や自然数の整除関係を扱うこともできます．

example {a b c : ℤ} : 3 ∣ (100 * c + 10 * b + a) ↔ 3 ∣ (c + b + a) := by omega

example {a b c : ℕ} : 3 ∣ (100 * c + 10 * b + a) ↔ 3 ∣ (c + b + a) := by omega

Lean by Example

omega