fin_cases
fin_cases
は有限通りの場合分けを行うタクティクです。
何度も cases
をしないと全通りに場合分けできない場合でも、一発で全てのケースを生成することができます。
h : x ∈ [a₁, ..., aₙ]
といった形の仮定に対して fin_cases h
とすると、代入 x = a₁, ..., x = aₙ
を施した n 個のゴールが生成されます。
import Mathlib.Tactic.FinCases
example {n : ℕ} (h : n ∈ [2, 4, 42]) : 2 ∣ n := by
-- n に 2, 4, 42 を順に代入した 3 つのゴールが生成される
fin_cases h
-- あとはそれぞれのゴールに対して具体的に計算して証明する
next =>
show 2 ∣ 2; decide
next =>
show 2 ∣ 4; decide
next =>
show 2 ∣ 42; decide
fin_cases
を使わない場合、以下のように cases
を繰り返し用いて一つずつケースを取り出すことになります。
example {n : ℕ} (h : n ∈ [2, 4, 42]) : 2 ∣ n := by
cases h
case head =>
show 2 ∣ 2; decide
case tail h =>
-- n ∈ [4, 42] であるケース
change n ∈ [4, 42] at h
cases h
case head =>
show 2 ∣ 4; decide
case tail h =>
-- n ∈ [42] であるケース
change n ∈ [42] at h
cases h
case head =>
show 2 ∣ 42; decide
case tail h =>
-- n ∈ [] であるケース
change n ∈ [] at h
contradiction
fin_cases
は List α
のほかに、Finset α
と Multiset α
に対して適用可能です。
example {n : ℕ} (h : n ∈ ({2, 4, 42} : Finset ℕ)) : 2 ∣ n := by
fin_cases h
all_goals decide
example {n : ℕ} (h : n ∈ ({2, 4, 42} : Multiset ℕ)) : 2 ∣ n := by
fin_cases h
all_goals decide
また、型 α
が「有限な型」である(インスタンス Fintype α
が実装されている)場合、fin_cases x
は x : α
のとりうる値に関する場合分けを行います。
-- `Fin n` は 0 から n-1 までの整数からなる型で、val : ℕ と isLt : val < n の 2 つのフィールドを持つ
example (n : Fin 10) (h : n.val ∣ 6) : n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 := by
-- n.val = 0, ..., n.val = 9 の 10 通りに場合分けする
fin_cases n
-- h : n.val ∣ 6 が成り立たないケースは contradiction で示される
any_goals contradiction
-- 残りのケースについて、n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 6 が成り立つ
all_goals decide