Zulip Chat Archive

Stream: new members

Topic: Solving simple (in)equalities gets frustrating


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 14:44):

#mwe ? ;-)

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Marc Masdeu (Dec 17 2020 at 14:47):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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" ?

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 14:59):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:06):

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

view this post on Zulip Marc Masdeu (Dec 17 2020 at 15:06):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Marc Masdeu (Dec 17 2020 at 15:08):

One and a half more to go ;-).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:13):

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

view this post on Zulip 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"...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 17 2020 at 15:18):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 17 2020 at 15:22):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:24):

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

view this post on Zulip 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!)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 17 2020 at 15:34):

Opportunistic automation.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 17 2020 at 15:37):

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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:37):

but it doesn't seem to deal with denominators.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:39):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:40):

and also look in the local context?

view this post on Zulip Mario Carneiro (Dec 17 2020 at 15:41):

and assumption at every stage

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:41):

got it

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 17 2020 at 15:44):

Kevin's suggestion looks like a tactic though

view this post on Zulip 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?

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:47):

thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:52):

How can I tell apply_rules to try norm_num?

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:53):

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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 15:57):

and also a - 1? :-/

view this post on Zulip Adam Topaz (Dec 17 2020 at 15:57):

?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 17 2020 at 15:58):

Oh yeah sure :)

view this post on Zulip 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

view this post on Zulip 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

:-(

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 16:00):

aah, it's the trailing ,

view this post on Zulip Johan Commelin (Dec 17 2020 at 16:05):

nice!

view this post on Zulip Johan Commelin (Dec 17 2020 at 16:05):

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

view this post on Zulip Johan Commelin (Dec 17 2020 at 16:06):

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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 16:10):

lol there's already a field tactic!

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 16:11):

Not sure it's the same fields though

view this post on Zulip Rob Lewis (Dec 17 2020 at 16:16):

Kevin Buzzard said:

lol there's already a field tactic!

It's completely undocumented :sad:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 16:17):

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

view this post on Zulip Kevin Buzzard (Dec 17 2020 at 16:18):

oh forget that, I think field_simp is fine

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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....

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip Sebastien Gouezel (Dec 17 2020 at 20:40):

It will just be by { field_simp, ring }.

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Dec 17 2020 at 20:52):

Sure.

view this post on Zulip Heather Macbeth (Dec 17 2020 at 20:52):

OK, great!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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