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
では示すことができない線形な命題です。
section
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
end
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
補題を渡す構文
omega
に明示的に補題を渡す構文を自作することができます。
open Lean Elab.Tactic in
/-- `omega [lem₁, lem₂, .. , lemₙ]` のように、カンマ区切りで補題を渡す構文 -/
elab "omega" "[" s:term,* "]" : tactic => do
for term in s.getElems do
evalTactic <| ← `(tactic| have := $term)
evalTactic <| ← `(tactic| omega)
/-- テスト用の構造体 -/
structure Test where
val : Nat
property : 30 ≤ val
example (x y : Test) : 2 ≤ x.val + y.val := by
-- 通常の omega では示すことができない
fail_if_success omega
-- 補題を渡す構文を使えば示せる
omega [x.property, y.property]