Should I be able to use `grind` for this?

Stream: general

[Harry Goldstein]

I have the kind of "uninteresting" lemma that seems like the perfect use-case for automated tactics (e.g., grind), but the current proof I have isn't obviously automatable. Here's the lemma and the proof:

private lemma ennreal_one_of_ge_half_add_half_sq {c : ENNReal}
    (hc_le : c ≤ 1) (h : c ≥ 1 / 2 + 1 / 2 * c ^ 2) : c = 1 := by
  have hc_ne  : c ≠ ⊤     := ne_top_of_le_ne_top ENNReal.one_ne_top hc_le
  have hc2_ne : c ^ 2 ≠ ⊤ := ne_top_of_le_ne_top ENNReal.one_ne_top (pow_le_one₀ (zero_le _) hc_le)
  have hle : c.toReal ≤ 1 := by
    simpa using (ENNReal.toReal_le_toReal hc_ne ENNReal.one_ne_top).mpr hc_le
  have hge : c.toReal ≥ 1 / 2 + 1 / 2 * c.toReal ^ 2 := by
    have h2ne : (1 / 2 + 1 / 2 * c ^ 2 : ENNReal) ≠ ⊤ :=
      ENNReal.add_ne_top.mpr ⟨by norm_num, ENNReal.mul_ne_top (by norm_num) hc2_ne⟩
    have hmono := (ENNReal.toReal_le_toReal h2ne hc_ne).mpr h
    rw [ENNReal.toReal_add (by norm_num) (ENNReal.mul_ne_top (by norm_num) hc2_ne),
        ENNReal.toReal_mul, ENNReal.toReal_pow] at hmono
    norm_num at hmono
    linarith
  have hone : c.toReal = 1 := by nlinarith [sq_nonneg (c.toReal - 1)]
  rw [← ENNReal.ofReal_toReal hc_ne, hone, ENNReal.ofReal_one]

If someone could help me automate this down (and, ideally, tell me the steps they took so I can get a better idea of how to do that for myself in the future), I'd really appreciate it. Or if this is really just more interesting than I thought, and there isn't much more automating to be done, that's fine too.

[Michael Rothgang]

Does the situation improve if you take c to be a Real which is positive? (Writing automation for ENNReal is harder than for Real. For instance, ENNReal is not a ring, so ring does not and will not work for it.)

[Harry Goldstein]

I can't get away from ENNReals completely (since the use-site talks about ENNReals). So I think the real issue here is automating the conversion of a bunch of assumptions about ENNReals to assumptions about Reals so we can solve the goal with nlinarith (which does just solve the goal immediately on Reals.

[David Ledvinka]

Slightly cleaner proof once #35155 is merged:

private lemma ennreal_one_of_ge_half_add_half_sq {c : ℝ≥0∞}
    (hc_le : c ≤ 1) (h : 1 / 2 + 1 / 2 * c ^ 2 ≤ c) : c = 1 := by
  by_cases h_top : c = ∞
  · simp [h_top] at hc_le
  lift c to ℝ≥0 using h_top
  rw [← toNNReal_le_toNNReal, toNNReal_add, toNNReal_mul] at h
  simp only [one_div, toNNReal_inv, toNNReal_pow, toNNReal_coe] at h
  norm_cast at *
  nlinarith
  all_goals finiteness

I have plans to work on automating the conversion of ENNReals to NNReals or Reals but it doesn't exist yet.

[Chris Henson]

This is what I ended up with by very mechanically thinking about what I could unnest from your original proof:

import Mathlib

private lemma ennreal_one_of_ge_half_add_half_sq {c : ENNReal}
    (hc_le : c ≤ 1) (h : c ≥ 1 / 2 + 1 / 2 * c ^ 2) : c = 1 := by
  have : c ≠ ⊤     := ne_top_of_le_ne_top ENNReal.one_ne_top hc_le
  have : c ^ 2 ≠ ⊤ := ne_top_of_le_ne_top ENNReal.one_ne_top (pow_le_one₀ (zero_le _) hc_le)
  have : (1 / 2 : ENNReal) ≠ ⊤ := by norm_num
  have : (1 / 2 + 1 / 2 * c ^ 2).toReal ≤ c.toReal := by grind [ENNReal.toReal_le_toReal]
  have : (1 / 2 : ENNReal).toReal = 1 / 2 := by norm_num
  have : 1 / 2 + 1 / 2 * c.toReal ^ 2 ≤ c.toReal := by
    grind [ENNReal.toReal_add, ENNReal.mul_ne_top, ENNReal.toReal_mul, ENNReal.toReal_pow]
  have : c.toReal = 1 := by nlinarith
  grind [ENNReal.ofReal_toReal, ENNReal.ofReal_one]

(no claims that these are very good general grind annotations)

[Michael Rothgang]

Can finiteness do the first three haves?

[Michael Rothgang]

Harry Goldstein said:

so we can solve the goal with nlinarith (which does just solve the goal immediately on Reals.

That was my question, thank you. So the issue is really about converting to Reals.

[Michael Rothgang]

David Ledvinka said:

I have plans to work on automating the conversion of ENNReals to NNReals or Reals but it doesn't exist yet.

I look forward to learning more about these (and am happy to meet and exchange ideas; I have also been thinking about this)!

[Violeta Hernández]

Do we have the lemma x : ENNReal → x ≠ ⊤ → ∃ y : ℝ, 0 ≤ y ∧ x = y? If your goal is to avoid extended reals, obtain on that will help

[Harry Goldstein]

I think the problem is that all of my assumptions are also about ENNReals. If I just had c, I could work with that. But all of my hypotheses also need to be converted to be about Reals.

[Willem vanhulle]

I have made a tactic for normalizing ENNReals some months ago https://github.com/wvhulle/ennreal-arith

Harry Goldstein said:

I think the problem is that all of my assumptions are also about ENNReals. If I just had c, I could work with that. But all of my hypotheses also need to be converted to be about Reals.

[Heather Macbeth]

Harry Goldstein said:

I can't get away from ENNReals completely (since the use-site talks about ENNReals). So I think the real issue here is automating the conversion of a bunch of assumptions about ENNReals to assumptions about Reals so we can solve the goal with nlinarith (which does just solve the goal immediately on Reals.

As @David Ledvinka pointed out, now that his PR #35155 is merged you only need to convert ENNReal-to-NNReal, not ENNReal-to-Real.