Tactic for stupid inequality

Stream: Is there code for X?

[Alex Kontorovich]

I don't want the solution to this:

import Mathlib

example (c : ℝ) (hc : c ≠ 0) (cpos : 0 < |c|) (cinvpos : 0 < |c|⁻¹)
    (a : ℝ) (ε : ℝ) (hε : 0 < ε) (h : |a| < ε * |c|⁻¹) : |c| * |a| < ε := by
  --linarith --failed, it's not linear
  --nlinarith --failed
  --simp? [h] -- made no progress
  -- field_simp at h -- does nothing, it's not an equality
  -- bound -- failed
  -- grind -- failed
  -- aesop -- failed
  exact (lt_div_iff₀' cpos).mp h

to be exact (lt_div_iff₀' cpos).mp h. There should be some simple general tactic that can convert h into the goal, and I shouldn't have to quote a theorem like lt_div_iff₀'. Help please? Thank you!

[Kenny Lau]

it would be grw [h]; field_simp after their proposed modification to change < to ≤, but alas the change hasn't happened yet so now you get ε < ε :upside_down:

[Ruben Van de Velde]

I think field_simp at h would ideally solve it. Not sure if that's feasible now with @Heather Macbeth 's rewrite

[Alex Kontorovich]

right now, field_simp at h just changes h to: |a| < ε / |c| :sad:

[Ruben Van de Velde]

Hence "ideally" :)

[Heather Macbeth]

Making field_simp handle inequalities is the next thing on the roadmap, but we didn't do it yet. (The new field_simp implementation is designed to support this.) "Handle inequalities" precisely means that field_simp would perform lt_div_iff₀' (by positivity) (and friends).

[Alex Kontorovich]

Thanks Heather, that's great! If I may ask, hopefully without putting you on the spot too much: what are the chances that it'll get done by next Fri? (Which is when I have in mind to assign a certain problem...) I'm guessing I should change the problem, and circle back around to this one... Actually an awful lot of what I have in mind to cover in the Real Analysis Game will be very much helped by this improved field_simp behavior.... :) Thanks again for your work on it, I really appreciate it!!

[Jireh Loreaux]

You might be able to copy the code from the branch, even if it's not merged by then. But that assumes it's finished by then.

[Alex Kontorovich]

Oh, good point! I can add custom tactics... (Well, I can ask @Jon Eugster very nicely and maybe he'll help :slight_smile: ...) @Heather Macbeth: How hard would it be to just jerry-rig an imperfect field_simp that can handle this inequality, so I don't have to wait for the "official" version to make it into Mathlib...? Thank you!

[Jon Eugster]

I can copy working code from a PR into your game if such a PR works and compiles (and isn't too huge). I can also copy-paste other tactic code into your game and change the syntax slightly, for example some easy changes like "field_simp should always execute field_simp; another_tactic instead".

I haven't looked at the field_simp code but if it requires deeper (new) changes within to make it work for inequalities, it's probably too much effort to do that just for the game.

If you want a "nicer" solution, maybe

import Mathlib

example (c : ℝ) (hc : c ≠ 0) (cpos : 0 < |c|) (cinvpos : 0 < |c|⁻¹)
    (a : ℝ) (ε : ℝ) (hε : 0 < ε) (h : |a| < ε * |c|⁻¹) :
    |c| * |a| < ε := by
  rw [← mul_lt_mul_left cpos] at h
  field_simp at h
  exact h

could be conceptually nicer to do?

[Heather Macbeth]

Alex Kontorovich said:

Thanks Heather, that's great! If I may ask, hopefully without putting you on the spot too much: what are the chances that it'll get done by next Fri?

OK I wrote this :-) #29364

[Heather Macbeth]

I'm not sure whether it handles all the edge cases, and I'm sure mathlib review will improve the code, but this may already be good enough for your purposes. Can you base your game off this mathlib branch?

[Alex Kontorovich]

Oh that's fantastic, thank you!! @Jon Eugster, is it possible to extract from this PR something that I can upload to my game and experiment with it? Thank you!!

[Alex Kontorovich]

Continuing these ideas: Any suggestions for how to get this to work? I'm willing to quote the theorem Nat.le_ceil, but I don't want to quote more than that... Thanks!!

import Mathlib

open Nat

example (ε : ℝ) (hε : 0 < ε) : ∃ N : ℕ, 1 / ε < N := by
  use ⌈1/ε⌉₊ + 1
  have : 1 / ε ≤ ⌈1/ε⌉₊ := by apply le_ceil
/- Goal state is now:
ε : ℝ
hε : 0 < ε
this : 1 / ε ≤ ↑⌈1 / ε⌉₊
⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1)
-/
  norm_cast
/- Did not change
**⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1)**
to
**⊢ 1 / ε < ↑(⌈1 / ε⌉₊) + 1**
and therefore
-/
  linarith -- fails

[Michael Stoll]

Try push_cast in place of norm_cast.

[Michael Stoll]

(push_cast pushes coercions inwards, which is what you want here.)

[Alex Kontorovich]

Thanks, that's what I was missing here...

[Jon Eugster]

Alex Kontorovich said:

Oh that's fantastic, thank you!! Jon Eugster, is it possible to extract from this PR something that I can upload to my game and experiment with it? Thank you!!

https://github.com/AlexKontorovich/RealAnalysisGame/pull/7 should do the trick. I've bumped lean4game to v4.23-rc2 and imported that in your game. I didn't test anything though, didn't even check if CI passes :upside_down:

I guess whenever Heather pushes to her branch, you can run lake update -R mathlib to get that newest version. (At least as long as neither the Lean version nor the Batteries commit used in that branch changes.)

[Alex Kontorovich]

Thank you!! I'll try it out...