linarith

linarith は線形算術(linear arithmetic)を行うタクティクです。Fourier-Motzkin elimination を用いて、線形な(不)等式系から矛盾を導こうとします。一般に、ゴールが False でないときにはゴールの否定を仮定に加えることで、ゴールを閉じようとします。

import Mathlib.Tactic.Linarith -- `linarith` のために必要
import Batteries.Data.Rat.Basic -- `ℚ` のために必要

variable (x y z : ℚ)

example (h1: x = 2 * y) (h2 : - x + 2 * y = 1) : False := by
  linarith

example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) :
    12 * y - 4 * z ≥ 0 := by
  linarith

linarith はローカルコンテキストにある命題を読むので、linarith が通らないとき、追加で補題を示すことで解決することがあります。

example : id x ≤ x := by
  -- `linarith` で示すことはできない
  fail_if_success linarith

  have : id x = x := rfl

  -- `id x = x` だと教えてあげると `linarith` で示せる
  linarith

また、使ってほしい補題を直接渡すこともできます。

example (h : x ≤ y) (pos : 0 ≤ x) : x + x ^ 2 ≤ y + y ^ 2 := by
  -- `linarith` では示せない
  fail_if_success linarith

  -- `linarith` 単独で扱えない部分、つまり `x ^ 2 ≤ y ≤ 2` を示すための
  -- 補題を引数で渡してやると通る
  linarith [pow_le_pow_left pos h 2]

舞台裏

linarith は一般に、型クラス LinearOrderedCommRing のインスタンスに対して動作します。ここで linear order とは全順序のことです。

variable {R : Type} [LinearOrderedCommRing R]

variable (x y z : R)

-- R 上の不等式だが `linarith` で証明できる
example (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) :
    12 * y - 4 * z ≥ 0 := by
  linarith

linarith と他のタクティクの使い分け

1 < 2 のような簡単な数値のみの不等式の場合、norm_num や simp_arith でも証明ができます。 同じ命題を示すのに複数のコマンドがあるわけですが、コマンド実行にかかる時間に違いがあります。

実行環境により正確な実行時間は異なりますが、linarith は比較的重いタクティクです。

#time example : 1 < 2 := by simp_arith

#time example : 1 < 2 := by norm_num

#time example : 1 < 2 := by linarith