tactic for basic real number game

Stream: mathlib4

[Kevin Buzzard]

In proving that the product of a continuous function by a positive constant is continuous, in an experimental real number game, my summer project student @Ronit Sachdeva is faced with this goal:

import Mathlib

variable (f : ℝ → ℝ) (t c ε y : ℝ) (hc : 0 < c) (hε : 0 < ε)

example (h : |f y - f t| < ε / c) :
    |c * f y - c * f t| < ε := by
  sorry

We do not really want to have to teach the users this sort of nonsense:

  rw [← mul_sub, abs_mul, abs_of_pos hc]
  rwa [lt_div_iff₀ hc, mul_comm] at h

because this involves teaching five "completely obvious to a schoolchild" and thus completely unnecessary lemmas just to finish the job. Is there a tactic which can take it from here because we'd far rather teach that tactic!

This question stems from the philosophy that Heather taught me -- that we should really be pushing to teach tactics in this sort of environment, rather than explicit lemmas (of which there are a gazillion and they're hard to remember and look up within the game framework).

[Kevin Buzzard]

In fact here's an even easier one:

⊢ |-f y + f x| = |f y - f x|

Do we have a tactic that can deal with this? If not, I'm wondering if we should make a bespoke tactic for the game which will just pwn these goals.

[Etienne Marion]

One tactic I don't know, but congr; ring should work.

[Kevin Buzzard]

I am not sure which goal you're talking about but if it's the second one then congr leads to a false goal because abs_sub_comm has not yet been applied.

[Kevin Buzzard]

Is this the sort of goal which a hammer would demolish?

[Etienne Marion]

Yes I was talking about the second. Probably congr 1; ring would work then.

[Kevin Buzzard]

You have to use abs_sub_comm before this is a goal which ring can solve and neither of the tactics you're suggesting will run this

[Etienne Marion]

Oh you're right :man_facepalming: sorry for the noise

[Kevin Buzzard]

Rather annoyingly, the Lean game framework is on Lean v4.21.0 but LeanHammer is on v4.20.0 and I don't know how to make them both work at the same time. I don't know if a hammer is a viable solution for a lean game either (I have no clue how long it takes to run hammer)

[Ruben Van de Velde]

Would be cool if field_simp [hc] at h worked

[Ruben Van de Velde]

And then maybe if grind was taught about abs... There was a comment about that elsewhere on zulip recently

[Kevin Buzzard]

We're going to make a bespoke tactic :-)

theorem abs_lt' (a b : ℝ) : |a| < b ↔ a < b ∧ -a < b := by
  sorry

macro "absarith" : tactic => `(tactic|
  (try repeat rw [abs_lt'] at *;
   try repeat rw [lt_div_iff₀ (by assumption)] at *;
   constructor <;>
   nlinarith (config := {splitHypotheses := true})))

[Kim Morrison]

Lots of good grind goals lurking here. The only thing I've got to work so far is

example (h : |f y - f t| = ε / c) :
    |c * f y - c * f t| = ε := by
  grind [_=_ mul_sub, abs_mul, abs_of_pos]

(Note inequalities replaced by =.) I hope we can improve grind so it can deal with the inequalities here. Both abs_mul and abs_of_pos are probably suitable for @[grind] annotations.

However calling grind with _=_ mul_sub is very hacky and inadvisable (because we are telling grind to start doing ring arithmetic "with its bare hands", rather than via normalization). Unfortunately there's no good way to tell grind's ring module "please, if you see a way to write this as a product, let us know, so we can apply abs_mul.