Zulip Chat Archive

Stream: new members

Topic: Nested pattern matching in cases


Rudy Peterson (Jan 05 2025 at 23:19):

In Lean 4, I am trying to do nested pattern matching in case analysis, however I am running into errors.

namespace nested.examples
section andor
variable (p q r : Prop)

theorem ex1 : p  (q  r)  (p  q)  (p  r) := by
  intro
  | Or.inl hp =>
    exact ⟨.inl hp, .inl hp
  | Or.inr hq, hr =>
    exact ⟨.inr hq, .inr hr

theorem ex2 : p  (q  r)  (p  q)  (p  r) := by
  intros hpqr
  cases hpqr
  case Or.inl hp =>
    exact ⟨.inl hp, .inl hp
  case Or.inr hq, hr =>
    exact ⟨.inr hq, .inr hr

theorem ex3 : p  (q  r)  (p  q)  (p  r) := by
  intros hpqr
  cases hpqr with
  | Or.inl hp =>
    exact ⟨.inl hp, .inl hp
  | Or.inr hq, hr =>
    exact ⟨.inr hq, .inr hr
end andor
end nested.examples

ex works fine, but ex2 and ex3 both get the same error when I try to do the nested pattern matching in the Or.inr case:

Messages below:
17:13:
unexpected token '⟨'; expected '=>'
25:10:
unexpected token '⟨'; expected '=>'

Is there a way to do nested pattern matching in cases?

Thanks!

Kevin Buzzard (Jan 05 2025 at 23:33):

You can use mathlib's rcases (I know this doesn't answer the question)

import Mathlib

variable (p q r : Prop)

theorem ex2 : p  (q  r)  (p  q)  (p  r) := by
  intro hpqr
  rcases hpqr with hp | hq, hr
  · exact ⟨.inl hp, .inl hp
  · exact ⟨.inr hq, .inr hr

Kyle Miller (Jan 06 2025 at 04:30):

cases looks like it would be similar to intro's pattern matching, but it uses a different system. (You have to label cases with inl and inr rather than Or.inl and Or.inr too, though that doesn't help with the further pattern matching.)

Instead, there's match for the equivalent to what intro can do:

theorem ex3 : p  (q  r)  (p  q)  (p  r) := by
  intros hpqr
  match hpqr with
  | Or.inl hp =>
    exact ⟨.inl hp, .inl hp
  | Or.inr hq, hr =>
    exact ⟨.inr hq, .inr hr

Last updated: May 02 2025 at 03:31 UTC