Naming cases' variables

Stream: new members

[Alex]

How do I name variables and hypothesis generated by cases? I understand Coq's destruct var as [H a b | H' a b c], but don't get how you're supposed to do it with Lean's default cases/induction.

theorem ex : (gt0 : { a : Nat // a > 0 }) -> match gt0 with
 | Subtype.mk a p => {b : Nat // b = a - 1 /\ b < a} := by
 intros gt0
 cases gt0 --auto names a as val?
 simp
 cases val --unknown identifier val

I couldn't get different variants of cases from the documentation and couldn't get it to work. Should I just use Mathlib's rcases, which seems to have a syntax I want?

[Kevin Buzzard]

I always use rcases or cases' because I can never get my head around the 2d syntax of cases

[Jireh Loreaux]

There's a code action for this. When you type cases gt0, there should be a light bulb that pops up. You can click it (or in VS Code type Ctrl+.) and click "Generate and explicit pattern match for 'cases'", so you never have to remember!

[Jireh Loreaux]

@Kevin Buzzard :up:

[Adam Topaz]

TIL! FYI, this also works with induction!

[Jireh Loreaux]

Indeed it does. The only thing to watch out for: if you type slightly too much the :idea: pop-up disappears

[Jireh Loreaux]

There are also code actions for calc blocks to generate new lines for you. I think Patrick demonstrated this in the video he made to celebrate the end of the port.

[Patrick Massot]

Those are not yet in mathlib. But I'll be able to resume work on this since https://github.com/EdAyers/ProofWidgets4/pull/16 got merged yesterday.

[Jireh Loreaux]

That would explain why I haven't yet been using them!

[Alex]

@Jireh Loreaux In VS? I'm using emacs.
@Kevin Buzzard fin2.cases'?

[Jireh Loreaux]

I use emacs, but not for Lean, so I'm unfamiliar with the chords relevant to this. Maybe C-x .? (Just guessing)

[Mario Carneiro]

Jireh Loreaux said:

Indeed it does. The only thing to watch out for: if you type slightly too much the :idea: pop-up disappears

this is now fixed on std master - it will trigger on cases e and cases e with now, although cases e with a trailing space will not trigger if your cursor is after the space