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