Deterministic timeout in rcases

Stream: general

[Violeta Hernández]

I'm having trouble with this proof:

import analysis.special_functions.trigonometric.basic

lemma two_mul_cos_cases {n : ℤ} {x : ℝ} (h : 2 * real.cos x = n) :
  n ∈ ({-2, -1, 0, 1, 2} : finset ℤ) :=
sorry

example {q : ℚ} : (∃ n : ℤ, 2 * real.cos (real.pi * q) = n) →
  int.fract q ∈ ({0, 1 / 3, 1 / 2, 2 / 3} : finset ℚ) :=
begin
  rintro ⟨n, hn⟩,
  have H := two_mul_cos_cases hn,
  simp only [finset.mem_insert, finset.mem_singleton] at H,
  rcases H with (rfl|rfl|rfl|rfl|rfl);
    sorry
end

The example times out. Changing the conclusion to something simpler makes it much faster. Changing simp only by rw or fin_cases still leads to the timeout.

[Violeta Hernández]

Changing the simp only line so that it also acts on the goal fixes this timeout...

[Mario Carneiro]

there is something really fishy going on in the expression ({0, 1 / 3, 1 / 2, 2 / 3} : finset ℚ)

[Mario Carneiro]

many basic operations take way longer than they should when that thing is around, and I managed to OOM kill lean while playing around with it

[Mario Carneiro]

my guess is that the expression consists of insert operations which require decidability of rat and this is blowing up for some reason on those concrete numbers

[Violeta Hernández]

You're almost certainly correct, since the problem goes away when I change finset with multiset

[Mario Carneiro]

this is fast:

example {q : ℚ} : (∃ n : ℤ, 2 * cos (pi * q) = n) →
  fract q ∈ ({0, 1 / 3, 1 / 2, 2 / 3} : finset ℚ) :=
begin
  generalize : (0:ℚ) = a,
  generalize : (1/3:ℚ) = b,
  generalize : (1/2:ℚ) = c,
  generalize : (2/3:ℚ) = d,
  rintro ⟨n, hn⟩,
end

but if you comment out the b and c or c and d lines then suddenly the rintro becomes really expensive

[Mario Carneiro]

which suggests that dec_trivial : 1 / 3 != 1 / 2 is being evaluated and something is not going well

[Violeta Hernández]

Is decidability of equality between rational fractions slow?

[Mario Carneiro]

it shouldn't be that slow

[Mario Carneiro]

ah, there is a gcd involved, maybe that's getting stuck

[Mario Carneiro]

Aha: when you whnf fract q ∈ ({a, b, c, d} : finset ℚ), you get list.mem (fract q) (list.insert a (list.insert b (list.insert c [d]))). Since it's using insert and not cons this does not make it all the way to the disjunction like you would prefer; and if you put in concrete numbers for a,b,c,d then it will have to evaluate whether they are equal or not before we can tell if it is definitionally a disjunction. This is a problem because lots of stuff likes to call whnf on the goal to find out if it's a prop and other things

[Mario Carneiro]

so the correct solution is to start the proof with simp only [finset.mem_insert, finset.mem_singleton], as you suggested

[Mario Carneiro]

oof:

#reduce as_true ((1 / 3 : ℚ) ≠ 1 / 2) -- timeout

[Mario Carneiro]

another way to "fix" it is to put local attribute [instance] classical.dec at the top of the file

[Mario Carneiro]

this will make the inserts infer the fake decidability instance, and this will fail to evaluate, meaning the whnf stops trying to reduce it earlier

[Mario Carneiro]

when you use the "computable" decidability instance, lean actually tries to compute it, and I suspect that whnf is even reducing proofs in order to evaluate the gcd, which times out

[Eric Wieser]

Why would the gcd time out here?

[Eric Wieser]

Is this to do with acc.rec being irreducible in the kernel?

[Mario Carneiro]

I think something is calling whnf with a really high reducibility setting

[Mario Carneiro]

here's a test you can play with, using the #whnf command:

section
open lean lean.parser

@[user_command] meta def whnf_cmd (_ : interactive.parse (tk "#whnf")) : lean.parser unit := do
  e ← parser.pexpr 0,
  (ts, _) ← synthesize_tactic_state_with_variables_as_hyps [e],
  of_tactic $ λ _, do {
    e ← tactic.to_expr e,
    e ← tactic.whnf e tactic.transparency.semireducible,
    tactic.trace e } ts

end

#whnf (1 / (3 : ℚ))

At this reducibility setting, it doesn't get evaluated much at all, but if you change semireducible to all it will evaluate the outer bit, and you can observe that e.g. (1 / (3 : ℚ)).denom - 3 reduces to 0

[Mario Carneiro]

interestingly, #whnf as_true ((1 / (3 : ℚ)) ≠ 1 / 2) evaluates to true quickly with all enabled and does not reduce at lower settings, so I'm not sure what got it stuck in a loop