Stream: lean4

Topic: nested patterns in cases?

Jason Gross (Mar 08 2021 at 14:32):

Is there a tactic that allows nested cases such as def x (n : Nat) : Unit := by cases n with | Nat.zero => _ | Nat.succ (Nat.succ _) => _ | Nat.succ _ => _

Leonardo de Moura (Mar 08 2021 at 14:37):

Lean 4 has a match tactic. The syntax is similar to match expressions

def f : Nat → Nat
| 0   => 1
| 1   => 2
| n+2 => 3

theorem ex (n : Nat) : f n > 0 := by
match n with
| 0  => simp [f]
| 1  => simp [f]
| Nat.succ (Nat.succ _) => simp [f]


Jason Gross (Mar 08 2021 at 14:41):

Hm, match, unlike cases, seems to suffer from the same issues in unifying metavariables with expressions as the non-tactic-mode elaborator (point (3) in https://github.com/leanprover/lean4/issues/337)

Jason Gross (Mar 08 2021 at 14:43):

(I am in fact using cases right now just to get around typing issues with nested patterns in the standard elaborator :-/ . I expect this will be useful in the future, though, so thanks!)

Last updated: May 18 2021 at 22:15 UTC