What is "case" and what is it used for?

Stream: lean4

[Kevin Buzzard]

There's something in the infoview which I always ignore, but I'm writing documentation for undergraduates so am suddenly paying attention to everything. In this code (my first example explaining the mathlib convert tactic)

import Mathlib.Tactic

example (a b c d e : ℝ) (f : ℝ → ℝ) (h : f (a + b) + f (c + d) = 37) :
    f (a + b) + f (c + e) = 37 := by
  convert h
  -- ⊢ e = d
  sorry

when the goal is e = d it also says at the top of the infoview case h.e'_2.h.e'_6.h.e'_1.h.e'_6, which looks like total gobble-de-gook to me (and hence will look like gobble-de-gook to the students, which is not ideal). I also occasionally notice "case" in the middle of long proofs when it seems to have become very long.

Given that I've got this far without having a clue what this thing is, and the output in the above example is nothing but confusing, is it possible to switch it off? Alternatively is someone going to tell me that this is somehow an important thing and my Lean skillz would be upgraded if I started paying attention to it? I wonder whether this confusion on my part is due to the fact that I am resolutely a cases' person, I think the whole Lean 4 ascii art involved in cases is confusing to mathematicians (and to me) so I typically avoid it; I neither know nor care what the names of the constructors of Or are and I don't think I should be expected to know. Or is this unrelated to "case"?

[Patrick Massot]

Kevin Buzzard said:

Given that I've got this far without having a clue what this thing is, and the output in the above example is nothing but confusing, is it possible to switch it off?

Yes. You can go to the extension settings to kill it. And remember your repo can include a file with VSCode settings.

[Eric Rodriguez]

your hunch is right, btw, and when it works it can be nice-ish:

image.png

sadly I think convert and refine always make some completely nonsensical case names, so therefore I agree with you that all I ever see is complete nonsense

[Kevin Buzzard]

Aren't names of hypotheses an implementation detail??

Patrick is dead right, these are apparently "names" and there's an option "Show Goal Names" which I've now turned off :-)

[Eric Rodriguez]

I guess the idea is that you can pretty them up for inductions :)

[Eric Rodriguez]

But I agree in principle

[Damiano Testa]

I consider names of hypotheses a little less of an implementation detail now that you can "call out" implicit arguments via apply thm (a := 0).

[Mario Carneiro]

Goal names are more than an implementation detail, they show up in ?a and case a =>

[Eric Rodriguez]

i don't think I've ever seen refine named cases be useful for much; as far as I know they just let you call them up earlier with case? It'd be nice if I could reuse it to mean "I want to use the same metavariable I defined before"

[Mario Carneiro]

That "it would be nice" is already the case, but IMO it's a misfeature

[Mario Carneiro]

because unlike regular names, goal names are not hygienic

[Eric Rodriguez]

I've never seen it work properly, and I've tried it a couple times. Why do you think it's a misfeature?

[Eric Rodriguez]

Oh, so there can be duplication?

[Damiano Testa]

I considered using those names as an "internal" working of tactics, where you make your own lemmas with their meaningful names for hypotheses and then you seek out the goals with the right name. It felt a little hacky, but it worked. Personally, I find it similar to using mdata, but more ad hoc...

[Mario Carneiro]

example (f : (x y : Nat) → True) : True := by
  have : True := by
    refine f ?a ?b
    exact 3
    exact 4
  have : True := by
    refine f ?a ?b
    -- done already
  have : True := by
    apply f
    · exact 1
    · exact 2
  have : True := by
    refine f ?x ?y
    -- done already
  let _z := ?x -- z = 1
  trivial

[Mario Carneiro]

can you spot where ?x was assigned?

[Mario Carneiro]

Kevin Buzzard said:

I wonder whether this confusion on my part is due to the fact that I am resolutely a cases' person, I think the whole Lean 4 ascii art involved in cases is confusing to mathematicians (and to me) so I typically avoid it; I neither know nor care what the names of the constructors of Or are and I don't think I should be expected to know. Or is this unrelated to "case"?

Note that this is actually about the case tactic, which has nothing to do with the cases tactic (or cases' which is similar), except that if you use cases' you are more likely to need case if you want to refer to the subcases rather than just proving them in the order they were given

[Damiano Testa]

This feels unhygienic to me!

Btw, the online lean server does not appear to show the case names.

[Mario Carneiro]

I know that mathematics rarely involves inductive types with more than two constructors (and one two-constructor inductive in particular), but if you ever have to deal with them you will want to be able to name them for clarity rather than just doing proofs in a randomish order. In fact, the same issue can arise when proving things with rw or applying a theorem with many hypotheses, you can end up with a ton of parallel subgoals, and it is good to refer to them by name if you want to make the proof script clearer

[Kevin Buzzard]

If I apply Finset.induction_on or something like that, and suddenly end up with 4 goals, I just put four dots and prove the four goals. Who cares what these goals are "called"? Oh -- you're saying that for readability you like "this is the 0 case" etc?

[Mario Carneiro]

yes

[Mario Carneiro]

case also has the secondary benefit that you can name the inaccessible variables that were created in each case, which allows you to write just bare cases x and then name the variables in the case instead of in a long list after

[Kevin Buzzard]

Yeah I don't think like that, I just think "this is one of the goals which needs proving at this point"

[Mario Carneiro]

I mean that makes sense when you are playing the lean game

[Mario Carneiro]

but if you want to maintain proofs over time it can be helpful

[Mario Carneiro]

there is also next =>, which also lets you name variables via next a b c => but doesn't name the case, so it's equivalent to . rename_i a b c; ...

[Kevin Buzzard]

I'm looking forward to starting FLT. For the first time I'll have to worry about things like bumping mathlib (Patrick and Johan did all the bumps with perfectoid) and I'm sure it'll teach me a lot.

[Mario Carneiro]

oh yes, maintaining a body of lean code will be a new experience for you

[Patrick Massot]

Kevin, note this infoview option was part of https://github.com/leanprover/vscode-lean4/pull/302/files which brought other options for teaching purposes.

[Ruben Van de Velde]

Hmm, when I was younger doing induction on paper, I'd usually mark the subgoals as "base case" and "inductive case" explicitly - this seems similar

[Mario Carneiro]

speaking of proof goal options, I really want an option to not show variables which are in common between all goals. When I have 4 goals with 30 hypotheses and the first 28 are the same this is so difficult to work with

[Kevin Buzzard]

I feel extremely lucky in this community that whenever I run into things, someone who knows how to solve them has often run into them earlier.

[Kevin Buzzard]

But variables getting out of hand is currently not one of those things ;-)

[Eric Rodriguez]

Patrick Massot said:

Kevin, note this infoview option was part of https://github.com/leanprover/vscode-lean4/pull/302/files which brought other options for teaching purposes.

these options are incredible and I'm sad I just noticed them now!

[James Gallicchio]

Mario Carneiro said:

I really want an option to not show variables which are in common between all goals

this would be lifechanging, not gonna lie. i would react all of the github emojis on an RFC for this

[Heather Macbeth]

Patrick Massot said:

And remember your repo can include a file with VSCode settings.

@Kevin Buzzard, here is the VS Code settings file for my teaching repo, which includes the "turn off case names" setting as well as several others:
https://github.com/hrmacbeth/math2001/blob/main/.vscode/settings.json

Highly recommend doing something like this in your teaching repo!

[Patrick Massot]

You can improve it a bit with

    "editor.semanticTokenColorCustomizations": {
        "rules": {"leanSorryLike": "#FF0000"},
        "[Default Light+]": {"rules": {"variable": "#1a31da"}}
    },

[Patrick Massot]

See here