論理結合子とデータ構造: `constructor`，`match`，`cases`¶

連言 P ∧ Q や同値 P ↔ Q は structure として実装されていました．これらを示すときは，constructor が対応する constructor を使い，必要な field をサブゴールとして生成します．

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · exact hP
  · exact hQ

example (P Q : Prop) (hPQ : P → Q) (hQP : Q → P) : P ↔ Q := by
  constructor
  · intro hP
    exact hPQ hP
  · intro hQ
    exact hQP hQ

連言や存在命題を分解するときは obtain が便利です． obtain ⟨hP, hQ⟩ := h は，h をパターンに従って分解し，得られた成分に名前をつけます．

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  obtain ⟨hP, hQ⟩ := h
  constructor
  · exact hQ
  · exact hP

example (P : Nat → Prop) (h : ∃ n : Nat, P n) : ∃ n : Nat, P n := by
  obtain ⟨n, hn⟩ := h
  exact ⟨n, hn⟩

rintro は intro とパターン分解を同時に行います．含意の仮定を導入しながら，連言や存在命題をすぐに分解したいときに便利です．

example (P Q R : Prop) : (P ∧ Q → R) → P → Q → R := by
  rintro h hP hQ
  exact h ⟨hP, hQ⟩

match は，inductive 型の値をコンストラクタごとに分けて式を作る構文です．命題の証明でも，証明項を直接書くときにはよく現れます．次の例では，h : P ∨ Q が Or.inl hP で作られている場合と Or.inr hQ で作られている場合に分けています．

example (P Q R : Prop) (h : P ∨ Q) (hPR : P → R) (hQR : Q → R) : R :=
  match h with
  | Or.inl hP => hPR hP
  | Or.inr hQ => hQR hQ

自然数も inductive 型なので，match で Nat.zero と Nat.succ k の場合に分けられます． cases は，このコンストラクタごとの分解を tactic モードで行うものだと見ると分かりやすいです．

example (n : Nat) : n = 0 ∨ ∃ k : Nat, n = k + 1 :=
  match n with
  | Nat.zero => Or.inl rfl
  | Nat.succ k => Or.inr ⟨k, rfl⟩

cases は，手元にある値や証明を，その型のコンストラクタごとに分けて使う tactic です．基本構文は次の形です．

cases h with
| constructor_name args =>
    ...

ここで h は inductive 型の値や証明です． cases h with と書くと，Lean は h の型を見て，その型を作る各コンストラクタに対応する枝を作ります．たとえば P ∨ Q は Or という inductive 型で，コンストラクタ Or.inl : P → P ∨ Q と Or.inr : Q → P ∨ Q を持ちます．そのため，h : P ∨ Q に対して cases h with を使うと，P の証明がある枝と Q の証明がある枝に分かれます．

example (P Q R : Prop) (h : P ∨ Q) (hPR : P → R) (hQR : Q → R) : R := by
  cases h with
  | inl hP =>
      exact hPR hP
  | inr hQ =>
      exact hQR hQ

cases は命題だけでなく，普通の帰納型の値にも使えます． Nat は zero と succ というコンストラクタを持つ inductive 型なので，cases n with は n = 0 の枝と n = k + 1 の枝を作ります．重要なのは，cases が「任意の命題について真偽を場合分けする」tactic ではなく，すでにある値や証明をその帰納型のコンストラクタに従って分解する tactic だという点です．一般の命題 P : Prop について P と ¬ P に分けるには，後で扱う by_cases h : P を使います．

example (n : Nat) : n = 0 ∨ ∃ k : Nat, n = k + 1 := by
  cases n with
  | zero =>
      exact Or.inl rfl
  | succ k =>
      exact Or.inr ⟨k, rfl⟩

rcases は，仮定をパターンに従って分解します． cases よりも複雑な入れ子の分解を短く書けます．

example (P Q R : Prop) (h : (P ∧ Q) ∨ R) : Q ∨ R := by
  rcases h with ⟨_hP, hQ⟩ | hR
  · left
    exact hQ
  · right
    exact hR

存在命題を作るには，証拠とその証明を与えます． Mathlib などを読み込んだ環境では，use という tactic で証拠を指定することもよくあります．ここでは Core Lean だけでも使えるように，Exists.intro の notation である ⟨3, rfl⟩ を直接書きます．

example : ∃ n : Nat, n + 2 = 5 := by
  exact ⟨3, rfl⟩

選言 P ∨ Q を示すには，left または right でどちらを示すかを選びます．

example (P Q : Prop) (hP : P) : P ∨ Q := by
  left
  exact hP

example (P Q : Prop) (hQ : Q) : P ∨ Q := by
  right
  exact hQ

演習¶

constructor と cases を使って，連言の順序を入れ替えてください． constructor は And.intro に対応し，cases は And の証明から左右の成分を取り出す操作に対応します．

example (P Q : Prop) : P ∧ Q → Q ∧ P := by
  sorry

論理結合子とデータ構造: constructor，match，cases¶

演習¶

論理結合子とデータ構造: `constructor`，`match`，`cases`¶