Zulip Chat Archive

Stream: general

Topic: I love library_search


Kevin Buzzard (Jul 21 2019 at 00:26):

I'm learning a new area and library_search has really helped me to get going much more quickly than usual. Thanks @Scott Morrison .

Is this supposed to happen:

import data.equiv.basic

example (α β : Type) (e : equiv α β) : e.inv_fun ∘ e.to_fun = id := by library_search
-- excessive memory consumption

? Whenever I see a thing like this I figure that it'll be somewhere in mathlib so just search for it.

Kevin Buzzard (Jul 21 2019 at 00:27):

Aah :-) Lean restart fixed it :-)

Scott Morrison (Jul 21 2019 at 08:07):

You're welcome! A student here is writing a related tool list_applies, which hopefully will list all (or at list a few) lemmas that can be applied at the current moment.

Johan Commelin (Aug 01 2019 at 09:14):

library_search just spit out exact buffer.lt_aux_2 hs. @Scott Morrison Is that intended behaviour? (It is a valid proof...)

Johan Commelin (Aug 01 2019 at 09:18):

Ok, maybe that lemma is just in the wrong file, etc...

Johan Commelin (Aug 01 2019 at 09:20):

There is also nat.sub_lt and the identical nat.sub_lt_self. I understand that library_search didn't find those...

Kevin Buzzard (Aug 01 2019 at 09:55):

What was the question?

Johan Commelin (Aug 01 2019 at 11:07):

That buffer.aux_blah is quite a funny name for this lemma. Not really a question, I agree.

Scott Morrison (Aug 01 2019 at 11:22):

library_search filters imported lemmas according to their head symbol, sorts them the length of their name, and tells you the first thing that works! It's not trying to be very clever.

Kevin Buzzard (Aug 01 2019 at 11:51):

I meant: what was the question you asked library_search?

Johan Commelin (Aug 01 2019 at 13:09):

The question was to prove n - 1 < n, where n : nat

Kevin Buzzard (Aug 01 2019 at 13:49):

That's not true!

Kevin Buzzard (Aug 01 2019 at 13:49):

aah, maybe hs is the assumption that n isn't 0 somehow...

Johan Commelin (Aug 01 2019 at 13:57):

Aah, sorry, forgot to include the assumption.

Kevin Buzzard (Aug 01 2019 at 13:58):

librarysearch finds different things depending on whether you have n > 0 or n ne 0

Kevin Buzzard (Aug 01 2019 at 13:58):

(unsurprisingly)

Kevin Buzzard (Aug 01 2019 at 15:34):

example (n i : ) (h : i + 1 < n) : n - 2 - i < n := by library_search
-- exact buffer.lt_aux_3 h

What can you do? It's the right answer :-)

Kevin Buzzard (Aug 01 2019 at 15:35):

And the definitions are in core :-)

Johan Commelin (Aug 01 2019 at 16:43):

Yeah, I guess so...

Johan Commelin (Aug 01 2019 at 16:43):

It's just... a bit disappointing from an aesthetic point of view?

Johan Commelin (Aug 01 2019 at 16:44):

Also, I would have never found this name without library_search. So... @Scott Morrison thanks a lot! It really helps with finding things I wouldn't find manually!

Kevin Buzzard (Aug 01 2019 at 17:06):

I'm idly trying to do one of this year's IMO problems in Lean whilst in a meeting and library_search has been essential!

Johan Commelin (Aug 01 2019 at 17:07):

Is the problem that easy?

Kevin Buzzard (Aug 01 2019 at 17:45):

I just finished it! I used library_search four times :-)

Kevin Buzzard (Aug 01 2019 at 17:46):

import tactic.ring

theorem imo2019Q1 (f :   ) :
( a b : , f (2 * a) + 2 * (f b) = f (f (a + b))) 
( x, f x = 0)   c,  x, f x = 2 * x + c :=
begin
  split, swap,
  { -- easy way
    intro h,
    cases h,
      intros a b,
      rw [h (2 * a), h b, h (f (a + b))],
      simp,
    intros a b,
    cases h with c h,
    repeat {rw h},
    ring,
  },
  intro h,
  have h0 : f 0 + 2 * f 0 = f(-2) + 2 * f 1,
    convert h 0 0,
    convert h (-1) 1,
  have h1 :  b, f 0 + 2 * f b = f (f b),
    intro b, convert h 0 b, simp,
  have h2 :  b, f (-2) + 2 * f (b + 1) = f (f b),
    intro b, convert h (-1) (b+1); simp,
  have h3 :  m,  b, f (b + 1) - f b = m,
    use f 1 - f 0,
    intro b,
    apply (domain.mul_left_inj (show (2 : )  0, from dec_trivial)).1,
    rw mul_sub,
    have h4 : 2 * f (b + 1) = f (f b) - f (-2),
      rw [h2 b], simp,
    have h5 : 2 * f b = f (f b) - f 0,
      rw [h1 b], simp,
    rw [h4, h5],
    rw eq_sub_of_add_eq h0.symm,
    ring,
  cases h3 with m h3,
  have h4 :  b, f b = m * b + f 0,
    intro b,
    apply int.induction_on' b 0, simp,
    { intros k hk hf,
      rw [eq_add_of_sub_eq (h3 k), hf],
      ring
    },
    { intros k hk hf,
      have h4 := h3 (k - 1),
      replace h4 := eq_add_of_sub_eq h4,
      rw add_comm m at h4,
      replace h4 := eq_sub_of_add_eq h4.symm,
      rw h4,
      rw add_comm at hf,
      rw eq_sub_of_add_eq hf.symm,
      rw sub_add_cancel,
      ring,
    },
  conv at h in (f (2 * _) + 2 * f _ = f (f (_))) begin
    rw h4 (2 * a),
    rw h4 b,
    rw h4 (a + b),
    rw h4 (m * (a + b) + f 0),
  end,
  have h5 : 2 * f 0 = m * f 0,
    simpa using h 0 0,
  by_cases h6 : f 0 = 0, swap,
    have h7 := (domain.mul_right_inj h6).1 h5,
    right,
    use (f 0),
    intro x,
    convert h4 x,
  rw h6 at h,
  by_cases h7 : m = 0,
    left,
    intro x,
    convert h4 x,
    rw [h6, h7],
    simp,
  have h8 : 2 * m = m * m,
    simpa using h 0 1,
  replace h8 := (domain.mul_right_inj h7).1 h8,
  right,
  use (f 0),
  intro x,
  convert h4 x,
end

Kevin Buzzard (Aug 01 2019 at 17:47):

I couldn't find a=b-c -> c=b-a in int (or any add_comm_group) though

Kevin Buzzard (Aug 01 2019 at 17:48):

I had to use eq_add_of_sub_eq, add_comm, eq_sub_of_add_eq

Kevin Buzzard (Aug 01 2019 at 17:50):

I was a bit surprised -- a lot of things I thought "eew, that will be hard in Lean" and then it turned out not to be so hard. Thanks @Paul-Nicolas Madelaine for PR'ing int.induction_on' -- things would have been a lot more awful without it.

Kevin Buzzard (Aug 01 2019 at 17:50):

I have memories of these sorts of questions being hell in Lean but because everything was in int not nat it was really quite straightforward.

Johan Commelin (Aug 01 2019 at 17:51):

Nice!

Kevin Buzzard (Aug 01 2019 at 17:51):

Just looked at the official solution -- I think mine is slightly better ;-) [and not just because it has been formalised!]

Johan Commelin (Aug 01 2019 at 17:52):

Now formalise the statement of the geometry question (-;

Kevin Buzzard (Aug 01 2019 at 17:53):

rofl I never liked the geometry questions :-)

Floris van Doorn (Aug 01 2019 at 17:53):

I've been thinking about formalizing IMO questions. This is really nice!

Kevin Buzzard (Aug 01 2019 at 17:53):

The only difference between the official solution and my solution is that they say "if M(a+b)+K=0 for all a and b then obviously M=K=0" whereas I say "let a=0,b=0 and then let a=0,b=1"

Kevin Buzzard (Aug 01 2019 at 17:53):

I think my proof is better :P

Kevin Buzzard (Aug 01 2019 at 17:57):

@Floris van Doorn I was quite surprised myself it came out so easily. I solved it on paper with not too much trouble 5 minutes before the meeting, and then I started on the formalisation in the meeting but I was expecting it to be troublesome, because formalisation is troublesome. But then it turned out to be quite straightforward. convert was crucial, as was ring, simp,and also that integer induction principle which has only been in mathlib for 3 months. But in a sense this has forced me to re-evaluate a bit how difficult these things are. I "knew" before I started that formalising an IMO problem would be a nightmare, but I kept going on and the things I thought might be hard just kind of turned out to be easy. As I say, I was surprised myself. Without stuff like ring it would have been a nightmare. In particular I think it's a credit to the community that even though core Lean is not moving, mathlib has somehow moved enough to make the paper proof formalisable without too much trouble.

Floris van Doorn (Aug 01 2019 at 18:32):

Yeah, it's nice that these kinds of problems can now be formalized without being a herculean task.

Kevin Buzzard (Aug 01 2019 at 18:41):

Was that true 10 years ago in Coq though?

Reid Barton (Aug 01 2019 at 18:54):

I actually did this too!

import tactic.rcases
import tactic.ring
import tactic.linarith

lemma linear_of_constant_difference (f :   )
  (hf :  a a', f (a + 1) - f a = f (a' + 1) - f a') :
   c d,  x, f x = c * x + d :=
begin
  use [f 1 - f 0, f 0],
  intro x,
  apply int.induction_on' x 0,
  { ring },
  { intros i _ IH,
    calc f (i + 1) = f i + (f (i + 1) - f i) : by ring
    ... = f i + (f 1 - f 0) : by { rw hf i 0, refl }
    ... = _ : by { rw IH, ring } },
  { intros i _ IH,
    calc f (i - 1) = f i - (f ((i - 1) + 1) - f (i - 1)) : by simp
    ... = f i - (f 1 - f 0) : by { rw hf (i - 1) 0, refl }
    ... = _ : by { rw IH, ring } }
end

section

parameters (f :   ) (hf :  a b, f (2 * a) + 2 * f b = f (f (a + b)))
include hf

theorem only_solutions : ( x, f x = 0)  ( d,  x, f x = 2 * x + d) :=
begin
  have :  a b, 2 * (f (b + 1) - f b) = f (2 * (a + 1)) - f (2 * a),
  { intros a b,
    have := calc
      f (2 * a) + 2 * f (b + 1)
        = f (f (a + b + 1)) : by { rw hf, simp }
    ... = f (2 * (a + 1)) + 2 * f b : by { rw hf, simp },
    rw sub_eq_zero at  this,
    convert this using 1,
    ring },
  rcases linear_of_constant_difference f _ with c, d, lf, swap,
  { intros a a',
    apply eq_of_mul_eq_mul_left (show (2 : )  0, by norm_num),
    rw [this 0, this 0] },
  have hf₀ := hf 0 0,
  have hf₁ := hf 1 0,
  simp [lf, mul_add] at hf₀ hf₁,
  have : c * c = c * 2, by linarith [hf₀, hf₁],
  rw [sub_eq_zero, mul_sub] at this,
  rcases mul_eq_zero.mp this with hc|hc,
  { subst c,
    rw [zero_mul, mul_eq_zero] at hf₀,
    rcases hf₀ with hd|hd,
    { norm_num at hd },
    { subst d,
      left,
      intro x,
      convert lf x,
      simp } },
  { rw sub_eq_zero at hc,
    subst c,
    right,
    use d,
    intro x,
    exact lf x }
end

end

theorem imo2019_1 (f :   ) :
  ( a b, f (2 * a) + 2 * f b = f (f (a + b))) 
  ((( x, f x = 0)  ( d,  x, f x = 2 * x + d))) :=
begin
  split,
  { exact λ h, only_solutions f h },
  { rintros (hf|⟨d,hf) a b; simp [hf]; ring }
end

Kevin Buzzard (Aug 01 2019 at 19:00):

Oh nice!

Kevin Buzzard (Aug 01 2019 at 19:00):

Maybe we should start a little project to pick off some other easy ones :-)

Kevin Buzzard (Aug 01 2019 at 19:04):

How are you doing with the geometry ones? :-)

Floris van Doorn (Aug 01 2019 at 19:05):

I'm working on IMO2019-4...

Reid Barton (Aug 01 2019 at 19:06):

I don't really know what to do with any of the geometry ones. Even some of the problems involving games or other random combinatorics seem pretty tricky to formalize.

Reid Barton (Aug 01 2019 at 19:07):

As you might guess from my other recent messages I started on problem 4 too but didn't get much further than proving that 2^36 < 15!

Floris van Doorn (Aug 01 2019 at 19:11):

For geometry we would have to define some basic planar geometry definitions. I don't know whether it is nicer to do analytically or synthetically (my guess would be analytically).

Floris van Doorn (Aug 01 2019 at 19:13):

For combinatorics it depends a lot on the problem. I think IMO2019-3 is not too hard to formulate as a finite sequence of graphs (it will not be pretty, though)

Kevin Buzzard (Aug 01 2019 at 19:38):

IMO2019-3 is just dec_trivial.


Last updated: Dec 20 2023 at 11:08 UTC