Zulip Chat Archive

Stream: new members

Topic: Naming cases' variables

Alex (Sep 07 2023 at 15:27):

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?
 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 (Sep 07 2023 at 15:31):

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

Jireh Loreaux (Sep 07 2023 at 15:39):

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 (Sep 07 2023 at 15:40):

@Kevin Buzzard :up:

Adam Topaz (Sep 07 2023 at 16:22):

TIL! FYI, this also works with induction!

Jireh Loreaux (Sep 07 2023 at 16:51):

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

Jireh Loreaux (Sep 07 2023 at 16:52):

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 (Sep 07 2023 at 17:27):

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 (Sep 07 2023 at 17:38):

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

Alex (Sep 08 2023 at 13:39):

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

Jireh Loreaux (Sep 08 2023 at 13:41):

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

Mario Carneiro (Sep 08 2023 at 19:14):

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

Last updated: Dec 20 2023 at 11:08 UTC