rcases
rcases
は cases
をパターンに従って再帰的(recursive)に適用します。cases
の上位互換という立ち位置です。
variable (P Q R : Prop)
example : P ∨ Q → (P → R) → (Q → R) → R := by
intro h hPR hQR
-- 場合分けをする
rcases h with hP | hQ
· apply hPR hP
· apply hQR hQ
-- 論理積 ∧ に対しても使える
example : P ∧ Q → Q ∧ P := by
-- `h: P ∧ Q` と仮定する
intro h
-- `h: P ∧ Q` を `hP: P` と `hQ: Q` に分解する
rcases h with ⟨hP, hQ⟩
-- `Q ∧ P` を証明する
exact ⟨hQ, hP⟩
rcases
は一般には ⟨x₁, x₂, ...⟩ | ⟨y₁, y₂, ...⟩ | ...
という記法で帰納型の分解が可能です。
inductive Sample where
| foo (x y : Nat) : Sample
| bar (z : String) : Sample
example (s : Sample) : True := by
rcases s with ⟨x, y⟩ | ⟨z⟩
case foo =>
-- `x`, `y` が取り出せている
guard_hyp x : Nat
guard_hyp y : Nat
trivial
case bar =>
-- `z` が取り出せている
guard_hyp z : String
trivial