## Stream: new members

### Topic: timeout in cases

#### Kevin Lacker (Oct 13 2020 at 07:37):

I'm trying to expand an existence clause in a hypothesis and Lean is timing out for some reason I can't figure out:

def in_range (n : ℤ) : Prop := 0 < n ∧ n ≤ 1981

def problem_predicate (m n : ℤ) : Prop :=
in_range m ∧ in_range n ∧ (n ^ 2 - m * n - m ^ 2) ^ 2 = 1

def specified_set : set ℤ :=
{k : ℤ | ∃ m : ℤ, ∃ n : ℤ, (k = m ^ 2 + n ^ 2 ∧ problem_predicate m n)}

lemma solution_bound {k : ℤ} (h1 : k ∈ specified_set) : k ≤ 3524578 :=
begin
have h2 : ∃ m : ℤ, ∃ n : ℤ, (k = m ^ 2 + n ^ 2 ∧ problem_predicate m n), from h1,
cases h2 with h3 h4, -- this line times out
end


I thought I wasn't doing anything fancy here - h2 is a hypothesis starting with ∃, so I use a cases tactic, but this times out. What's going on here?

#### Sebastien Gouezel (Oct 13 2020 at 07:46):

This is really strange. Changing the bound in the goal from 3524578 to something small makes the problem go away. I don't see why a complicated goal should change something to casing on an hypothesis... Same thing with rcases or obtain.

#### Kyle Miller (Oct 13 2020 at 07:47):

I'm going to guess it's the large number in the goal. This times out, too:

example {k : ℤ} : k ≤ 3524578 :=
begin
exfalso, -- times out
sorry
end


#### Kevin Lacker (Oct 13 2020 at 07:48):

hmm. well at least I was justified in finding it strange

#### Kyle Miller (Oct 13 2020 at 07:50):

(By the way, rather than your have h2 line, you can do simp only [specified_set, set.mem_set_of_eq] at h1, to put it into the same form.)

#### Kevin Lacker (Oct 13 2020 at 07:51):

yeah, I just stuck that in to make it clear

#### Sebastien Gouezel (Oct 13 2020 at 07:51):

Yes, I have no clue about what is going on.

#### Sebastien Gouezel (Oct 13 2020 at 07:51):

You don't even need the h2 line, you can case on h1.

#### Kevin Lacker (Oct 13 2020 at 07:51):

I was wondering if there was some problem with converting between the set-membership and the other form of the statement

#### Kevin Lacker (Oct 13 2020 at 07:51):

yeah, well casing on h1 also times out

#### Sebastien Gouezel (Oct 13 2020 at 07:52):

Yes, I was just saying that casing on h1 or h2 is the same. If one fails, the other one will fail similarly.

#### Sebastien Gouezel (Oct 13 2020 at 07:53):

I guess at some place it goes back from the binary expansion of the constant in the goal to the unary expansion, which is too large. But I really don't see why it should do something like that!

#### Sebastien Gouezel (Oct 13 2020 at 08:02):

Minimal example:

import linear_algebra.basic

lemma solution_bound {k : ℤ} :
let p := (3524578 : ℤ) in k ≤ p :=
begin
simp,
exfalso, -- times out with the simp
end


Without the simp call, it doesn't time out.

#### Kyle Miller (Oct 13 2020 at 08:07):

A workaround:

lemma solution_bound {k : ℤ} (h1 : k ∈ specified_set) : k ≤ (3524578 : ℕ) :=
begin
simp only [specified_set, set.mem_set_of_eq] at h1,
cases h1 with h3 h4,
sorry
end


#### Mario Carneiro (Oct 13 2020 at 08:08):

It's the same issue that was remarked on in the norm_num thread, I think. Inequality on int is defined to be either true or false, so it's easy to get into a situation where whnf on the goal causes divergence

#### Kyle Miller (Oct 13 2020 at 08:12):

@Mario Carneiro Testing what you said, indeed this does not time out:

example {k : ℤ} : -3524578 ≤ -k :=
begin
exfalso, -- does not time out
end


(I'm assuming whnf of k - 3524578 involves a nontrivial amount of computation, but -(-3524578) - (-k) does not.)

#### Mario Carneiro (Oct 13 2020 at 08:13):

aha, it's probably when the numeral is on the right

#### Kyle Miller (Oct 13 2020 at 08:13):

And the workaround from before has a coercion to block the whnf.

#### Mario Carneiro (Oct 13 2020 at 08:14):

from the prelude:

def nonneg (a : ℤ) : Prop := int.cases_on a (assume n, true) (assume n, false)

protected def le (a b : ℤ) : Prop := nonneg (b - a)

protected def lt (a b : ℤ) : Prop := (a + 1) ≤ b


#### Mario Carneiro (Oct 13 2020 at 08:17):

I wonder if it would be better to make nonneg a structure to prevent this unfolding

#### Sebastien Gouezel (Oct 13 2020 at 08:20):

I thought that int.le has been made irreducible in #4474? Apparently this is not the case...

import linear_algebra.basic

attribute [irreducible] int.le

lemma solution_bound {k : ℤ} :
k ≤ (3257648 : ℤ) :=
begin
exfalso, -- times out without the irreducible attribute
end


#### Sebastien Gouezel (Oct 13 2020 at 08:23):

It's only int.lt that was marked irreducible...

#### Mario Carneiro (Oct 13 2020 at 08:27):

Aha:

meta def contradiction : tactic unit :=
do try intro1,
ctx ← local_context,
(contra_false ctx <|>
contra_not_a_refl_rel_a ctx <|>
contra_p_not_p ctx ctx <|>
contra_constructor_eq ctx <|>

meta def exfalso : tactic unit :=
do fail_if_no_goals,
assert Hfalse (expr.const false []),


exfalso calls contradiction, which fails at the first line, try intro1, because the state at that point is:

state:
2 goals
k : ℤ,
Hfalse : false
⊢ k ≤ 3524578

k : ℤ
⊢ false


so intro1 is going to try to check if the goal is an implication, which will involve a whnf

#### Mario Carneiro (Oct 13 2020 at 08:28):

I mean for all lean knows at the bottom of the stack of definitions nonneg might unfold to true -> true instead of true

#### Mario Carneiro (Oct 13 2020 at 08:30):

for something like try intro1 at the beginning of a more complicated tactic, it seems pretty obvious that lean wasn't supposed to try this hard, though. Probably intro1 should have a transparency parameter

#### Kevin Lacker (Oct 13 2020 at 08:32):

well, I got around it by making one lemma just not use any tactics

#### Kevin Lacker (Oct 13 2020 at 08:32):

eventual proof in https://github.com/leanprover-community/mathlib/pull/4599

#### Sebastien Gouezel (Oct 13 2020 at 08:33):

It's not specific to exfalso:

import linear_algebra.basic

lemma foo (k : ℤ) (h : ∃ (i : ℤ), true) : k ≤ 1543678 :=
begin
cases h,
end


fails in the same way.

#### Mario Carneiro (Oct 13 2020 at 08:34):

You could just generalize the number...?

#### Mario Carneiro (Oct 13 2020 at 08:34):

there is no need to have big numbers in your goal, just generalize them after establishing the requisite facts with norm_num

#### Kevin Lacker (Oct 13 2020 at 08:35):

hmm, well as it happens I am proving several lemmas about 3524578

#### Mario Carneiro (Oct 13 2020 at 08:35):

I don't see how that changes anything

#### Kevin Lacker (Oct 13 2020 at 08:35):

I guess I'm not sure what your suggestion is, exactly

#### Mario Carneiro (Oct 13 2020 at 08:36):

rather than proving things about the number 2019 because the test writers think they are being clever, prove the theorem for all numbers satisfying a property

#### Mario Carneiro (Oct 13 2020 at 08:37):

The Metamath library developed for over a decade without needing any numbers bigger than 12

#### Kevin Lacker (Oct 13 2020 at 08:37):

numbers bigger than 12 are useful for a lot of things

#### Mario Carneiro (Oct 13 2020 at 08:38):

It's not like the library didn't talk about natural numbers bigger than 12

#### Mario Carneiro (Oct 13 2020 at 08:38):

it talks about the whole infinite family

#### Kevin Lacker (Oct 13 2020 at 08:38):

sometimes you just want to know whether a particular fact is true about 3524578

#### Mario Carneiro (Oct 13 2020 at 08:39):

it's almost always a better idea to generalize to the relevant fact about that number

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

true, this number is special because it's the sum of the squares of the two largest fibonacci numbers smaller than 1981

#### Mario Carneiro (Oct 13 2020 at 08:39):

and why is 1981 special?

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

because it's in the problem statement

#### Mario Carneiro (Oct 13 2020 at 08:40):

...because the test writers were being clever

yes

#### Mario Carneiro (Oct 13 2020 at 08:40):

so now, generalize 1981 to n and tell me whether the theorem still holds

#### Kevin Lacker (Oct 13 2020 at 08:40):

that's why when you are practicing for the IMO, you make sure to note any interesting properties of the current year

yes I know

#### Mario Carneiro (Oct 13 2020 at 08:42):

Looking at the PR, it looks like the problem has the form determine M(n) where n = 1981. How about defining M(n) instead of M(1981) then?

#### Kevin Lacker (Oct 13 2020 at 08:42):

I just don't understand why I would do that

#### Kevin Lacker (Oct 13 2020 at 08:43):

I mean, as a workaround to avoid mentioning large numbers, it works, but there are easier workarounds

#### Mario Carneiro (Oct 13 2020 at 08:43):

because it will make the file compile much faster, and it will also make the file actually prove something useful instead of just being a cute and useless fact

#### Kevin Lacker (Oct 13 2020 at 08:43):

it's still not useful at all when you replace 1981 with n

#### Mario Carneiro (Oct 13 2020 at 08:46):

Determine the maximum value of m ^ 2 + n ^ 2, where m and n are integers in
{1, 2, ..., 1981} and (n ^ 2 - m * n - m ^ 2) ^ 2 = 1.
The trick to this problem is that m and n have to be consecutive Fibonacci numbers,
because you can reduce any solution to a smaller one using the Fibonacci recurrence.


this looks like a useful observation. Why not extract it as a lemma?

#### Kevin Lacker (Oct 13 2020 at 08:47):

that basically is the pp_reduction lemma

#### Kyle Miller (Oct 13 2020 at 08:47):

I'm not understanding why to generalize this IMO problem -- I know why as a mathematician, but it seems like this IMO folder is for formalizations of solutions to IMO problems. You wouldn't expect a test-taker to give a full solution to the generalized problem.

#### Mario Carneiro (Oct 13 2020 at 08:48):

I know that this number abstraction method is very useful in physics problems. You are given a problem statement with a bunch of numbers, and rather than doing intermediate calculations the first thing you do is replace all the numbers in the input with variables, solve the whole problem, then plug and chug at the end

#### Kevin Lacker (Oct 13 2020 at 08:49):

the thing is that if you generalize this problem, you have to define a bunch of awkward functions like "the largest fibonacci number less than x". and then prove things about them. but if you just stick with 1981 then you can skip a bunch of that

#### Mario Carneiro (Oct 13 2020 at 08:49):

It's not even about getting a more general result, although that often happens as a side effect. It's about localizing the calculator stuff to one small part and doing algebra with letters

#### Mario Carneiro (Oct 13 2020 at 08:50):

No, you just need a number m (the answer) that relates to n (the year) in some way

#### Kevin Lacker (Oct 13 2020 at 08:50):

that way is the largest pair of fibonacci numbers less than the current year

#### Mario Carneiro (Oct 13 2020 at 08:51):

it's not a function, it's a relation, the collection of all numerical properties between the numbers that you need a calculator for

#### Mario Carneiro (Oct 13 2020 at 08:51):

If you can write it as m = f(n) then that's even better but it's not a necessity

#### Mario Carneiro (Oct 13 2020 at 08:54):

In fact, it looks like you are using a property of monotone functions that @Kevin Buzzard pointed out in the question about n ^ 3 != 2, where the fib function sandwiches 1981 at fib 17 and fib 18

#### Ruben Van de Velde (Oct 13 2020 at 09:11):

That would be ne_of_monotone_of_lt_of_lt from #4482

#### Sebastien Gouezel (Oct 13 2020 at 09:47):

int.le is made irreducible in #4601

#### Mario Carneiro (Oct 13 2020 at 09:53):

I pushed a commit to the IMO 1981-Q3 PR that implements the N = 1981 generalization, without rewriting too much of the rest of the formalization.

#### Joseph Myers (Oct 14 2020 at 00:26):

Kyle Miller said:

I'm not understanding why to generalize this IMO problem -- I know why as a mathematician, but it seems like this IMO folder is for formalizations of solutions to IMO problems. You wouldn't expect a test-taker to give a full solution to the generalized problem.

I think the idea is that, for whatever reason, formalizing a more general result can end up being easier than formalizing a more specific result, even if no-one is going to have any use for the general result beyond proving the specific one (because the general one is still only relevant to this one problem, so isn't going in the main part of mathlib). That is, "prove the most general result that your argument gives, and then apply it to the specific case" is a formalization trick just like "use this tactic" or "write lots of small lemmas rather than one big proof"; a way in which the things that work best in formalization differ from what's convenient in informal mathematics. (Note that "the most general result that your argument gives" may well be less general than the most general version of the problem that's actually true.)

#### Bryan Gin-ge Chen (Oct 14 2020 at 00:29):

The discussion reminds me of this classic MathOverflow post.

#### Joseph Myers (Oct 14 2020 at 00:30):

Yes, it's a useful trick in informal mathematics, it just seems more often useful in formalization.

Last updated: May 12 2021 at 23:13 UTC