Merge pull request #530 from lean-ja/Seasawher/issue341

refactor: `rcases` を `cases` から独立させる

Author: Seasawher

Examples/Tactic/Cases.lean

@@ -4,7 +4,8 @@
 
 たとえば、ローカルコンテキストに `h : P ∨ Q` があるときに `cases h` とすると、仮定に `P` を付け加えたゴール `case inl` と、仮定に `Q` を付け加えたゴール `case inr` を生成します。
 
-補足すると、`inl` と `inr` はそれぞれ `left injection` と `right injection` からその名前があり、`Or` 型のコンストラクタです。-/
+上位互換にあたるタクティクに [`rcases`](./RCases.md) があります。
+-/
 
 -- `P`, `Q`, `R` を命題とする
 variable (P Q R : Prop)
@@ -40,8 +41,7 @@ example : P ∨ Q → (P → R) → (Q → R) → R := by
   | inr hQ =>
     exact hQR hQ
 
-/-!
-## 補足
+/- ## 舞台裏
 
 `cases` は、実際には論理和に限らず帰納型をコンストラクタに分解することができるタクティクです。
 論理和を分解することができるのも、`Or` が帰納型として定義されているからです。
@@ -57,52 +57,23 @@ Or.inr : ∀ {a b : Prop}, b → a ∨ b
 -/
 #guard_msgs in #print Or
 
+-- Or のコンストラクタ
 #check (Or.inl : P → P ∨ Q)
 #check (Or.inr : Q → P ∨ Q)
 
-end Cases --#
-
-/-! ## rcases
-
-`rcases` は `cases` をパターンに従って再帰的(recursive)に適用します。`cases` の上位互換という立ち位置です。-/
-
-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
+  -- cases で場合分けを実行できる
+  cases s
 
+  case foo x y =>
     trivial
 
-  case bar =>
-    -- `z` が取り出せている
-    guard_hyp z : String
-
+  case bar z =>
     trivial
+
+end Cases --#

Examples/Tactic/Intro.lean

@@ -53,7 +53,7 @@ example (hPR : P → R) (hQR : Q → R) : P ∨ Q → R := by
   | Or.inr hQ =>
     exact hQR hQ
 
-/- `rcases` を使って分解することも一般的です。-/
+/- [`rcases`](./RCases.md) を使って分解することも一般的です。-/
 
 example (hPR : P → R) (hQR : Q → R) : P ∨ Q → R := by
   intro h

Examples/Tactic/Obtain.lean

@@ -29,7 +29,7 @@ example (h : ∃ e : X, P e) : True := by
   trivial
 
 /-
-`obtain` に与えることのできるパターンは `rcases` に与えられるパターンと同様で、一般の帰納型を分解することができます。
+`obtain` に与えることのできるパターンは [`rcases`](./RCases.md) に与えられるパターンと同様で、一般の帰納型を分解することができます。
 -/
 
 inductive Sample where

Examples/Tactic/RCases.lean

@@ -0,0 +1,46 @@
+/- # rcases
+
+`rcases` は [`cases`](./Cases.md) をパターンに従って再帰的(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

Examples/Term/Type/Prop.lean

@@ -15,7 +15,7 @@ theorem proof_irrel (P : Prop) (h1 h2 : P) : h1 = h2 := rfl
 /-- info: 'Proposition.proof_irrel' does not depend on any axioms -/
 #guard_msgs in #print axioms proof_irrel
 
-/- 証明無関係の重要な帰結のひとつに、「命題から値を取り出すことができるのは、証明の中だけ」というものがあります。たとえば次のように、証明の中であれば命題を [`cases`](../../Tactic/Cases.md) や `rcases` で分解して値を取り出すことができます。-/
+/- 証明無関係の重要な帰結のひとつに、「命題から値を取り出すことができるのは、証明の中だけ」というものがあります。たとえば次のように、証明の中であれば命題を [`cases`](../../Tactic/Cases.md) や [`rcases`](../../Tactic/RCases.md) で分解して値を取り出すことができます。-/
 
 -- 同じ存在命題の２通りの証明
 -- 2乗すると1になる整数を２通り与えた

src/SUMMARY.md

@@ -108,6 +108,7 @@
   - [positivity: 正値性を示す](./Tactic/Positivity.md)
   - [push_neg: ドモルガン](./Tactic/PushNeg.md)
   - [qify: 有理数にキャストする](./Tactic/Qify.md)
+  - [rcases: パターン分解](./Tactic/RCases.md)
   - [refine: 穴埋め推論](./Tactic/Refine.md)
   - [rel: 不等式を使う](./Tactic/Rel.md)
   - [rename_i: 死んだ変数に名前を付ける](./Tactic/RenameI.md)