debugging inefficient tactics

Stream: new members

[Kevin Lacker]

Hey, so I have this proof with a tactic that works for the number 5, and in theory it should work for 1000 which I need it to go up to. However, when I set the constant to above 30 or so, it pegs my CPU at 100% for a while and never terminates. Intuitively, I would only expect it to be using a small, linear amount of resources. But I am probably not understanding something about how it works. Is there some way I can profile this, figure out why it's slow, or is it fundamentally not going to work for some architectural reason?

lemma foo (n : ℕ) (h: n ∈ list.range 5) : ¬ problem_predicate n :=
begin
  iterate 5 {cases h, rw h, norm_num},

  unfold list.mem at *,
  finish
end

problem_predicate is just some short expression that norm_num can resolve for any one number.

[Kevin Lacker]

@Johan Commelin it's this thread

[Kevin Lacker]

def sum_of_squares (L : list ℕ) : ℕ := L.foldr (λ x y, x*x + y) 0

def problem_predicate (n : ℕ) :=
(nat.digits 10 n).length = 3 ∧ 11 ∣ n ∧ n / 11 = sum_of_squares (nat.digits 10 n)

[Kevin Lacker]

i want to prove \not problem_predicate n for n in, say, 0...500

[Kevin Lacker]

for a single case, norm_num works fine

[Johan Commelin]

I think it might be better to prove this, instead of computing it.

[Kevin Lacker]

there's no "nice" reason this is true, unfortunately

[Johan Commelin]

Although it is of course nice if Lean could just bash through the 1000 cases.

[Johan Commelin]

Oooh, ok

[Kevin Lacker]

I can cut it down and only pay attention to the multiples of 11, and make it only like 90 cases

[Johan Commelin]

That sounds like a good improvement, right?

[Kevin Lacker]

yeah, but I still can't expand a fin_cases by 90x

[Kevin Lacker]

or even compile a 90-line file where each line is calling a norm_num

[Johan Commelin]

Can you determine which part is slow?

[Johan Commelin]

Is it the division, or computing the digits? Or the sum of squares?

[Kevin Lacker]

I don't know - is there a profiler?

[Johan Commelin]

If computing the digits is slow, then you might just generate the lists.

[Kevin Lacker]

intuitively, I don't really understand why any of it would be slow

[Johan Commelin]

Yes... set_option profiler true

[Johan Commelin]

But it won't look inside norm_num. So you will have to cut it into steps yourself

[Johan Commelin]

There is also try_for which might be helpful to impose some bounds on the running time of some tactics

[Kevin Lacker]

i see - well it's almost certainly inside norm_num, because i can write the whole loop as one refine plus one norm_num

[Kevin Lacker]

all right, well at least you weren't like ho ho you haven't heard of the *&{/run fast/}& operator? just enable that and it'll all work in one line

[Kevin Lacker]

i am moderately reassured that the amount this is bugging me may be proportional to the fundamental difficulty

[Kevin Lacker]

i'll try seeing if i can cut norm num into different steps here

[Johan Commelin]

Yup, it would be good to know which part of the computation is taking a lot of time

[Johan Commelin]

Like, does can it do nat.digits 10 345 = [3, 4, 5] fast? Can it do 90 of such computations in 1 second?

[Kevin Buzzard]

@Kevin Lacker Lean was not designed to compute, people have been concentrating on getting it to prove mathematical theorems whose proofs are pure thought arguments rather than brute force computations. Remember the definition of nat is via peano and this is an extremely inefficient way of working with naturals from a computational purpose -- but it's the best way for theorem proving

[Scott Morrison]

It's not quite that bad!

[Shing Tak Lam]

I don't think norm_num is the issue here to be honest. (nb: my mathlib is a few weeks old, so the example below probably doesn't check for you).

import tactic
import data.nat.digits

def sum_of_squares (L : list ℕ) : ℕ := L.foldr (λ x y, x*x + y) 0

def problem_predicate (n : ℕ) :=
let x := digits 10 n in
x.length = 3 ∧ 11 ∣ n ∧ n = sum_of_squares x * 11

set_option profiler true

example : ¬problem_predicate 345 :=
begin
  unfold problem_predicate,
  norm_num,
end -- 240ms on my not very fast laptop

[Johan Commelin]

@Shing Tak Lam But 0.24s * 1000 is quite a bit

[Johan Commelin]

And even 90 * 0.24 will time out

[Shing Tak Lam]

Maybe it's worth it to break it down to separate lemmas for 0 <= n < 10, 10 <= n < 20, ... and then prove it that way. Something like this might help?

lemma helper (P : ℕ → Prop) (a b c : ℕ) (h1 : ∀ x, a ≤ x → x ≤ b → P x) (h2 : ∀ x, b ≤ x → x ≤ c → P x) :
  ∀ x, a ≤ x → x ≤ c → P x := sorry

[Kevin Buzzard]

Yes Scott's right, Lean is capable of doing computations -- but don't expect miracles.

[Johan Commelin]

@Shing Tak Lam I think KevinL said that even that didn't help

[Kevin Lacker]

yeah, the problem is just the large number of norm_nums. If I write a python program that completely unrolls the loop into 1000 different lemmas, lean has trouble compiling the resulting file. so just solving the case-expansion part isn't sufficient

[Kevin Lacker]

@Kevin Buzzard well, you know, i dont write IMO problems so don't blame me if some of them require brute force :P

[Kevin Lacker]

i bet this is the sort of thing that will allegedly be better in lean 4

[Johan Commelin]

@Kevin Lacker but the competitors weren't supposed to brute force through 90 cases, right?

[Johan Commelin]

So there must be more that you can prove here

[Kevin Lacker]

the solutions on art of problem solving suggest brute forcing it

[Kevin Lacker]

you have what, an hour per problem? that's a whole minute to brute force, what's the sum of the squares of the digits of the number 550

[Kevin Lacker]

plenty of time

[Johan Commelin]

That must be extremely boring to grade...

[Kevin Lacker]

well it was an early imo problem, there were only 39 contestants at the time

[Johan Commelin]

@Kevin Lacker maybe I missed something, but I think this is a proof. only need to assemble some pieces

def problem_predicate₁ (a b : ℕ) : Prop :=
2 * (a * a) + 2 * (a * b) + 2 * (b * b) = 1210 * a + 121 * b

lemma foo (a b : ℕ) (ha : a ≤ 9) (hb : b ≤ 9) (ha1 : 1 ≤ a) :
  ¬ problem_predicate₁ a b :=
begin
  rw problem_predicate₁,
  apply ne_of_lt,
  calc  2 * (a * a) + 2 * (a * b) + 2 * (b * b)
      ≤ 2 * (9 * 9) + 2 * (9 * 9) + 2 * (9 * 9) : _
  ... < 487 * 1 + 0 : _
  ... ≤ 1210 * a + 121 * b : _,
  { apply_rules [add_le_add, mul_le_mul, le_refl, nat.zero_le] },
  { norm_num },
  { apply add_le_add _ (nat.zero_le _),
    apply nat.mul_le_mul _ ha1,
    norm_num },
end

def problem_predicate₂ (a b : ℕ) : Prop :=
(a * a) + (a + b - 11) * (a + b - 11) + (b * b) = 11 * (100 * a + 10 * (a + b - 11) + b)


lemma bar (a b : ℕ) (ha : a ≤ 9) (hb : b ≤ 9) (hab : 11 ≤ a + b) :
  ¬ problem_predicate₂ a b :=
begin
  rw problem_predicate₂,
  have ha2 : 2 ≤ a,
  { contrapose! hab, rw nat.lt_succ_iff at hab ⊢, linarith },
  have hb2 : 2 ≤ b,
  { contrapose! hab, rw nat.lt_succ_iff at hab ⊢, linarith },
  obtain ⟨a, rfl⟩ := nat.exists_eq_add_of_le ha2,
  replace ha : a ≤ 7, { linarith },
  obtain ⟨b, rfl⟩ := nat.exists_eq_add_of_le hb2,
  replace hb : b ≤ 7, { linarith },
  clear ha2 hb2,
  zify,
  simp only [int.coe_nat_sub hab, int.coe_nat_add, int.coe_nat_bit0, int.coe_nat_bit1, int.coe_nat_one],
  have aux : ∀ (n : ℕ), n ≤ 7 → 2 * (n : ℤ) ^ 2 - 10 * n ≤ 100,
  { dec_trivial },
  apply ne_of_lt,
  calc _ = ((2 * a ^ 2 - 10 * a) + (2 * b ^ 2 - 10 * b) + 2 * a * b + 57 : ℤ) : _
  ... ≤ 100 + 100 + (2 * 7 * 7) + 57 : _
  ... < (0 * 0 + 0 * 0) + 1452 : _
  ... ≤ (1210 * a + 121 * b : ℤ) + 1452 : _
  ... = _ : _,
  { ring_exp },
  { apply_rules [aux, add_le_add, le_refl, mul_le_mul, int.coe_nat_nonneg];
    assumption_mod_cast },
  { norm_num },
  { apply add_le_add _ (le_refl _),
    apply add_le_add; apply mul_le_mul; norm_num <|> assumption_mod_cast },
  { ring_exp }
end

[Kevin Buzzard]

@Kevin Lacker funnily enough I have written Olympiad problems (including IMO) and we really try to avoid giving students boring case bashes --certainly 100 cases is way too many.

[Kevin Lacker]

@Kevin Buzzard yeah, I saw your name on there when I was looking through the IMO problems ;-) some of the older problems seem like they'd never make it by today's standards.

[Kevin Lacker]

@Johan Commelin what are a and b there - two of the three digits of the number?

[Johan Commelin]

yup the first and last

[Kevin Lacker]

hmm, i'm not really following what these predicates are. tools for doing a subsequent search? the answer is supposed to be 550 or 803, so that has to pop out somehow

[Kevin Lacker]

for what it's worth, I got this working, by writing some explicit ways to simplify these expressions and passing them to norm_num so that the norm_num call doesn't take so long, and by splitting the iterate call up into chunks of size <= 40.

[Johan Commelin]

What's supposed to be 550 or 803?

[Kevin Lacker]

the answers to the search over all 3-digit numbers

[Johan Commelin]

If you have a 3-digit number axb that is divisible by 11, then 11 divides a - x + b. So there are two cases: x = a + b or x + 11 = a + b.

[Johan Commelin]

In both these cases, I prove the claim.

[Kevin Lacker]

which claim are you proving here

[Johan Commelin]

Hmm, there must be a mistake in my formalization of the problem (-;

[Kevin Lacker]

it's kind of ridiculous how many theorems humans take for granted about "three digit numbers"

[Kevin Lacker]

and, since three digit numbers are not particularly interesting for abstract mathematics, there isn't really a library of a zillion things about them

[Kevin Lacker]

so i'm curious about your code - when you write something like apply_rules [aux, add_le_add, le_refl, mul_le_mul, int.coe_nat_nonneg];

[Kevin Lacker]

how do you know how to do that

[Kevin Lacker]

are you already familiar with what aux, add_le_add, le_refl, all those things do, and you are just thinking hmm i'll apply these

[Johan Commelin]

I think the more interesting question is what the mistake is in my statement (-;

[Kevin Lacker]

well, the math problem is not a very interesting problem. the problem with these enormous case-by-case bashes is you forget a minus sign somewhere and then waste half an hour of calculation on nothing

[Johan Commelin]

Yup... that's (sort of) what happened

[Kevin Lacker]

in your code i see a bunch of different tactics i dont recognize. apply_rules, obtain, replace. I don't see these mentioned in https://leanprover.github.io/theorem_proving_in_lean/tactics.html . Is there something else I can be reading about tactics?

[Mario Carneiro]

the mathlib docs are much more up to date than TPIL on mathlib tactics

[Kevin Lacker]

so is there a way to simplify an expression that just uses built in operators like ((18 + 1) * 11 % 10) ^ 2, without having to call norm_num? I feel like that is sort of what Johan is doing with that apply_rules [long, list, of, random, characters], but i'm not sure how i could construct by own such thing

[Mario Carneiro]

That's literally what norm_num is designed for

[Mario Carneiro]

If it's a one off thing you should absolutely use norm_num

[Mario Carneiro]

If you are doing it 900 times in a loop then you should preprocess the expression to make it easier to evaluate

[Mario Carneiro]

But the apply_rules line in Johan's proof is not something norm_num can do, but rather the monotonicity tactic

[Mario Carneiro]

because it has variables in it

[Kevin Lacker]

ok, thanks for explaining!