Zulip Chat Archive

Stream: new members

Topic: timeout in `cases`


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

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

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

view this post on Zulip 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.)

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

yeah, I just stuck that in to make it clear

view this post on Zulip Sebastien Gouezel (Oct 13 2020 at 07:51):

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

view this post on Zulip Sebastien Gouezel (Oct 13 2020 at 07:51):

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

view this post on Zulip 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

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

yeah, well casing on h1 also times out

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:09):

this one -> https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/deep.20recursion.20was.20detected.20at.20'replace'/near/212360087

view this post on Zulip 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.)

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

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

view this post on Zulip Kyle Miller (Oct 13 2020 at 08:13):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:17):

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

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Oct 13 2020 at 08:23):

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

view this post on Zulip 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 <|>
    fail "contradiction tactic failed")

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

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:32):

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

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:32):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:34):

You could just generalize the number...?

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:35):

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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:35):

I don't see how that changes anything

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:35):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:37):

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

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

numbers bigger than 12 are useful for a lot of things

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:38):

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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:38):

it talks about the whole infinite family

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:38):

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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:39):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:39):

and why is 1981 special?

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

because it's in the problem statement

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:40):

...because the test writers were being clever

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:40):

yes

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:40):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 13 2020 at 08:40):

yes I know

view this post on Zulip 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?

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:42):

I just don't understand why I would do that

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:43):

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

view this post on Zulip 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?

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:47):

that basically is the pp_reduction lemma

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Oct 13 2020 at 08:50):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ruben Van de Velde (Oct 13 2020 at 09:11):

That would be ne_of_monotone_of_lt_of_lt from #4482

view this post on Zulip Sebastien Gouezel (Oct 13 2020 at 09:47):

int.le is made irreducible in #4601

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Bryan Gin-ge Chen (Oct 14 2020 at 00:29):

The discussion reminds me of this classic MathOverflow post.

view this post on Zulip 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