timeout in `cases`

Stream: new members

[Kevin Lacker]

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]

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]

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]

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

[Kyle Miller]

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

yeah, I just stuck that in to make it clear

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Kevin Lacker]

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

[Kevin Lacker]

yeah, well casing on h1 also times out

[Sebastien Gouezel]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Kyle Miller]

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

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

[Kyle Miller]

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

[Mario Carneiro]

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]

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

[Sebastien Gouezel]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Kevin Lacker]

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

[Sebastien Gouezel]

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]

You could just generalize the number...?

[Mario Carneiro]

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

[Kevin Lacker]

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

[Mario Carneiro]

I don't see how that changes anything

[Kevin Lacker]

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

[Mario Carneiro]

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]

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

[Kevin Lacker]

numbers bigger than 12 are useful for a lot of things

[Mario Carneiro]

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

[Mario Carneiro]

it talks about the whole infinite family

[Kevin Lacker]

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

[Mario Carneiro]

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

[Kevin Lacker]

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

[Mario Carneiro]

and why is 1981 special?

[Kevin Lacker]

because it's in the problem statement

[Mario Carneiro]

...because the test writers were being clever

[Kevin Lacker]

yes

[Mario Carneiro]

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

[Kevin Lacker]

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

[Mario Carneiro]

yes I know

[Mario Carneiro]

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]

I just don't understand why I would do that

[Kevin Lacker]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

that basically is the pp_reduction lemma

[Kyle Miller]

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]

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]

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]

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]

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

[Kevin Lacker]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

That would be ne_of_monotone_of_lt_of_lt from #4482

[Sebastien Gouezel]

int.le is made irreducible in #4601

[Mario Carneiro]

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]

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]

The discussion reminds me of this classic MathOverflow post.

[Joseph Myers]

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