## Stream: new members

### Topic: debugging inefficient tactics

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

#### 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)


#### Kevin Lacker (Oct 01 2020 at 07:02):

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

#### Kevin Lacker (Oct 01 2020 at 07:02):

for a single case, norm_num works fine

#### Johan Commelin (Oct 01 2020 at 07:03):

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

#### Kevin Lacker (Oct 01 2020 at 07:03):

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

#### Johan Commelin (Oct 01 2020 at 07:03):

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

Oooh, ok

#### 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

#### Johan Commelin (Oct 01 2020 at 07:04):

That sounds like a good improvement, right?

#### Kevin Lacker (Oct 01 2020 at 07:04):

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

#### Kevin Lacker (Oct 01 2020 at 07:04):

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

#### Johan Commelin (Oct 01 2020 at 07:04):

Can you determine which part is slow?

#### Johan Commelin (Oct 01 2020 at 07:05):

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

#### Kevin Lacker (Oct 01 2020 at 07:05):

I don't know - is there a profiler?

#### Johan Commelin (Oct 01 2020 at 07:05):

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

#### Kevin Lacker (Oct 01 2020 at 07:05):

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

#### Johan Commelin (Oct 01 2020 at 07:05):

Yes... set_option profiler true

#### 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

#### 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

#### 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

#### 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

#### 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

#### Kevin Lacker (Oct 01 2020 at 07:09):

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

#### 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

#### 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?

#### 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

#### 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


#### Johan Commelin (Oct 01 2020 at 08:00):

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

#### Johan Commelin (Oct 01 2020 at 08:01):

And even 90 * 0.24 will time out

#### 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


#### Kevin Buzzard (Oct 01 2020 at 08:10):

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

#### Johan Commelin (Oct 01 2020 at 08:26):

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

#### 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

#### 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

#### Kevin Lacker (Oct 01 2020 at 08:33):

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

#### Johan Commelin (Oct 01 2020 at 08:36):

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

#### Johan Commelin (Oct 01 2020 at 08:36):

So there must be more that you can prove here

#### Kevin Lacker (Oct 01 2020 at 08:36):

the solutions on art of problem solving suggest brute forcing it

#### 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

plenty of time

#### Johan Commelin (Oct 01 2020 at 08:38):

That must be extremely boring to grade...

#### Kevin Lacker (Oct 01 2020 at 08:39):

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

#### 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 : _,
{ norm_num },
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 },
assumption_mod_cast },
{ norm_num },
{ ring_exp }
end


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

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

#### Kevin Lacker (Oct 01 2020 at 15:17):

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

#### Johan Commelin (Oct 01 2020 at 15:17):

yup the first and last

#### 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

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

#### Johan Commelin (Oct 01 2020 at 17:37):

What's supposed to be 550 or 803?

#### Kevin Lacker (Oct 01 2020 at 17:38):

the answers to the search over all 3-digit numbers

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

#### Johan Commelin (Oct 01 2020 at 17:38):

In both these cases, I prove the claim.

#### Kevin Lacker (Oct 01 2020 at 17:39):

which claim are you proving here

#### Johan Commelin (Oct 01 2020 at 17:40):

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

#### Kevin Lacker (Oct 01 2020 at 17:41):

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

#### 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

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

#### Kevin Lacker (Oct 01 2020 at 17:42):

how do you know how to do that

#### 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

#### Johan Commelin (Oct 01 2020 at 17:42):

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

#### 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

#### Johan Commelin (Oct 01 2020 at 17:47):

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

#### 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?

#### Mario Carneiro (Oct 01 2020 at 17:50):

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

#### 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

#### Mario Carneiro (Oct 01 2020 at 18:05):

That's literally what norm_num is designed for

#### Mario Carneiro (Oct 01 2020 at 18:06):

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

#### 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

#### 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

#### Mario Carneiro (Oct 01 2020 at 18:08):

because it has variables in it

#### Kevin Lacker (Oct 01 2020 at 18:26):

ok, thanks for explaining!

Last updated: May 10 2021 at 18:22 UTC