EReal

Stream: mathlib4

[Michael Stoll]

Context: The abscissa of (absolute) convergence of an L-series is naturally an EReal (i.e., between -∞ and ∞ inclusive). So I need to work with EReals in this context. See also here.

My most fundamental question in this regard is: can we hide the ugly implementation-detail asymmetry of the definition and have cases x (with x : EReal) accept three match arms of the form ⊥ => ..., ⊤ => ... and (Real.toEReal y) => ...? I can use match x with, but then I have to write some (some y) in the last alternative and in many cases change that to ↑y manually to be able to work with it.

One attempt:

import Mathlib.Data.Real.EReal

lemma EReal.elim {α : EReal → Sort*} (motive : EReal) (hb : α ⊥) (ht : α ⊤) (hr : ∀ y : ℝ, α y) :
    α motive :=
  match motive with
  | ⊥ => hb
  | ⊤ => ht
  | (some (some y)) => hr y

syntax (name := casesEReal) "casesEReal" term "with" term : tactic

macro_rules | `(tactic| casesEReal $x:term with $y:term) => `(tactic|
  refine EReal.elim $x ?_ ?_ (fun $y ↦ ?_))

variable (P : EReal → Prop)

example (x : EReal) : P x := by
  casesEReal x with y
  -- 3 goals: ⊢ P ⊥, ⊢ P ⊤, y: ℝ ⊢ P ↑y
  all_goals sorry

But it would be nice to teach the existing cases, rcasesetc. to use EReal.elim. Is this at all possible?

[Antoine Chambert-Loir]

Isn't it docs#EReal.rec (up to the order of parameters)?

[Michael Stoll]

I missed that somehow.
Still, induction x using EReal.rec feels a bit unnatural as there is no induction hypothesis.

[Yaël Dillies]

Sadly, custom default recursors are not there yet. We've been wanting them for a while.

[Michael Stoll]

... and induction x using EReal.rec with y apparently does not work to name the real number in the main case...

[Michael Stoll]

...using case labels is also ugly:

lemma exists_between_ofReal_left {x : EReal} {z : ℝ} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z := by
  obtain ⟨a, ha₁, ha₂⟩ := exists_between h
  induction a using EReal.rec
  case intro.intro.h_bot => simp only [not_lt_bot] at ha₁
  case intro.intro.h_top => simp only [not_top_lt] at ha₂
  case intro.intro.h_real a₀ => exact ⟨a₀, by exact_mod_cast ha₁, by exact_mod_cast ha₂⟩

[Yaël Dillies]

Michael Stoll said:

... and induction x using EReal.rec with y apparently does not work to name the real number in the main case...

Have you tried induction' x using EReal.rec with y?

[Michael Stoll]

Can that be improved so that the case have names like bot, top and ofReal?

[Yaël Dillies]

Once again, this is a missing Lean feature that we've been petitioning for

[Michael Stoll]

induction' allows to name the variable, but I got the impression that induction' is a crutch used for the port of mathlib.

[Yaël Dillies]

It was originally presented that way, but the new induction syntax is so unergonomic that I really doubt we'll actually switch from induction' to induction everywhere.

[Michael Stoll]

I assume using the case names is preferred as that does not rely implicitly on the order of arguments of EReal.rec. So it would be nice to have nicer names.

[Yaël Dillies]

That too is really up for debate.

[Eric Rodriguez]

Yaël Dillies said:

It was originally presented that way, but the new induction syntax is so unergonomic that I really doubt we'll actually switch from induction' to induction everywhere.

I think this is the long-term idea, although I'm not a tremendous fan either, to be honest.

[Alex J. Best]

You can tag your lemma with @[eliminator] seems to work fine to me

import Mathlib.Data.Real.EReal
@[eliminator]
lemma EReal.elim {α : EReal → Sort*} (motive : EReal) (hb : α ⊥) (ht : α ⊤) (hr : ∀ y : ℝ, α y) :
    α motive :=
  match motive with
  | ⊥ => hb
  | ⊤ => ht
  | (some (some y)) => hr y

syntax (name := casesEReal) "casesEReal" term "with" term : tactic

macro_rules | `(tactic| casesEReal $x:term with $y:term) => `(tactic|
  refine EReal.elim $x ?_ ?_ (fun $y ↦ ?_))

variable (P : EReal → Prop)

example (x : EReal) : P x := by
  casesEReal x with y
  -- 3 goals: ⊢ P ⊥, ⊢ P ⊤, y: ℝ ⊢ P ↑y
  all_goals sorry

example (x : EReal) : P x := by
  cases x
  -- 3 goals: ⊢ P ⊥, ⊢ P ⊤, y: ℝ ⊢ P ↑y
  all_goals sorry

[Michael Stoll]

Then also cases' x with y works.
However, the yellow lightbulb appearing on cases still generates cases none and some val...

[Michael Stoll]

Would it be reasonable to add this to Mathlib as well?

[Alex J. Best]

I think so yes, I think we are missing out by not using this feature more.
And the light bulb thing sounds like a bug indeed!

[Mario Carneiro]

I don't think the code action supports cases using

[Michael Stoll]

But cases works without using?

[Mario Carneiro]

yes?

[Mario Carneiro]

sorry I'm not sure what the bug report is here

[Michael Stoll]

import Mathlib.Data.Real.EReal

@[eliminator]
lemma EReal.elim {α : EReal → Sort*} (motive : EReal)
    (bot : α ⊥) (top : α ⊤) (ofReal : ∀ y : ℝ, α y) :
    α motive :=
  match motive with
  | ⊥ => bot
  | ⊤ => top
  | (some (some y)) => ofReal y

variable (P : EReal → Prop)

example (x : EReal) : P x := by
  cases x with
  | bot => sorry
  | top => sorry
  | ofReal y => sorry

[Mario Carneiro]

oh, you are using @[eliminator] as an auto-using

[Mario Carneiro]

yeah that's not supported either

[Michael Stoll]

Which eliminator is picked by cases and which by the lightbulb?

[Mario Carneiro]

in fact it will probably cause things to be really weird since it will generate case names that don't match what cases thinks

[Mario Carneiro]

the code action only ever looks at the inductive type

[Mario Carneiro]

i.e. as if you didn't use using or @[eliminator]

[Alex J. Best]

I guess https://github.com/leanprover/std4/blob/03a0f24da542fcf3fd60d9a9de9db6c5af0391f7/Std/CodeAction/Misc.lean#L283 is the relevant code, the code action just uses typename.casesOn

[Michael Stoll]

So we should redefine EReal.casesOn? (If that's possible...)

[Mario Carneiro]

what's the goal?

[Michael Stoll]

To have cases x give the natural trichotomy on x : EReal (and the lightbulb to do the same).

[Mario Carneiro]

the lightbulb thing is a bug, it doesn't reflect what cases actually does and gives wrong hints as a result. Assuming that issue is fixed, are there any other bugs?

[Alex J. Best]

The goal is that in the presence of @[eliminator] the light bulb produces working code

[Alex J. Best]

No I think thats it!