expanding cases syntax

Stream: lean4

[Yakov Pechersky]

What's the right approach to get lean3 style cases h with hp hq hr working? Here's a test case for And that I am not sure how to get working

-- this is the existing way
example {p q : Prop} (h : And p q) : q := by
  cases h with | _ hp hq => _
  exact hq

syntax "cases" term "with" ident withPosition(ident) : tactic

macro_rules
  | `(tactic| cases $d:term with $p:ident $q:ident) => `(tactic| cases $d with | _ $p $q => ?_)

-- my attempt
example {p q : Prop} (h : And p q) : q := by
  cases h with hp hq
  -- failed with
  -- elaboration function for 'missing' has not been implemented
  -- [Error pretty printing syntax: unknown constant 'missing'. Falling back to raw printer.]
  -- <missing>
  sorry

[Yakov Pechersky]

Reading the rss feed, I guess my usage of | _, specifically _ was the problem?

[Sebastian Ullrich]

No, that was unrelated :)

[Sebastian Ullrich]

If something goes wrong in expanded syntax, adding antiquotation kinds is always the best first move

macro_rules
  | `(tactic| cases $d:term with $p:ident $q:ident) => `(tactic| cases $d:term with | _ $p $q => ?_)

[Sebastian Ullrich]

This is because cases can accept a sequence of targets (which in turn can be more than just a term): https://github.com/leanprover/lean4/blob/a0eff55772c7c02e6e203dccda9c7ee51b623146/src/Init/Notation.lean#L296

[Kevin Buzzard]

Thanks Yakov and Sebastian!

[Yakov Pechersky]

(Now to get the variadic one working ...)

[Yakov Pechersky]

Why does the first example work, and what about the semicolon makes it work?

structure And3 (a b c : Prop) : Prop where
  intro :: (first : a) (second : b) (third : c)

variable {p q r : Prop}

syntax "cases" term "with" ident withPosition(ident)+ : tactic

macro_rules
  | `(tactic| cases $d:term with $p:ident $q:ident) => `(tactic| cases $d:term with | _ $p $q => ?_) -- nil case

-- works, but why?
example (h : And3 p q r) : q := by
  cases h with hp hq; -- notice semicolon here
  exact hq

-- this breaks, as I think it should
example (h : And3 p q r) : q := by
  cases h with hp hq -- parse error because we did not deal with the cons case
  exact hq

[Yakov Pechersky]

Ah the working example is that match destructs across all the structure/inductive fields; the third one is hidden under an unhygienic name