cases timeout; using zfc sets

Stream: new members

[Evan Haskell]

I've been working through a book on axiomatic set theory and have been proving much of it in lean for fun using the constructions in set_theory.zfc. But I've run into a deterministic timeout on a few occasions. Here's a MWE.

import set_theory.zfc

namespace Set

def dom (R : Set) : Set := {x ∈ R.Union.Union | ∃ y, x.pair y ∈ R}
def ran (R : Set) : Set := {y ∈ R.Union.Union | ∃ x : Set, x.pair y ∈ R}
def fun_value (F x : Set) : Set := {y ∈ F.Union.Union | x.pair y ∈ F}.Union
def inv (R : Set) : Set := pair_sep (λ a b, b.pair a ∈ R) R.ran R.dom

theorem ttt {F : Set} : F.inv.fun_value ∅ ∈ F :=
begin
  cases 0, -- deterministic timeout in vscode
end

end Set

The lean command returns after ~10 seconds. cases and related tactics timeout regardless of the arguments. It doesn't timeout if I remove .inv or .fun_value ∅ or replace ∈ with = in the goal. Is the goal just too complicated? What's going on? Can I increase the timeout threshold?

The strange thing is I can do nat.cases_on without issue:

  apply @nat.cases_on (λ n, F.inv.fun_value ∅ ∈ F) 0,
    sorry,
  intro n, sorry,

[Mario Carneiro]

I would guess that cases is trying to find the weak head normal form of the goal and this is particularly expensive for the example goal

[Mario Carneiro]

adding

local attribute [irreducible] Set.mem

makes it instant