Improving the error for `cases p` when `p` is a proposition

Stream: lean4

[Kyle Miller]

Yesterday on a project, someone I was working with accidentally did cases p instead of by_cases p and was puzzled by the cryptic message

tactic 'cases' failed, major premise type is not an inductive type
  Prop

and we thought "there's got to be a way to improve this, right?" The PR lean4#6378 has some possible improvements, and I'd appreciate feedback. (Side note: thinking a bit laterally, I wondered "couldn't cases p just work?" but cases and by_cases are sufficiently different that it might be too confusing.)

Added explanation when the type is Prop:

example (p : Prop) : True := by
  cases p
/-
error: tactic 'cases' failed, major premise type is not an inductive type
  Prop

Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
in which a term could have been constructed. The 'Prop' universe is not an inductive type however,
so 'cases' does not apply. Consider using the 'by_cases' tactic, which enables true/false reasoning.
p : Prop
⊢ True
-/

Added explanation when the type is a type universe:

example (α : Type) : True := by
  cases α
/-
error: tactic 'cases' failed, major premise type is not an inductive type
  Type

Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
in which a term could have been constructed. Type universes are not inductive types however, so such
case-based reasoning is not possible. This is a strong limitation. According to Lean's underlying
theory, the only distinguishing feature of types is their cardinalities.
α : Type
⊢ True
-/

Added explanation for other types:

example (f : Bool → Bool) : True := by
  cases f
/-
error: tactic 'cases' failed, major premise type is not an inductive type
  Bool → Bool

Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
in which a term could have been constructed. It can sometimes be helpful defining an equivalent
auxiliary inductive type to apply 'cases' to instead.
f : Bool → Bool
⊢ True
-/

[Johan Commelin]

This looks really helpful!

[Johan Commelin]

Should we also have something like this?

example (i : Fin 3) : True := by
  cases α
/-
error: tactic 'cases' failed, major premise type is not an inductive type
  Type

Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
in which a term could have been constructed. `Fin 3` is not a inductive type however,
so 'cases' does not apply. Consider using the 'fin_cases' tactic, ...
-/

[Kyle Miller]

The third explanation is definitely the weakest of the three. Do you have any idea how to phrase suggesting that there are other tactics that might be available in other projects? A problem with referring to fin_cases is that it's only in mathlib.

[Mario Carneiro]

also you didn't do cases i there, of course that won't work

[Mario Carneiro]

but more problematic for your suggestion @Johan Commelin is that cases i does work already, because Fin 3 is an inductive type

[Mario Carneiro]

so it's difficult to give a suggestion without breaking the cases where this is being done on purpose

[Kyle Miller]

That's all true @Mario Carneiro, but a bit beside the point — we should be assuming we're in a situation where cases fails, and changing cases to fail on purpose for inductive types is out of the question.

In my third example that's something enumerating a Fintype would work for, but it's hard to come up with any generic advice.

[Mario Carneiro]

isn't that what I said?

[Mario Carneiro]

are you saying that fin_cases i works in situations where i is not an inductive type?

[Kyle Miller]

Yes, can't it work for something like all functions Bool -> Bool?

[Mario Carneiro]

oh because it works on A : Type such that Fintype A

[Mario Carneiro]

One way to do this would be to give cases an extensible hook for error reporting

[Mario Carneiro]

and fin_cases can try itself on failed cases applications and suggest itself if successful

[Kyle Miller]

That's crossed my mind, but I worry it's a lot of engineering for something that happens really infrequently. Almost all the time the term is going to be for an inductive type.

[Mario Carneiro]

although I worry about getting too fancy here because tactic failure is something that can also happen on purpose and running slow things on tactic failure causes problems for try cases

[Eric Wieser]

Mario Carneiro said:

One way to do this would be to give cases an extensible hook for error reporting

Could this be implemented today with a linter inspecting the infotree?

[Mario Carneiro]

it would be better to put such smarts in a linter

[Kyle Miller]

We have a trick for this already, which is inserting the additional friendly diagnostics into lazy messages.

[Kyle Miller]

That's how decide works for example

[Mario Carneiro]

Kyle Miller said:

That's crossed my mind, but I worry it's a lot of engineering for something that happens really infrequently. Almost all the time the term is going to be for an inductive type.

I think that's a bit of a silly argument, errors happen infrequently only if you don't make mistakes

[Mario Carneiro]

Language error messages are usually make or break for the user experience

[Kyle Miller]

Would you mind trying to "yes and" here? You can see this thread is about trying to improve the error messages to improve the user experience, right?

[Mario Carneiro]

right, so I'm not sure what your argument is

[Mario Carneiro]

Having a hook is a way to solve the problem (which TBH I wish didn't exist) that "lean doesn't want to ever recommend things in mathlib even if there is good reason to"

[Kyle Miller]

I'm worrying that this is an engineering investment (making an extensible framework just to add mentioning fin_cases to the error message for cases) and it's very rare that someone will be doing cases on a function type. Even doing fin_cases on a function type seems to be very rare.

[Kyle Miller]

So why suggest doing something that no one really does?

[Mario Carneiro]

There does not have to be a lot of work to make something extensible. The barest version is you stick it in an IO ref and use it

[Mario Carneiro]

I do something like this to make ring suggest ring_nf

[Mario Carneiro]

even though ring_nf is defined after ring

[Kyle Miller]

Look, I get that and know how to implement it. This is code that needs to be maintained, so thinking about the added complexity is necessary as part of the engineering.

[Mario Carneiro]

https://github.com/leanprover-community/mathlib4/blob/8fe8834dbbef8a87e09d0ba3ef2854a643b60521/Mathlib/Tactic/Ring/Basic.lean#L1192-L1225

[Kyle Miller]

The question that needs to be exhausted first is "would a blurb be enough"? Or "can we suggest that there might be type-specific tactics that may or may not help"? And also "is this a place where we can break the rule and refer to a mathlib tactic"?

example (f : Bool → Bool) : True := by
  cases f
/-
error: tactic 'cases' failed, major premise type is not an inductive type
  Bool → Bool

Explanation: the 'cases' tactic is for constructor-based reasoning, with cases exhausting every way
in which a term could have been constructed. It can sometimes be helpful defining an equivalent
auxiliary inductive type to apply 'cases' to instead.
f : Bool → Bool
⊢ True
-/

[Mario Carneiro]

it doesn't need to be a huge deal or require maintenance any more than any other kind of code

[Mario Carneiro]

A basic blurb you could add which doesn't try to do too much analysis is "You may have confused this tactic with 'by_cases' or 'fin_cases' (in mathlib)"

[Mario Carneiro]

made better if you can make those links to HTML doc pages of some kind

[Kyle Miller]

I respectfully disagree that adding a hook to extend error messages that is intended to be used by downstream projects doesn't need much thought. I'd like to avoid this if possible, since I don't want to guarantee anything about support or stability (rather, I don't want to do the design work to be able to guarantee this). The ring/ring_nf example is different since it's all under the purview of mathlib in the end.

Thanks for the "you may have confused ..." suggestion. I'll keep it in mind, and something like that might work.

[Mario Carneiro]

if you don't want to guarantee support or stability, then put that in the docstring, just like anything else

[Mario Carneiro]

lean core already has many many public functions with every possible stance on support or stability

[Kyle Miller]

I'd then ask mathlib not to use it, and then it wouldn't be used for its raison d'être, mentioning fin_cases.