## Stream: lean4

### Topic: expanding cases syntax

#### Yakov Pechersky (Mar 23 2021 at 18:05):

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 (Mar 23 2021 at 18:16):

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

#### Sebastian Ullrich (Mar 23 2021 at 18:16):

No, that was unrelated :)

#### Sebastian Ullrich (Mar 23 2021 at 18:18):

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 (Mar 23 2021 at 18:20):

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 (Mar 23 2021 at 18:22):

Thanks Yakov and Sebastian!

#### Yakov Pechersky (Mar 23 2021 at 18:23):

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

#### Yakov Pechersky (Mar 23 2021 at 18:42):

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 (Mar 23 2021 at 19:15):

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

Last updated: May 07 2021 at 12:15 UTC