Difference between `match h with` and `cases h with`

Stream: new members

[Ying Xiong]

I am reading "Theorem Proving in Lean 4", chapter 5: Tactics. I saw a few examples using match and cases, e.g.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    cases h.right with
    | inl hq => exact Or.inl ⟨h.left, hq⟩
    | inr hr => exact Or.inr ⟨h.left, hr⟩
  . intro h
    cases h with
    | inl hpq => exact ⟨hpq.left, Or.inl hpq.right⟩
    | inr hpr => exact ⟨hpr.left, Or.inr hpr.right⟩

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    match h with
    | ⟨_, Or.inl _⟩ => apply Or.inl; constructor <;> assumption
    | ⟨_, Or.inr _⟩ => apply Or.inr; constructor <;> assumption
  . intro h
    match h with
    | Or.inl ⟨hp, hq⟩ => constructor; exact hp; apply Or.inl; exact hq
    | Or.inr ⟨hp, hr⟩ => constructor; exact hp; apply Or.inr; exact hr

But I don't quite appreciate the difference of the two, and it seems to me that they can be used interchangably. Can someone shed some light on this? Thanks!

[Kyle Miller]

cases does one thing: apply the "cases eliminator" for the type. The syntax for each case is restrictive, and it can only be constructorname arg1 arg2 ... argn or @constructorname arg1 arg2 ... argn where each argi is a variable name.

match is more complicated and can use full pattern matching for each case. It can also support matching multiple discriminators with match h1, h2, h3 with .... However, my understanding is that the way in which it generalizes the local context is not as strong as cases, but I don't have any examples on hand.

There's a third alternative, which is the rcases/obtain/rintro family, which has its own destructuring language.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    obtain ⟨_, _ | _⟩ := h
    · apply Or.inl; constructor <;> assumption
    · apply Or.inr; constructor <;> assumption
  . rintro (⟨hp, hq⟩ | ⟨hp, hr⟩)
    · constructor; exact hp; apply Or.inl; exact hq
    · constructor; exact hp; apply Or.inr; exact hr