if-then-else needs [decidable] but by_cases doesn't!?

Stream: general

[Chris Wong]

Is there some magic in by_cases that lets it decide l = [] without classical reasoning? And if so, how can I use it in term mode?

-- Works!?
example {α} (l : list α) : l = [] ∨ l ≠ [] :=
by { by_cases l = [], exact or.inl h, exact or.inr h }

-- Error: "failed to synthesize type class instance for ... ⊢ decidable (l = list.nil)"
example {α} (l : list α) : l = [] ∨ l ≠ [] :=
if h : l = [] then or.inl h else or.inr h

[Chris Wong]

Never mind, this works as well so I'm pretty sure by_cases just uses excluded middle :P

import data.real.basic

example (l : list ℝ) : l = [42] ∨ l ≠ [42] :=
by { by_cases l = [(42 : ℝ)], exact or.inl h, exact or.inr h }

[Reid Barton]

Yes, I think by_cases was upgraded to use classical automatically

[Chris Wong]

Interesting. Does this mean the documentation is out of date? ("This tactic requires that p is decidable.")

https://leanprover-community.github.io/mathlib_docs/tactics.html#by_cases

[Bhavik Mehta]

I think there's an instance which says l = [] is decidable (even if you don't go classical)

[Gabriel Ebner]

@Chris Wong Yes, the documentation is indeed out of date. That sentence actually comes from mathlib. PRs welcome!

[Reid Barton]

Chris Wong said:

Interesting. Does this mean the documentation is out of date? ("This tactic requires that p is decidable.")

https://leanprover-community.github.io/mathlib_docs/tactics.html#by_cases

It seems so

[Chris Wong]

It looks like by_contra doesn't need decidability either, so we'll need to fix the docs for both

[Chris Wong]

Wait, it does... @Gabriel Ebner what's the reasoning behind by_cases using classical reasoning but by_contra still requiring decidable?

[Gabriel Ebner]

That's simple. I don't use by_contra enough to notice.

[Chris Wong]

https://github.com/leanprover-community/mathlib/pull/3718
https://github.com/leanprover-community/lean/issues/433