Solving simple (in)equalities gets frustrating

Stream: new members

[Marc Masdeu]

Hi,

I am working on a proof of Euler summation, which is now complete up to general facts on definite integrals (essentially, FTC2 as called in here, just for continuous functions). There has been lots of frustration when doing apparently simple manipulations, and my feeling is that someone good at tactic writing should look at how to improve the situation. Here are three examples that have I have taken from calc proofs and that I thought would require one or two lines only. Each has taken me quite a bit of both lines and time. Of course I could golf the proof of each of them, but that wouldn't reduce the time. The first involves simple manipulations with the reals, but ring/field_simp combinations didn't do the trick at all. The other two are inequalities that should be very easy (especially the last one) but took a bit too much. Any comments are welcome.

import data.real.basic
import analysis.special_functions.trigonometric
open real


lemma original_difficult_inequality (n : ℕ) (x : ℝ) :
  -(x ^ 2 *
         (cos x ^ (2 * n + 2) -
            ↑(2 * n + 1) * (1 - cos x ^ 2) * cos x ^ (2 * n))) =
    ↑(2 * n + 1) * (x ^ 2 * cos x ^ (2 * n)) -
      ↑(2 * (n + 1)) * (x ^ 2 * cos x ^ (2 * (n + 1))) :=
begin
  sorry,
end

lemma difficult_equality {x c : ℝ} {n : ℕ} :
  -(x ^ 2 *
         (c^(2 * n + 2) -
            ((2 * n + 1)) * (1 - c^2) * c^(2 * n))) =
    ((2 * n + 1)) * (x^2 * c^(2 * n)) -
      ((2 * (n + 1))) * (x^2 * c^ (2 * (n + 1))) :=
begin
    sorry
end

lemma annoying_inequality (A B x : ℝ) (n : ℕ) (hx : x ≠ 0)
  (quo_pos : 0 < 2 * B / A)
  (h : 2 * B / A ≤ x^2 / (4 * (n + 1))) :
  -(x^2 / (4 * (n + 1))) ≤
    2 * x^3 * 2 / (24 * x) - 2 * B / A - x^2 / 6 :=
begin
    sorry
end

lemma simple_inequality (x y : ℝ) (n : ℕ)
  (h1 : 0 < 2 * x)
  (h2 : x ≤ y^2 / (8 * (↑n + 1))) :
  2 * x ≤ y^2 / (4 * (↑n + 1)) :=
begin
    sorry
end

[Kevin Buzzard]

#mwe ? ;-)

[Kevin Buzzard]

lemma difficult_equality {x c : ℝ} {n : ℕ} :
  -(x ^ 2 *
         (c^(2 * n + 2) -
            ((2 * n + 1)) * (1 - c^2) * c^(2 * n))) =
    ((2 * n + 1)) * (x^2 * c^(2 * n)) -
      ((2 * (n + 1))) * (x^2 * c^ (2 * (n + 1))) :=
begin
  ring_exp,
end

[Marc Masdeu]

Kevin Buzzard said:

#mwe ? ;-)

I copy/pasted for a file I had made to prepare this question, and forgot the two first lines! I fixed it now...

[Marc Masdeu]

Oh! ring_exp! Just learned a new tactic...

[Marc Masdeu]

Kevin Buzzard said:

begin
  ring_exp,
end

I've updated the original question with a original_difficult_equality challenge, which was what I encountered originally. Of course, once you have difficult_equality then you can solve the origional one with exact_mod_cast @difficult_equality x (cos x) n. But is there an easier tactic way for this? You just need to use that cos x is real...

[Kevin Buzzard]

lemma simple_inequality (x y : ℝ) (n : ℕ)
  (h1 : 0 < 2 * x)
  (h2 : x ≤ y^2 / (8 * (↑n + 1))) :
  2 * x ≤ y^2 / (4 * (↑n + 1)) :=
begin
  convert mul_le_mul_of_nonneg_left h2
    (show (0 : ℝ) ≤ 2, by norm_num),
  have := nat.succ_ne_zero n,
  rw [mul_div_assoc', div_eq_div_iff],
  { ring },
  { exact mul_ne_zero (by norm_num) (by assumption_mod_cast) },
  { exact mul_ne_zero (by norm_num) (by assumption_mod_cast) },
end

[Marc Masdeu]

@Kevin Buzzard Are you implying that I should consider this an admissible proof for an argument that is just "divide both sides by 2" ?

[Kevin Buzzard]

(I would be surprised if analysis.special_functions.trigonometric didn't import data.real.basic ;-) )

[Kevin Buzzard]

yeah I'm sure we can do better with that one. What's the lemma? a/(2*b)=2*a/b right? I totally agree.

[Kevin Buzzard]

It's a <= b / (d * c) -> d * a <= b / c or something. I bet that's not in there. But a <= x/d -> d * a <= x will be. Division is hard, you have to prove you're not dividing by zero. You omitted that part in your argument. What I'm saying is that in your _statement_ there is already some mathematics, namely the implicit assertion that what you write makes sense. As a mathematician you forget that this is part of the argument.

[Kevin Buzzard]

"Just dividing both sides by 2" is under half of the proof. The rest is making sure that what you write has mathematical meaning.

[Rob Lewis]

lemma simple_inequality (x y : ℝ) (n : ℕ)
  (h1 : 0 < 2 * x)
  (h2 : x ≤ y^2 / (8 * (↑n + 1))) :
  2 * x ≤ y^2 / (4 * (↑n + 1)) :=
begin
  rw le_div_iff,
  rw le_div_iff at h2,
  {linarith},
  all_goals {norm_cast, linarith}
end

[Kevin Buzzard]

begin
  rw le_div_iff at ⊢ h2,
  {linarith},
  all_goals {norm_cast, linarith}
end

[Marc Masdeu]

I like these a bit better @Rob Lewis and @Kevin Buzzard ...

[Kevin Buzzard]

le_div_iff gives a <= x/d -> a * d <= x which is what I should have used in the first place.

[Marc Masdeu]

Yes, I was now trying to add 0 < 2 to the list of assumptions and see if Lean could figure out the proof by itself.

[Marc Masdeu]

One and a half more to go ;-).

[Johan Commelin]

it would be great if we could have some sort of tidy_ineq_basher that would "try the obvious things" and call norm_num and linarith when needed. And then spit out a proof-script that is reasonably fast.

[Kevin Buzzard]

lemma original_difficult_inequality (n : ℕ) (x : ℝ) :
  -(x ^ 2 *
         (cos x ^ (2 * n + 2) -
            ↑(2 * n + 1) * (1 - cos x ^ 2) * cos x ^ (2 * n))) =
    ↑(2 * n + 1) * (x ^ 2 * cos x ^ (2 * n)) -
      ↑(2 * (n + 1)) * (x ^ 2 * cos x ^ (2 * (n + 1))) :=
begin
  generalize : cos x = c,
  simp,
  ring_exp,
end

[Kevin Buzzard]

Is annoying_inequality true? What's the maths proof? Oh, I missed the x on the denominator, I thought we had an x^3 not cancelling with an x^2

[Marc Masdeu]

Two new tactics today, I didn't know about generalize either, it looks like it's really handy to remove clutter...

[Marc Masdeu]

Johan Commelin said:

it would be great if we could have some sort of tidy_ineq_basher that would "try the obvious things" and call norm_num and linarith when needed. And then spit out a proof-script that is reasonably fast.

I was thinking about this... also for field_simp it would be useful that it gave you feedback on which things it tried to invert but failed because it didn't know they were nonzero. You could then try to add those manually.

[Kevin Buzzard]

field_simp does give you that feedback -- just look at the denominators it leaves behind.

[Marc Masdeu]

Well, it doesn't try very hard at those. You'd expect that it'd know that (2:\R) was nonzero. But fine, I know that "this is not the job of field_simp"...

[Kevin Buzzard]

lemma annoying_inequality (A B x : ℝ) (n : ℕ) (hx : x ≠ 0)
  (quo_pos : 0 < 2 * B / A)
  (h : 2 * B / A ≤ x^2 / (4 * (n + 1))) :
  -(x^2 / (4 * (n + 1))) ≤
    2 * x^3 * 2 / (24 * x) - 2 * B / A - x^2 / 6 :=
begin
  have h24 : (24 : ℝ) ≠ 0 := by norm_num,
  have : 2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6,
    field_simp [hx, h24], ring,
  linarith,
end

[Kevin Buzzard]

Of course some part of Lean's system can prove easily that 2 isn't 0. But not all parts of Lean's system talk to all other parts at all times, because this would just cause chaos. You are falling into a trap which I used to fall into a lot -- "it's obvious, so why doesn't Lean do it automatically?". Making Lean do all obvious things automatically would just make it stop working, because there are 10000 things which are obvious to you as a professional number theorist.

[Johan Commelin]

It's not the job of field_simp, but that doesn't mean that there can't be another tactic that does this for us.

[Johan Commelin]

It just means that we need higher-level "conductor" tactics, that direct the lower-level ones

[Johan Commelin]

Those "conductor" tactics will probably be slow. So they should have a ? option to print the proof-script they found in lower-level tactics.

[Johan Commelin]

Like Mario says about metamath: you don't want omega in your proof. You should run it once, and store the output.

[Johan Commelin]

Unfortunately, I have no idea how to write these conductor-tactics. But I think they will be a huge win for these kinds of computations.

[Marc Masdeu]

Kevin, I understand your point, I had read it from you somewhere else. But as Johan says, there should be higher-level tactics that do this. The examples I gave you showed up as simple calc steps, I already broke it up in simple bits. But these ones caused a lot of pain.

[Kevin Buzzard]

@Marc Masdeu if you want to learn how to write a tactic, then you could write field_simp2 which was field_simp but in addition looked through the local context to find any hypotheses of the form x ≠ 0 and added them to some list, and also looked through all denominators which were nonzero numerals and added them automatically to the list, and then applied field_simp with that list. And then the moment you did this you'd have someone complainining that they have a hypothesis A != B and your stupid tactic didn't know that A - B was non-zero. So then you fix this and you have someone else complaining that your stupid tactic doesn't know that x^2+37 != 0 where x is a rational. Can't you see? It never ends! If you learn how to write tactics you can write your own tactics which are minor extensions of the basic ones, and these minor extensions are not hard to write.

[Marc Masdeu]

Johan Commelin said:

Unfortunately, I have no idea how to write these conductor-tactics. But I think they will be a huge win for these kinds of computations.

My feeling is that this would allow more people to jump in and proving things. I have 900-line proof of this very simple result (Euler summation). On a pdf it takes 3 pages, which could easily be condensed to one or two. I tell this to my colleagues and they laugh at it...

[Kevin Buzzard]

But this is the second time in the last few days that numerals being non-zero not being known by field_simp has come up and it would not be hard to fix.

[Johan Commelin]

@Kevin Buzzard "it never ends" but we should do it anyway

[Kevin Buzzard]

Take the LaTeX file and compare it to the size of the Lean file. What's the ratio?

[Johan Commelin]

@Mario Carneiro is this something for norm_num plugins? Or should it rather be a new higher-level tactic?

[Johan Commelin]

Kevin Buzzard said:

Take the LaTeX file and compare it to the size of the Lean file. What's the ratio?

After gziping right?

[Marc Masdeu]

Kevin Buzzard said:

Take the LaTeX file and compare it to the size of the Lean file. What's the ratio?

It's not the size, but how long it takes to type up what matters. And I better not tell you how long it has taken me to type the proof up...

[Kevin Buzzard]

Usually these things are around 4. But also remember that you are an expert in writing pdfs and a relative newcomer for writing Lean proofs.

[Kevin Buzzard]

Writing Lean proofs like this is a really good way to learn though.

[Kevin Buzzard]

(relative newcomer in the sense that you've been doing maths in LaTeX for a lot longer!)

[Marc Masdeu]

Kevin Buzzard said:

(relative newcomer in the sense that you've been doing maths in LaTeX for a lot longer!)

Don't worry, I wouldn't take offense :laughing:

[Kevin Buzzard]

@Marc Masdeu we should think more carefully about how to make field_simp better because I absolutely do agree that you have a point.

[Kevin Buzzard]

I mostly agree this because it's the second time it has come up in the last week.

[Kevin Buzzard]

  have h24 : (24 : ℝ) ≠ 0 := by norm_num,
  have : 2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6,
    field_simp [hx, h24], ring,

takes four tactics to solve

[Marc Masdeu]

And I'd like to learn how to write tactics. I hoped that by giving some challenges the tactic-writers would take the hint...

[Kevin Buzzard]

It's difficult for me to know how hard these are in practice because I am not a tactic-writer. In the first part of one of my whingey messages above I was saying that all you have to do in this case is to look for (a) things of the form "x \ne 0" in the local context, and (b) nonzero numerals in the local context, but maybe it's even easier.

[Marc Masdeu]

Kevin Buzzard said:

I mostly agree this because it's the second time it has come up in the last week.

@Kevin Buzzard make sure that it wasn't a close relative of mine who came up with the problem...

[Kevin Buzzard]

One could envisage a general "prove that this is non-zero" tactic, which given a hypothesis hx : x != 0 manages to prove automatically that 24*x != 0 and, because this is a denominator in the goal, feeds this into field_simp which makes field_simp work better.

[Johan Commelin]

I guess that one could try to write a tactic that decides formulas in the language of real closed fields... but this sounds like quite a big effort. And it will be slow if it isn't written by an expert. Also, it might not give short witnesses that can replace the tactic call.

[Alex J. Best]

Marc Masdeu said:

And I'd like to learn how to write tactics. I hoped that by giving some challenges the tactic-writers would take the hint...

You should make an issue on mathlib's github page (tagged with meta, and easy / medium or something) then so the hint isan't lost to time!

[Marc Masdeu]

I'll look at the tactics videos that are around and see if I can make sense of it...

[Johan Commelin]

@Kevin Buzzard We should probably have a IMOkid tactic that just knows all the standard IMO tricks for solving inequalities.
That tactic doesn't need to be able to tackle every IMO inequality ever. If it tackles 70% that will already be very helpful.

[Johan Commelin]

Opportunistic automation.

[Kevin Buzzard]

I see. I think I am proposing a clear_denom tactic, which acts on goals of the form a / b = c / d or a / b = c and tries to reduce them to the form a * d = b * c or a * c = b, closing the auxiliary goals which show up (denominators != 0) by applying a simple show_nonzero tactic which looks through the local context, applies things like mul_nonzero and that numerals other than zero are non-zero. And then there's a natural field tactic, which applies field_simp and then clear_denom and then ring. @Rob Lewis @Mario Carneiro is this as simple as it looks or am I missing something? Of course it won't work in every case but it might be a step in the right direction for people like Marc.

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro is this something for norm_num plugins? Or should it rather be a new higher-level tactic?

Is what? I see a lot of things in this thread, but not much that is actionable as a tactic-writer. What's the tactic supposed to do?

[Kevin Buzzard]

We already have nlinarith which is surprisingly good! Rob was just "well I'll assume squares are non-negative and that's it" and I'm thinking "that won't buy us much" but actually it bought us lots!

[Kevin Buzzard]

show_nonzero is an opportunistic attempt to show things are non-zero by checking they're a product of things known to be nonzero. clear_denom clears denominators using show_nonzero.

[Mario Carneiro]

@Kevin Buzzard My understanding was that this is what field_simp is supposed to do

[Kevin Buzzard]

but it doesn't seem to deal with denominators.

[Johan Commelin]

it deals with them, if you pass proofs that things are nonzero.
Kevin wants a tactic that is like field_simp, but proves by itself that denoms are nonzero.

[Kevin Buzzard]

In the docstring it says "If the goal is an equality, this simpset will also clear the denominators" but it won't deal with 24*x if x != 0 is in the local context, because it doesn't know 24 != 0 and it's irritating to have to tell it this -- ring doesn't need to be told it.

[Kevin Buzzard]

example (x : ℝ) : 2 * x ^ 2 * 2 / 24 = x ^ 2 / 6 := by ring -- works

[Kevin Buzzard]

example (x : ℝ) : 2 * x ^ 2 * 2 / 24 = x ^ 2 / 6 :=
begin
  field_simp, -- simplify tactic failed to simplify
end

[Johan Commelin]

Mario Carneiro said:

Is what? I see a lot of things in this thread, but not much that is actionable as a tactic-writer. What's the tactic supposed to do?

we just want a tactic that takes the goals that Marc posted above, and outputs the proof scripts that Kevin wrote himself (also posted above)

[Mario Carneiro]

Okay so show_nonzero is something like apply_rules with:

• a != 0 -> b != 0 -> a * b != 0
• n != 0 for n a numeral -> call norm_num
• \u a != 0 -> call norm_cast

[Kevin Buzzard]

and also look in the local context?

[Mario Carneiro]

and assumption at every stage

[Kevin Buzzard]

got it

[Mario Carneiro]

Johan Commelin said:

Mario Carneiro said:

Is what? I see a lot of things in this thread, but not much that is actionable as a tactic-writer. What's the tactic supposed to do?

we just want a tactic that takes the goals that Marc posted above, and outputs the proof scripts that Kevin wrote himself (also posted above)

I suspected you would say that. That's not what I would call actionable, because I'm not clever enough to invent an algorithm that will solve arbitrarily complicated combinations of things

[Mario Carneiro]

Kevin's suggestion looks like a tactic though

[Kevin Buzzard]

Can someone remind me how to write a tactic which just runs a tactic script? For example if I want to write a tactic which does rw add_comm, simp, ring, how do I make that into one tactic?

[Shing Tak Lam]

Kevin Buzzard said:

Can someone remind me how to write a tactic which just runs a tactic script? For example if I want to write a tactic which does rw add_comm, simp, ring, how do I make that into one tactic?

import tactic

meta def foo := `[rw add_comm, simp, ring]

[Kevin Buzzard]

There is some ludicrously simple way to do this involving some number of backticks but I can never remember where it is and my

[Kevin Buzzard]

thanks

[Kevin Buzzard]

...my last attempt to get an example such as this into extras/tactic_writing.html failed for some reason I can't remember

[Rob Lewis]

Johan Commelin said:

I guess that one could try to write a tactic that decides formulas in the language of real closed fields... but this sounds like quite a big effort. And it will be slow if it isn't written by an expert. Also, it might not give short witnesses that can replace the tactic call.

This is certainly a big effort, will probably be slow even if written by an expert, and I'm not aware of a good certificate format. https://www.cl.cam.ac.uk/~jrh13/papers/cade05.pdf

[Rob Lewis]

Kevin Buzzard said:

...my last attempt to get an example such as this into extras/tactic_writing.html failed for some reason I can't remember

https://leanprover-community.github.io/extras/tactic_writing.html#marios-backtick-cheat-sheet last bullet point?

[Kevin Buzzard]

How can I tell apply_rules to try norm_num?

[Kevin Buzzard]

https://leanprover-community.github.io/extras/tactic_writing.html#marios-backtick-cheat-sheet last bullet point?

I would have noticed it if there had been an example, I suspect. Maybe I should write one!

[Kevin Buzzard]

Kevin Buzzard said:

How can I tell apply_rules to try norm_num?

hmm, maybe I should just do it afterwards.

[Adam Topaz]

i would be very happy if field_simp could solve things like this:

example {K : Type*} [field K] {a b c : K} {h : a ≠ 1} : (1 - a) * (1-a)⁻¹ * b = b :=
begin
  field_simp [h],
end

[Kevin Buzzard]

and also a - 1? :-/

[Adam Topaz]

?

[Kevin Buzzard]

If h : A != B then you want to know both that A - B != 0 and that B - A != 0

[Adam Topaz]

Oh yeah sure :)

[Kevin Buzzard]

and tomorrow you'll want to know that if A < B then also A - B != 0 and B - A != 0

[Kevin Buzzard]

import tactic
import data.real.basic

example (x : ℝ) (hx : x ≠ 0) :
  2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6 :=
begin
  try {rw div_eq_div_iff},
  try {rw eq_div_iff},
  try { ring },
  apply_rules [mul_ne_zero],
  all_goals {try {norm_num}},
end -- works

meta def clear_denoms := `[
  try {rw div_eq_div_iff},
  try {rw eq_div_iff},
  try { ring },
  apply_rules [mul_ne_zero],
  all_goals {try {norm_num}},
] -- incomprehensible error

:-(

[Kevin Buzzard]

aah, it's the trailing ,

[Johan Commelin]

nice!

[Johan Commelin]

this should probably be plugged into the generic machinery that Scott wrote for tidy

[Johan Commelin]

Like, tidy is implemented using tactic.chain, and maybe this should also use that.

[Kevin Buzzard]

lol there's already a field tactic!

[Kevin Buzzard]

Not sure it's the same fields though

[Rob Lewis]

Kevin Buzzard said:

lol there's already a field tactic!

It's completely undocumented :sad:

[Rob Lewis]

From the tests:

def my_semigroup := semigroup

example {α} (mul : α → α → α) (h : false) : my_semigroup α :=
begin
  refine_struct { mul := mul, .. },
  field mul_assoc {
    guard_target ∀ a b c : α, mul (mul a b) c = mul a (mul b c),
    exact h.elim }
end

[Rob Lewis]

But it has no doc of its own and it's not mentioned in the docs for refine_struct

[Kevin Buzzard]

Do we have a tactic which turns a/b*c*d/e*f into X/Y?

[Kevin Buzzard]

oh forget that, I think field_simp is fine

[Kevin Buzzard]

import tactic
import data.real.basic

namespace tactic.interactive

meta def show_nonzero := `[
  apply_rules [
    mul_ne_zero,
    sub_ne_zero.2,
    ne.symm,
    ne_of_gt,
    ne_of_lt
    ],
  all_goals {try {norm_num}}
]

meta def clear_denoms := `[
  try {rw div_eq_div_iff},
  try {rw eq_div_iff},
  try {symmetry, rw eq_div_iff},
  try { ring_exp },
  all_goals {show_nonzero}
]

meta def discrete_field := `[
  try {field_simp},
  try {clear_denoms},
  try {ring_exp}
]

end tactic.interactive

example (x : ℝ) (hx : x ≠ 0) :
  2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6 :=
begin
  discrete_field
end

example {K : Type*} [field K] {a b c : K} {h : a ≠ 1} : (1 - a) * (1-a)⁻¹ * b = b :=
begin
  rw inv_eq_one_div,
  discrete_field,
end

@Marc Masdeu @Adam Topaz

[Kevin Buzzard]

just ignore the "maximal iterations reached" stuff, I have no idea what that means but the goal gets closed

[Reid Barton]

Not really relevant here, but with only outermost universal quantifiers it should be possible to produce proof certificates based on the Positivstellensatz.

[Reid Barton]

I say it's not relevant because these problems are not really any harder than checking the proof certificates

[Kevin Lacker]

in theory it seems like this should be solvable using brute force, without any mathematical understanding of this specific problem. it takes 4 tactics to solve, lean doesn't have that many tactics....

[Sebastien Gouezel]

I have already said this several times, but I'll say it again and again, hoping it percolates to someone who can implement that. In Isabelle, there is something called simprocs: baby tactics that are applied by simp under the right conditions. Checking that a numeral is nonzero would be a perfect simproc. With this, no need for a new tactic, field_simp would work fine as it is just simp with an additional simpset.

[Frédéric Dupuis]

I think this is one situation where Lean 4's default arguments will turn out to be very useful: we'll be able to put by prove_its_nonzero as the default argument in those division lemmas.

[Rob Lewis]

In this case it could be achieved by using a different discharger in field_simp, right? Not a full simp proc. If field_simp were something like simp only using field_simps {discharger := prove_its_nonzero <|> default_discharger} wouldn't that achieve what you want?

[Mario Carneiro]

simprocs are a rather fundamental change to the way simp works, and so I don't expect it to happen in lean 3. Perhaps we should put that on the todo list for lean 4 simp

[Sebastien Gouezel]

Rob Lewis said:

In this case it could be achieved by using a different discharger in field_simp, right? Not a full simp proc. If field_simp were something like simp only using field_simps {discharger := prove_its_nonzero <|> default_discharger} wouldn't that achieve what you want?

I didn't even know this existed!

example (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) :
  2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6 :=
begin
  field_simp [-mul_eq_zero, mul_ne_zero] {discharger := `[assumption <|> norm_num]},
  ring
end

works fine.

[Heather Macbeth]

I didn't know this existed either! Is there any reason not to rewrite field_simp so that this "discharger" is there by default? I would say that 50% of the time I use field_simp there's a numeric constant around which I need to use norm_num for.

[Sebastien Gouezel]

I'm on it. I need to practice a little bit my tactic fu, but I'll get there :-)

[Heather Macbeth]

Will this make things easier, though? Currently I would solve a goal like this as follows:

example (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) :
  2 * x ^ 3 * 2 / (24 * x) = x ^ 2 / 6 :=
begin
  have h1 : (24:ℝ) ≠ 0 := by norm_num,
  have h2 : (6:ℝ) ≠ 0 := by norm_num,
  field_simp [hx, h1, h2],
  ring
end

and in particular there's no need to remember the names of the lemmas mul_eq_zero and mul_ne_zero; field_simp takes care of this for me. In the new version of the tactic, does one need to mention such lemmas explicitly?

[Sebastien Gouezel]

It will just be by { field_simp, ring }.

[Heather Macbeth]

And will it still be possible to pass extra nonzero-facts as hypotheses? field_simp [ne_of_gt (norm_pos_iff.mpr ha)], etc.

[Sebastien Gouezel]

Sure.

[Heather Macbeth]

OK, great!

[Patrick Massot]

I'm late to the party, but I want to write that I agree with everything Marc wrote. All this is incredibly painful, and the fact that we can golf the proofs is not at all the right measure of performance of Lean+mathlib here. Formalization time is the right one. This is simply yet another proof that we are very very far from having a usable tool.

[Kevin Buzzard]

To add to this data point, I met with Ashvni this morning who is doing some combinatorial stuff related to Bernouilli numbers, and she wanted an identity of products of binomial coefficients which turned into an equality of ratios of factorials which was trivial modulo factorial_ne_zero applied four times. Maybe some ne_zero lemmas could be tagged in some way and fed into this?

[Sebastien Gouezel]

If you have a mwe, I can check if tagging factorial_ne_zero with field_simp is enough here. Or you can try it yourself, with attribute [field_simps] factorial_ne_zero.

[Mario Carneiro]

I don't think norm_num should literally be the discharger. That entry point includes a lot of unnecessary simp. I think the discharger should be custom built to identify numeral != 0 goals and call the internal norm_num function for this directly