## Stream: new members

### Topic: Solving simple (in)equalities gets frustrating

#### Marc Masdeu (Dec 17 2020 at 14:43):

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


#mwe ? ;-)

#### Kevin Buzzard (Dec 17 2020 at 14:45):

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 (Dec 17 2020 at 14:46):

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 (Dec 17 2020 at 14:47):

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

#### Marc Masdeu (Dec 17 2020 at 14:54):

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 (Dec 17 2020 at 14:55):

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 (Dec 17 2020 at 14:59):

@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 (Dec 17 2020 at 14:59):

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

#### Kevin Buzzard (Dec 17 2020 at 15:00):

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 (Dec 17 2020 at 15:03):

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 (Dec 17 2020 at 15:04):

"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 (Dec 17 2020 at 15:04):

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 (Dec 17 2020 at 15:06):

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


#### Marc Masdeu (Dec 17 2020 at 15:06):

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

#### Kevin Buzzard (Dec 17 2020 at 15:07):

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

#### Marc Masdeu (Dec 17 2020 at 15:08):

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 (Dec 17 2020 at 15:08):

One and a half more to go ;-).

#### Johan Commelin (Dec 17 2020 at 15:08):

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 (Dec 17 2020 at 15:08):

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 (Dec 17 2020 at 15:09):

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 (Dec 17 2020 at 15:11):

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

#### Marc Masdeu (Dec 17 2020 at 15:13):

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 (Dec 17 2020 at 15:13):

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

#### Marc Masdeu (Dec 17 2020 at 15:15):

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 (Dec 17 2020 at 15:16):

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 (Dec 17 2020 at 15:17):

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 (Dec 17 2020 at 15:17):

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 (Dec 17 2020 at 15:18):

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

#### Johan Commelin (Dec 17 2020 at 15:18):

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 (Dec 17 2020 at 15:19):

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

#### Johan Commelin (Dec 17 2020 at 15:20):

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 (Dec 17 2020 at 15:20):

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 (Dec 17 2020 at 15:21):

@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 (Dec 17 2020 at 15:21):

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 (Dec 17 2020 at 15:22):

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 (Dec 17 2020 at 15:22):

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

#### Kevin Buzzard (Dec 17 2020 at 15:22):

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

#### Johan Commelin (Dec 17 2020 at 15:23):

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

#### Johan Commelin (Dec 17 2020 at 15:23):

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 (Dec 17 2020 at 15:23):

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 (Dec 17 2020 at 15:23):

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 (Dec 17 2020 at 15:24):

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

#### Kevin Buzzard (Dec 17 2020 at 15:24):

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

#### Marc Masdeu (Dec 17 2020 at 15:25):

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 (Dec 17 2020 at 15:25):

@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 (Dec 17 2020 at 15:26):

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

#### Kevin Buzzard (Dec 17 2020 at 15:26):

  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 (Dec 17 2020 at 15:27):

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 (Dec 17 2020 at 15:28):

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 (Dec 17 2020 at 15:29):

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 (Dec 17 2020 at 15:30):

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 (Dec 17 2020 at 15:32):

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 (Dec 17 2020 at 15:32):

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 (Dec 17 2020 at 15:32):

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

#### Johan Commelin (Dec 17 2020 at 15:34):

@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 (Dec 17 2020 at 15:34):

Opportunistic automation.

#### Kevin Buzzard (Dec 17 2020 at 15:34):

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 (Dec 17 2020 at 15:35):

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 (Dec 17 2020 at 15:35):

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 (Dec 17 2020 at 15:36):

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 (Dec 17 2020 at 15:37):

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

#### Kevin Buzzard (Dec 17 2020 at 15:37):

but it doesn't seem to deal with denominators.

#### Johan Commelin (Dec 17 2020 at 15:38):

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 (Dec 17 2020 at 15:38):

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 (Dec 17 2020 at 15:39):

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


#### Kevin Buzzard (Dec 17 2020 at 15:40):

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


#### Johan Commelin (Dec 17 2020 at 15:40):

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 (Dec 17 2020 at 15:40):

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 (Dec 17 2020 at 15:40):

and also look in the local context?

#### Mario Carneiro (Dec 17 2020 at 15:41):

and assumption at every stage

got it

#### Mario Carneiro (Dec 17 2020 at 15:43):

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 (Dec 17 2020 at 15:44):

Kevin's suggestion looks like a tactic though

#### Kevin Buzzard (Dec 17 2020 at 15:45):

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 (Dec 17 2020 at 15:46):

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 (Dec 17 2020 at 15:46):

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

thanks

#### Kevin Buzzard (Dec 17 2020 at 15:48):

...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 (Dec 17 2020 at 15:48):

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 (Dec 17 2020 at 15:50):

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

#### Kevin Buzzard (Dec 17 2020 at 15:52):

How can I tell apply_rules to try norm_num?

#### Kevin Buzzard (Dec 17 2020 at 15:53):

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

#### Kevin Buzzard (Dec 17 2020 at 15:54):

Kevin Buzzard said:

How can I tell apply_rules to try norm_num?

hmm, maybe I should just do it afterwards.

#### Adam Topaz (Dec 17 2020 at 15:56):

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 (Dec 17 2020 at 15:57):

and also a - 1? :-/

?

#### Kevin Buzzard (Dec 17 2020 at 15:58):

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

Oh yeah sure :)

#### Kevin Buzzard (Dec 17 2020 at 15:58):

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

#### Kevin Buzzard (Dec 17 2020 at 16:00):

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 (Dec 17 2020 at 16:00):

aah, it's the trailing ,

nice!

#### Johan Commelin (Dec 17 2020 at 16:05):

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

#### Johan Commelin (Dec 17 2020 at 16:06):

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

#### Kevin Buzzard (Dec 17 2020 at 16:10):

lol there's already a field tactic!

#### Kevin Buzzard (Dec 17 2020 at 16:11):

Not sure it's the same fields though

#### Rob Lewis (Dec 17 2020 at 16:16):

Kevin Buzzard said:

lol there's already a field tactic!

It's completely undocumented :sad:

#### Rob Lewis (Dec 17 2020 at 16:16):

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 (Dec 17 2020 at 16:16):

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

#### Kevin Buzzard (Dec 17 2020 at 16:17):

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

#### Kevin Buzzard (Dec 17 2020 at 16:18):

oh forget that, I think field_simp is fine

#### Kevin Buzzard (Dec 17 2020 at 16:21):

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 (Dec 17 2020 at 16:22):

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

#### Reid Barton (Dec 17 2020 at 16:39):

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

#### Reid Barton (Dec 17 2020 at 16:39):

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

#### Kevin Lacker (Dec 17 2020 at 17:17):

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 (Dec 17 2020 at 17:51):

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 (Dec 17 2020 at 17:55):

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 (Dec 17 2020 at 17:56):

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 (Dec 17 2020 at 18:21):

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 (Dec 17 2020 at 20:13):

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 (Dec 17 2020 at 20:23):

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 (Dec 17 2020 at 20:28):

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

#### Heather Macbeth (Dec 17 2020 at 20:36):

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 (Dec 17 2020 at 20:40):

It will just be by { field_simp, ring }.

#### Heather Macbeth (Dec 17 2020 at 20:52):

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

Sure.

OK, great!

#### Patrick Massot (Dec 18 2020 at 09:54):

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 (Dec 18 2020 at 11:22):

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 (Dec 18 2020 at 13:28):

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 (Dec 18 2020 at 13:40):

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

Last updated: May 16 2021 at 21:11 UTC