Agda style interactive case splitting?

Stream: Is there code for X?

[Solomon]

Is there any way to do agda style case splitting? I imported import «Std».CodeAction but the only suggestion for holes is to start a tactics proof.

[Johan Commelin]

I don't know what agda style case splitting is...
If you import Std you might get more code actions. And if you import Mathlib you might get even more.
Can you give an #mwe of what you are expecting?

[Solomon]

In Agda if you have a function with a hole in it like this:

def foo : (n : ℕ) → ℕ := _

You can press a ctrl-c ctrl-c on the hole and enter the variable name and it will insert a pattern match on the variable. This is incredibly helpful, especially when working with inductive types and sigma types.

[Joachim Breitner]

That would be great to have. I think we have something similar where you write

import Mathlib
def foo (n : ℕ) : ℕ := by
  induction n with

(but not match n with, for whatever reason) and you get a code action to complete it to

import Mathlib
def foo (n : ℕ) : ℕ := by
  induction n with
  | zero => sorry
  | succ n ih => sorry

so doing it for function definitions should be possible as well.

[Kyle Miller]

At least if the type is a function you can generate the pattern match:

image.png

def foo : ℕ → ℕ := fun
  | .zero => _
  | .succ n => _

[Joachim Breitner]

Nice! I need to get better at discovering and using these code actions

[Kyle Miller]

It'd be neat if match n would generate a code action too!

[Patrick Massot]

Yes, every now and then I rediscover it doesn’t and I’m disappointed.

[Kyle Miller]

This has made me wonder why it is again we need nomatch syntax. Wouldn't match x with no with clause suffice for nomatch x?

Then match x by itself could suggest a code action with the cases you need to handle, if indeed there are any cases you need to handle.

[Solomon]

Kyle Miller said:

At least if the type is a function you can generate the pattern match:

image.png

def foo : ℕ → ℕ := fun
  | .zero => _
  | .succ n => _

What do i need to import to get this code action?

[Mario Carneiro]

Patrick Massot said:

Yes, every now and then I rediscover it doesn’t and I’m disappointed.

Maybe you should report an issue or ping me when these things happen ;)

[Mario Carneiro]

Kyle Miller said:

This has made me wonder why it is again we need nomatch syntax. Wouldn't match x with no with clause suffice for nomatch x?

Then match x by itself could suggest a code action with the cases you need to handle, if indeed there are any cases you need to handle.

I think we should also allow match x with an (empty) with, along the lines of lean#3555

[Mario Carneiro]

I don't like that nomatch requires learning a new keyword, it's less discoverable.

[Mario Carneiro]

But I guess it's too late now to stop the nofun in 4.7.0-rc1 which is imminent...

[Joachim Breitner]

It’s only a release candidate, I'd say it is only fair to listen to feedback from our rc beta testers (i.e. mathlib) :-)

To me it seems reasonable for match x with to be accepte instead of nomatch x, but I didn’t follow the discussions around nomatch and nofun fully. OTOH, the nomatch is a nice explicit herald. :shrug:

[Joachim Breitner]

I also wonder if the nofun keyword is necessary if (nomatch \.) is equivalent (assuming it is)

[Mario Carneiro]

nofun is to fun | a => _ | b => _ as nomatch x is to match x with | a => _ | b => _

[Mario Carneiro]

It's also not equivalent to that, it's equivalent to (nomatch ., ., .) with the appropriate number of .

[Mario Carneiro]

that is, the empty argument might not be the first one

[Mario Carneiro]

although, having written that, the nomatch a, b form is hella ambiguous and I think it's a good argument for match a, b with working

[Mario Carneiro]

I didn’t follow the discussions around nomatch and nofun fully

There weren't really any (at least not in public), it was a suggestion and then an implementation. I recall Scott mentioning that he was surprised it was taken seriously

[Mario Carneiro]

The implementation is based on fun. and match x with. which I added to std to replace uses of the empty pattern match (match x with end and def foo : empty -> A.) in lean 3

[Mario Carneiro]

the dot was there to avoid ambiguity with the lean parser, it would not have been necessary if implemented in core, but then it got absorbed into core

[Mario Carneiro]

Although another syntax suggestion that is making the rounds in rust land is the "never pattern" !, and some discussion about deprecating match x {} in favor of match x { ! }. Agda uses () as a never pattern but I think that's not an option in either lean or rust because that means the value of the unit type

[Mario Carneiro]

The lean version of that might look like fun | !

[Mario Carneiro]

but on the other hand lean doesn't use ! as syntax for the empty type, and adding it as a term would probably make for lots of ambiguity with all the other uses of !