Zulip Chat Archive

Stream: new members

Topic: cases timeout; using zfc sets

Evan Haskell (May 26 2021 at 01:07):

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 :=
  cases 0, -- deterministic timeout in vscode

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,
  intro n, sorry,

Mario Carneiro (May 26 2021 at 02:18):

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 (May 26 2021 at 02:20):


local attribute [irreducible] Set.mem

makes it instant

Last updated: Dec 20 2023 at 11:08 UTC