Zulip Chat Archive

Stream: new members

Topic: debugging inefficient tactics


view this post on Zulip Kevin Lacker (Oct 01 2020 at 04:43):

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.

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:01):

@Johan Commelin it's this thread

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:02):

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)

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:02):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:02):

for a single case, norm_num works fine

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:03):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:03):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:03):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:03):

Oooh, ok

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:03):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:04):

That sounds like a good improvement, right?

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:04):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:04):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:04):

Can you determine which part is slow?

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:05):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:05):

I don't know - is there a profiler?

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:05):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:05):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:05):

Yes... set_option profiler true

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:06):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:07):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:07):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:08):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:08):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 07:09):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:18):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 07:19):

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

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 07:49):

@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

view this post on Zulip Scott Morrison (Oct 01 2020 at 07:54):

It's not quite that bad!

view this post on Zulip Shing Tak Lam (Oct 01 2020 at 07:58):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:00):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:01):

And even 90 * 0.24 will time out

view this post on Zulip Shing Tak Lam (Oct 01 2020 at 08:05):

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

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 08:10):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:26):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:30):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:31):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:33):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:36):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:36):

So there must be more that you can prove here

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:36):

the solutions on art of problem solving suggest brute forcing it

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:37):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:37):

plenty of time

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:38):

That must be extremely boring to grade...

view this post on Zulip Kevin Lacker (Oct 01 2020 at 08:39):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 10:03):

@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

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 11:02):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 15:09):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 15:17):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 15:17):

yup the first and last

view this post on Zulip Kevin Lacker (Oct 01 2020 at 15:32):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:36):

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.

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:37):

What's supposed to be 550 or 803?

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:38):

the answers to the search over all 3-digit numbers

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:38):

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.

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:38):

In both these cases, I prove the claim.

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:39):

which claim are you proving here

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:40):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:41):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:41):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:42):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:42):

how do you know how to do that

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:42):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:42):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:44):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:47):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 17:49):

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?

view this post on Zulip Mario Carneiro (Oct 01 2020 at 17:50):

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

view this post on Zulip Kevin Lacker (Oct 01 2020 at 18:01):

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

view this post on Zulip Mario Carneiro (Oct 01 2020 at 18:05):

That's literally what norm_num is designed for

view this post on Zulip Mario Carneiro (Oct 01 2020 at 18:06):

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

view this post on Zulip Mario Carneiro (Oct 01 2020 at 18:06):

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

view this post on Zulip Mario Carneiro (Oct 01 2020 at 18:08):

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

view this post on Zulip Mario Carneiro (Oct 01 2020 at 18:08):

because it has variables in it

view this post on Zulip Kevin Lacker (Oct 01 2020 at 18:26):

ok, thanks for explaining!


Last updated: May 10 2021 at 18:22 UTC