I love library_search

Stream: general

[Kevin Buzzard]

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]

Aah :-) Lean restart fixed it :-)

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

What was the question?

[Johan Commelin]

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

[Scott Morrison]

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]

I meant: what was the question you asked library_search?

[Johan Commelin]

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

[Kevin Buzzard]

That's not true!

[Kevin Buzzard]

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

[Johan Commelin]

Aah, sorry, forgot to include the assumption.

[Kevin Buzzard]

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

[Kevin Buzzard]

(unsurprisingly)

[Kevin Buzzard]

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]

And the definitions are in core :-)

[Johan Commelin]

Yeah, I guess so...

[Johan Commelin]

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

[Johan Commelin]

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]

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]

Is the problem that easy?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I had to use eq_add_of_sub_eq, add_comm, eq_sub_of_add_eq

[Kevin Buzzard]

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]

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]

Nice!

[Kevin Buzzard]

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

[Johan Commelin]

Now formalise the statement of the geometry question (-;

[Kevin Buzzard]

rofl I never liked the geometry questions :-)

[Floris van Doorn]

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

[Kevin Buzzard]

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]

I think my proof is better :P

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

Was that true 10 years ago in Coq though?

[Reid Barton]

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]

Oh nice!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Floris van Doorn]

I'm working on IMO2019-4...

[Reid Barton]

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]

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]

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]

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]

IMO2019-3 is just dec_trivial.