split
仮定やゴールにある if ... then ... else
や match ... with ...
式を扱うのに有用なタクティクです。
if/match 式を扱う必要が生じるのは、典型的には Lean で定義したアルゴリズムや関数に関して、何か性質を証明しようとしたときです。
ゴールが ⊢ Q (if P then a else b)
であったときに、split
を使用すると2つのサブゴールが生成されます。具体的には
- 1つはローカルコンテキストに
† : P
が追加され、ゴールが⊢ Q (a)
- 1つはローカルコンテキストに
† : ¬ P
が追加され、ゴールが⊢ Q (b)
というサブゴールです。split
によって追加される仮定は名前がついているとは限りません。名前がついていなかった場合、case
などで名前を付けることができます。
仮定に対して用いる場合は split at h
のように利用します。
-- if 式を使って関数を定義する
def myabs (x : Int) : Int :=
if x ≥ 0 then x else - x
example (x : Int) : myabs (2 * x) = 2 * myabs x := by
-- `myabs` の定義を展開する
dsimp [myabs]
-- ゴールの中に if 式があって複雑
show (if 2 * x ≥ 0 then 2 * x else -(2 * x)) = 2 * if x ≥ 0 then x else -x
-- `split` タクティクでケース分割する
split
case isTrue h =>
-- `2 * x ≥ 0` の場合
guard_hyp h: 2 * x ≥ 0
-- 左辺にあった if 式が消えた
show 2 * x = 2 * if x ≥ 0 then x else -x
replace h : x ≥ 0 := by linarith [h]
-- `simp` で if を消すことができる
simp [h]
case isFalse h =>
-- `2 * x < 0` の場合
guard_hyp h: ¬2 * x ≥ 0
-- 左辺にあった if 式が消えた
show -(2 * x) = 2 * if x ≥ 0 then x else -x
-- if 式を消すための補題を準備する
have hx : ¬ x ≥ 0 := by linarith [h]
-- `simp` で単純化
simp [h, hx]
match 式と split
if
式だけでなく match
式に対しても使うことができます。
-- match式を使って関数を定義する
def mysgn (x : Int) :=
match x with
| Int.negSucc _ => -1
| Int.ofNat 0 => 0
| _ => 1
example (x : Int) : mysgn (mysgn x) = mysgn x := by
-- mysgn x を k と置く
set k := mysgn x with h
-- h の mysgn の定義を展開する
dsimp [mysgn] at h
-- h の match の結果によって場合分け
-- すべての場合 (k = -1, 0, 1) に関して mysgn の定義に従い計算する
split at h
all_goals
rw [h]
rfl