Zulip Chat Archive
Stream: mathlib4
Topic: brute force calculation of Bell/Stirling numbers
Yakov Pechersky (Apr 03 2023 at 01:59):
As part of familiarizing myself with lean4, I am attempting to formalize Bell's and Stirling numbers. With Bhavik, we tried the "brute force" counting approach for a small number, like 3. This code works in mathlib3, and doesn't time out up to n = 3.
import order.partition.finpartition
open finset
instance fintype_finpartition {α : Type*} [decidable_eq α] (a : finset α) :
fintype (finpartition a) :=
{ elems := a.powerset.powerset.image
(λ p, if h : p.sup_indep id ∧ p.sup id = a ∧ ⊥ ∉ p then ⟨p, h.1, h.2.1, h.2.2⟩ else ⊥),
complete :=
begin
rintro p,
rw [finset.mem_image],
refine ⟨p.parts, _, _⟩,
{ simp only [finset.mem_powerset],
intros i hi,
rw finset.mem_powerset,
exact p.le hi },
{ rw [dif_pos],
ext : 1,
{ refl },
simp only [p.sup_indep, p.sup_parts, p.not_bot_mem, eq_self_iff_true, not_false_iff,
and_self] },
end }
example : @fintype.card (finpartition (∅ : finset unit)) (fintype_finpartition _) = 1 := rfl
example : @fintype.card (finpartition (∅ : finset unit)) (fintype_finpartition _) = 1 := dec_trivial
example : @fintype.card (finpartition (range 3)) (fintype_finpartition _) = 5 := rfl
Yakov Pechersky (Apr 03 2023 at 02:00):
Bhavik also has a version of an explicit partition construction on lists that can go up to n = 8.
Yakov Pechersky (Apr 03 2023 at 02:00):
However, the equivalent code in mathlib4 dies even on the empty partition example!
Yakov Pechersky (Apr 03 2023 at 02:00):
import Mathlib.Order.Partition.Finpartition
open Finset
instance Finpartition.fintype_finset
{α : Type _} [DecidableEq α] (a : Finset α) : Fintype (Finpartition a) where
elems := a.powerset.powerset.image
(λ p => if h : p.SupIndep id ∧ p.sup id = a ∧ ⊥ ∉ p then ⟨p, h.1, h.2.1, h.2.2⟩ else ⊥)
complete := by
rintro p
rw [mem_image]
refine' ⟨p.parts, _, _⟩
· simp only [mem_powerset]
intros i hi
rw [mem_powerset]
exact p.le hi
· rw [dif_pos]
simp only [p.supIndep, p.supParts, p.not_bot_mem, eq_self_iff_true, not_false_iff, and_self]
example : @Fintype.card (Finpartition (∅ : Finset Unit)) (Finpartition.fintype_finset _) = 1 := rfl
-- (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Yakov Pechersky (Apr 03 2023 at 02:01):
what am I missing/what's the change that causes this "regression"?
Yaël Dillies (Apr 03 2023 at 07:00):
Could it be a missing computable recursor? We've been adding those by hand.
Reid Barton (Apr 03 2023 at 07:11):
that's a different kind of computation
Reid Barton (Apr 03 2023 at 07:13):
Maybe try with eta experiment? I'm not sure if it would make things better or worse
Yakov Pechersky (Apr 03 2023 at 15:23):
That seems to run indefinitely using 100% CPU
Chris Hughes (Apr 03 2023 at 17:20):
My guess would be that there's some use of Acc blocking the computation. Either something now uses Acc that didn't before, probably a function defined with pattern matching, or Acc is reducing less often in Lean4 because in general reduction doesn't terminate and the heuristic has slightly changed.
Yakov Pechersky (Apr 03 2023 at 17:58):
Do you have a suggestion on how to inspect where this could be occurring?
Yakov Pechersky (Apr 03 2023 at 17:59):
I don't know how to "follow" a rfl proof in either lean3 or lean4, nor how to interrupt a long running rfl proof
Matthew Ballard (Apr 03 2023 at 18:02):
[Meta.isDefEq] [14.641187s] 💥 Fintype.card (Finpartition ∅) = 1 =?= ?m.4430 = ?m.4430
Matthew Ballard (Apr 03 2023 at 18:03):
I turned on
set_option profiler true in
set_option trace.Meta.isDefEq true in
but didn't poke it further
Matthew Ballard (Apr 03 2023 at 18:05):
Just turned off the heart beats bounds to see if it actually finishes
Matthew Ballard (Apr 03 2023 at 18:08):
It does
Matthew Ballard (Apr 03 2023 at 18:12):
And now I have 130k lines of output :/
Matthew Ballard (Apr 03 2023 at 18:19):
This looks like one blocker
Reid Barton (Apr 03 2023 at 18:35):
This would certainly also take me more than 100 seconds to prove
Reid Barton (Apr 03 2023 at 18:36):
Does it break down further into slow things?
Matthew Ballard (Apr 03 2023 at 18:36):
I am tracing instance synthesis to get more info. I have tried set_option trace.Meta.whnf true but I haven't been able to make it work (ever)
Reid Barton (Apr 03 2023 at 18:38):
Oh right, there can still be unsolved decidability instance metavariables and stuff while we're doing isDefEq, though I'm not sure why it would be the case here?
Matthew Ballard (Apr 03 2023 at 18:39):
You are putting more thought into than me :)
Reid Barton (Apr 03 2023 at 18:40):
I am just assuming they could only occur in the example itself, because ones in the defs it uses would have been solved already.
Matthew Ballard (Apr 03 2023 at 18:41):
The decidability stuff is still not defeq right?
Reid Barton (Apr 03 2023 at 18:41):
Certainly we need to synthesize some Fintype instance but I guess that happen before everything else
Matthew Ballard (Apr 03 2023 at 18:41):
Hmm
Matthew Ballard (Apr 03 2023 at 18:42):
Going to let this finish but someone else could try using @ and (_) on instance argumentsin the meantime
Reid Barton (Apr 03 2023 at 18:42):
what do you mean? If you have something like if h then x else y then it really means to call Decidable.rec on the implicit decidability instance for h, with x and y as the other arguments... and all that stuff should show up as intermediate states in isDefEq
Reid Barton (Apr 03 2023 at 18:43):
And the decidability instance for say Finset.SupIndep p id ∧ Finset.sup p id = ∅ ∧ ¬⊥ ∈ p should have been synthesized already in the definition of whatever contains that.
Matthew Ballard (Apr 03 2023 at 18:43):
Sorry, I was thinking of something else
Matthew Ballard (Apr 03 2023 at 18:58):
Maybe somewhere down line two different (slowly) defeq instances are being synthesized? But I am not sure where that would be. Only going of my limited experience of very slow but successful checks where this has been the majority of cases
Yakov Pechersky (Apr 03 2023 at 19:59):
I don't think it's about instances. It's having issues proving that {} and {{}} are different
Yakov Pechersky (Apr 03 2023 at 20:01):
import Mathlib.Data.Finset.Powerset
set_option autoImplicit false
set_option profiler true
set_option trace.Meta.isDefEq true
example : (∅ : Finset Unit).powerset = {∅} := rfl
/-
[0.034324s] ✅ Finset.powerset ∅ = {∅} =?= ?m.230 = ?m.230
-/
example : (∅ : Finset Unit).powerset.powerset = {∅, {∅}} := rfl
/-
[5.022038s] ✅ Finset.powerset (Finset.powerset ∅) = {∅, {∅}} =?= ?m.3885 = ?m.3885 ▼
[] [0.000001s] ✅ Finset (Finset (Finset Unit)) =?= Finset (Finset (Finset Unit))
[] [2.480647s] ✅ {∅,
{∅}}.val =?= Multiset.pmap Finset.mk (Multiset.powerset (Finset.powerset ∅).val)
(_ : ∀ (_t : Multiset (Finset Unit)), _t ∈ Multiset.powerset (Finset.powerset ∅).val → Multiset.Nodup _t) ▶
[] [2.541109s] ✅ {∅, {∅}}.nodup =?= Finset.powerset.proof_2 (Finset.powerset ∅) ▼
[] [2.540974s] ✅ {∅,
{∅}}.val =?= Eq.ndrecOn (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(_ :
(Quot.lift
(Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
fun l H => ↑(List.pmap Finset.mk l H))
(_ :
∀ (a b : List (Multiset (Finset Unit))),
Setoid.r a b →
Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(fun l H => ↑(List.pmap Finset.mk l H)) a =
Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(fun l H => ↑(List.pmap Finset.mk l H)) b)
(Multiset.powerset (Finset.powerset ∅).val)).fst =
Multiset.powerset (Finset.powerset ∅).val)
(Quot.lift
(Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
fun l H => ↑(List.pmap Finset.mk l H))
(_ :
∀ (a b : List (Multiset (Finset Unit))),
Setoid.r a b →
Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(fun l H => ↑(List.pmap Finset.mk l H)) a =
Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(fun l H => ↑(List.pmap Finset.mk l H)) b)
(Multiset.powerset (Finset.powerset ∅).val)).snd
(_ :
∀ (_t : Multiset (Finset Unit)),
_t ∈ Multiset.powerset (Finset.powerset ∅).val → Multiset.Nodup _t) ▼
[] [2.540100s] ✅ {∅,
{∅}}.1 =?= (Quot.lift
(Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
fun l H => ↑(List.pmap Finset.mk l H))
(_ :
∀ (a b : List (Multiset (Finset Unit))),
Setoid.r a b →
Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(fun l H => ↑(List.pmap Finset.mk l H)) a =
Quot.indep (motive := fun x =>
(∀ (a : Multiset (Finset Unit)), a ∈ x → (fun a => Multiset.Nodup a) a) →
Multiset (Finset (Finset Unit)))
(fun l H => ↑(List.pmap Finset.mk l H)) b)
(Multiset.powerset (Finset.powerset ∅).val)).2
(_ :
∀ (_t : Multiset (Finset Unit)),
_t ∈ Multiset.powerset (Finset.powerset ∅).val → Multiset.Nodup _t) ▼
[] [2.539566s] ✅ List.insert ∅
[{∅}] =?= List.pmap Finset.mk
(Multiset.powersetAux
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset ∅.val → Multiset.Nodup _t)))
(_ :
∀ (_t : Multiset (Finset Unit)),
_t ∈ Multiset.powerset (Finset.powerset ∅).val → Multiset.Nodup _t) ▼
-/
example : (∅ : Finset Unit).powerset.powerset.image (λ p => ((∅ : Finset Unit))) = {∅} := rfl
/-
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
[13.332704s] 💥 Finset.image (fun p => ∅) (Finset.powerset (Finset.powerset ∅)) = {∅} =?= ?m.467830 = ?m.467830 ▼
[] [0.000013s] ✅ Finset (Finset Unit) =?= ?m.467829 ▶
[] [0.000018s] ✅ Finset.image (fun p => ∅) (Finset.powerset (Finset.powerset ∅)) =?= ?m.467830 ▶
[] [13.332652s] 💥 {∅} =?= Finset.image (fun p => ∅) (Finset.powerset (Finset.powerset ∅)) ▼
[] [13.332633s] 💥 {∅} =?= Finset.image (fun p => ∅) (Finset.powerset (Finset.powerset ∅)) ▼
[] [13.332576s] 💥 {∅} =?= Multiset.toFinset (Multiset.map (fun p => ∅) (Finset.powerset (Finset.powerset ∅)).val) ▼
[] [13.332540s] 💥 {∅} =?= { val := Multiset.dedup (Multiset.map (fun p => ∅) (Finset.powerset (Finset.powerset ∅)).val),
nodup :=
(_ :
Multiset.Nodup
(Multiset.dedup (Multiset.map (fun p => ∅) (Finset.powerset (Finset.powerset ∅)).val))) } ▼
[] [0.000001s] ✅ Finset (Finset Unit) =?= Finset (Finset Unit)
[] [7.061364s] ✅ {∅}.val =?= Multiset.dedup (Multiset.map (fun p => ∅) (Finset.powerset (Finset.powerset ∅)).val) ▶
[] [6.271131s] 💥 {∅}.nodup =?= Multiset.toFinset.proof_1
(Multiset.map (fun p => ∅) (Finset.powerset (Finset.powerset ∅)).val) ▶
-/
Yakov Pechersky (Apr 03 2023 at 20:02):
I would think it would be fast, since it could just execute on the list level, seeing past the quotient...
Reid Barton (Apr 03 2023 at 20:16):
Interesting that it timed out while trying to defeq test two proofs
Yakov Pechersky (Apr 03 2023 at 20:21):
More specifically, here is checking the powerset rfl, comparing multiset and finset. I've avoided notation as much as possible to prevent any TC search for EmptyCollection or Singleton:
import Mathlib.Data.Finset.Powerset
set_option autoImplicit false
set_option profiler true
set_option trace.Meta.isDefEq true
example : (∅ : Finset Unit).powerset = {∅} := rfl
/-
[0.034324s] ✅ Finset.powerset ∅ = {∅} =?= ?m.230 = ?m.230
-/
example : (Multiset.zero : Multiset Unit).powerset.powerset =
(Multiset.cons Multiset.zero (Multiset.cons (Multiset.cons Multiset.zero Multiset.zero) Multiset.zero) : Multiset (Multiset (Multiset Unit))) := rfl
/-
[0.497044s] ✅ Multiset.powerset (Multiset.powerset Multiset.zero) =
Multiset.powerset
(Multiset.powerset
Multiset.zero) =?= Multiset.powerset (Multiset.powerset Multiset.zero) =
Multiset.zero ::ₘ (Multiset.zero ::ₘ Multiset.zero) ::ₘ Multiset.zero
-/
example : (Finset.empty : Finset Unit).powerset.powerset =
(Finset.cons Finset.empty (Finset.cons (Finset.cons Finset.empty Finset.empty sorry) Finset.empty sorry) sorry : Finset (Finset (Finset Unit))) := by
ext
simp [show (Finset.empty : Finset Unit) = ∅ from rfl, show (Finset.empty : Finset (Finset Unit)) = ∅ from rfl, show (Finset.empty : Finset (Finset (Finset Unit))) = ∅ from rfl]
example : (Finset.empty : Finset Unit).powerset.powerset =
(Finset.cons Finset.empty (Finset.cons (Finset.cons Finset.empty Finset.empty sorry) Finset.empty sorry) sorry : Finset (Finset (Finset Unit))) := rfl
/-
[3.660799s] ✅ Finset.powerset (Finset.powerset Finset.empty) =
Finset.cons Finset.empty
(Finset.cons (Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty)) Finset.empty
(_ : ¬Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty) ∈ Finset.empty))
(_ :
¬Finset.empty ∈
Finset.cons (Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty)) Finset.empty
(_ :
¬Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty) ∈
Finset.empty)) =?= ?m.4628 = ?m.4628
-/
Yakov Pechersky (Apr 03 2023 at 20:22):
Is it trying to defeq the proof terms themselves?
Yakov Pechersky (Apr 03 2023 at 20:23):
[] [1.802547s] ✅ List.pmap Finset.mk
(Multiset.powersetAux
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val → Multiset.Nodup _t)))
(_ :
∀ (_t : Multiset (Finset Unit)),
_t ∈ Multiset.powerset (Finset.powerset Finset.empty).val →
Multiset.Nodup
_t) =?= [Finset.empty,
Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty)] ▼
[] [0.277031s] ✅ {
val :=
↑(List.foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0 (Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[0],
nodup :=
(_ :
(fun a => Multiset.Nodup a)
↑(List.foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0 (Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[0]) } ::
List.pmap Finset.mk
(List.map Multiset.ofList
[(List.foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0 (Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[1]])
(_ :
∀ (x : Multiset (Finset Unit)),
x ∈
List.map Multiset.ofList
[(List.foldr
(fun a arr =>
Array.foldl
(fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0
(Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[1]] →
(fun a => Multiset.Nodup a)
x) =?= [Finset.empty,
Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty)] ▶
Yakov Pechersky (Apr 03 2023 at 20:24):
I can't find what's taking the 1.6 unaccounted for seconds there
Sebastian Ullrich (Apr 03 2023 at 20:29):
For what it's worth, https://github.com/leanprover/lean4/pull/2181 should be helpful with such performance investigations in the future
Matthew Ballard (Apr 03 2023 at 20:31):
Yakov Pechersky said:
I can't find what's taking the 1.6 unaccounted for seconds there
Is that the only node nested below List.pmap Finset.mk?
Sebastian Ullrich (Apr 03 2023 at 20:38):
There may be hidden TC nodes, try synthInstance as well
Matthew Ballard (Apr 03 2023 at 21:03):
import took 211ms
elaboration took 519ms
elaboration took 4.11s
cumulative profiling times:
attribute application 0.00429ms
compilation new 0.0254ms
elaboration 4.66s
import 211ms
initialization 13.7ms
interpretation 1.37s
linting 0.349ms
parsing 1.04ms
simp 7.04ms
tactic execution 1.24ms
type checking 11ms
typeclass inference 6.35ms
I dumped the output to a file output.txt. Have to go to dinner now.
Yakov Pechersky (Apr 03 2023 at 21:03):
There's not subnodes between the 1.9s and 0.2:
[] [1.926125s] ✅ List.pmap Finset.mk
(Multiset.powersetAux
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val → Multiset.Nodup _t)))
(_ :
∀ (_t : Multiset (Finset Unit)),
_t ∈ Multiset.powerset (Finset.powerset Finset.empty).val →
Multiset.Nodup
_t) =?= [Finset.empty,
Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty)] ▼
[] [0.294699s] ✅ {
val :=
↑(List.foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0 (Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[0],
nodup :=
(_ :
(fun a => Multiset.Nodup a)
↑(List.foldr
(fun a arr =>
Array.foldl
(fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0
(Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[0]) } ::
List.pmap Finset.mk
(List.map Multiset.ofList
[(List.foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0 (Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[1]])
(_ :
∀ (x : Multiset (Finset Unit)),
x ∈
List.map Multiset.ofList
[(List.foldr
(fun a arr =>
Array.foldl
(fun r l => Array.push (Array.push r l) (a :: l))
(Array.mkEmpty (Array.size arr * 2)) arr 0
(Array.size arr))
#[[]]
(List.pmap Finset.mk (Multiset.powersetAux [])
(_ :
∀ (_t : Multiset Unit),
_t ∈ Multiset.powerset Finset.empty.val →
Multiset.Nodup _t)))[1]] →
(fun a => Multiset.Nodup a)
x) =?= [Finset.empty,
Finset.cons Finset.empty Finset.empty (_ : ¬Finset.empty ∈ Finset.empty)] ▶
Yakov Pechersky (Apr 03 2023 at 22:00):
What's the right way to switch my lean version to try trace.profiler?
Yakov Pechersky (Apr 03 2023 at 22:01):
because the flamegraph is boring otherwise:
image.png
Yakov Pechersky (Apr 11 2023 at 18:42):
I think this is also rearing its head even in tactic proofs. In here:
import Mathlib.Data.Finset.Powerset
import Mathlib.Algebra.BigOperators.Basic
open Finset
lemma foo : Finset.sum (range 4)
(λ n => card ((range 3).powerset.powerset.filter (λ s => s.card = n))) = 0 := by
rewrite [range_succ]
rewrite [sum_insert] -- slooow
Yakov Pechersky (Apr 11 2023 at 18:42):
I'm using rewrite to try to avoid rfl at the end of rw, still
Yakov Pechersky (Apr 11 2023 at 22:05):
Fewer imports:
simp took 29.8s
Yakov Pechersky (Apr 11 2023 at 22:05):
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.Basic
set_option autoImplicit false
set_option profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option maxHeartbeats 0 in
set_option synthInstance.maxHeartbeats 0 in
lemma foo : ⟨∅, Finset.empty_mem_powerset (Finset.range 2)⟩ ∈
(Finset.univ : Finset ((Finset.range 2).powerset)).filter (λ t => t.1.card = 1) := by
simp only
Yakov Pechersky (Apr 11 2023 at 22:06):
I know the statement is false, but I'm not sure why simp only would take so long. It times out on range 3
Yakov Pechersky (Apr 11 2023 at 22:10):
Even (config := {decide := false}) is slow
Yakov Pechersky (Apr 14 2023 at 11:39):
I think (config := { etaStruct := .none }) speeds it up a bit
Yakov Pechersky (Apr 14 2023 at 11:55):
But still:
[Meta.isDefEq] [8.192934s] ❌ Finset.univ =?= Finset.univ ▶
[Meta.Tactic.simp.unify] @Fintype.univ_ofSubsingleton:1000, failed to unify
Finset.univ
with
Finset.univ
[Meta.isDefEq] [8.263717s] ❌ Finset.univ =?= Finset.univ ▶
[Meta.Tactic.simp.unify] @Fintype.univ_of_isEmpty:1000, failed to unify
Finset.univ
with
Finset.univ
Yakov Pechersky (Apr 14 2023 at 11:59):
That's in this context:
[Meta.Tactic.simp.discharge] @Finset.univ_unique, failed to synthesize instance
Unique { x // x ∈ Finset.powerset (Finset.range 2) }
[Meta.isDefEq] [8.661934s] ❌ Finset.univ =?= Finset.univ ▶
[Meta.Tactic.simp.unify] @Fintype.univ_ofSubsingleton:1000, failed to unify
Finset.univ
with
Finset.univ
[Meta.isDefEq] [7.900318s] ❌ Finset.univ =?= Finset.univ ▶
[Meta.Tactic.simp.unify] @Fintype.univ_of_isEmpty:1000, failed to unify
Finset.univ
with
Finset.univ
Scratch.lean:13:58
Yakov Pechersky (Apr 14 2023 at 11:59):
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Fintype.Basic
set_option autoImplicit false
set_option profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option trace.Meta.Tactic.simp true in
set_option maxHeartbeats 0 in
set_option synthInstance.maxHeartbeats 0 in
lemma foo : ⟨∅, Finset.empty_mem_powerset (Finset.range 2)⟩ ∈
(Finset.univ : Finset ((Finset.range 2).powerset)) := by
simp (config := {
maxSteps := 100
maxDischargeDepth := 1
contextual := false
memoize := false
singlePass := false
zeta := false
beta := false
eta := false
etaStruct := .none
iota := false
proj := false
decide := false
arith := false
autoUnfold := false
dsimp := false
}) [-Finset.mem_univ, -Finset.mem_attach, -Finset.univ_eq_attach]
_
Yakov Pechersky (Apr 14 2023 at 12:01):
However, just a #synth takes < 0.002 s:
set_option profiler true in
set_option trace.Meta.synthInstance true in
set_option trace.Meta.isDefEq true in
set_option trace.Meta.Tactic.simp true in
set_option maxHeartbeats 0 in
set_option synthInstance.maxHeartbeats 0 in
#synth Unique { x // x ∈ Finset.powerset (Finset.range 2) }
Yakov Pechersky (Apr 14 2023 at 12:05):
Ah, the Unique thing is fast anyway. It's about Subsingleton and IsEmpty checks
Kevin Buzzard (Apr 14 2023 at 12:58):
Can you make this fast yet?
import Mathlib.Data.Finset.Powerset
import Mathlib.Algebra.BigOperators.Basic
open Finset
set_option profiler true in
example : (Finset.sum (insert 3 (range 3)) fun n => card (filter (fun s => card s = n) (powerset (powerset (range 3))))) = 0 := by
rw [sum_insert] -- type checking takes 7 seconds on my machine
-- and running it several times causes a stack overflow on my machine
-- (or sometimes causes it to hang)
sorry
sorry
Bhavik Mehta (Sep 22 2023 at 14:26):
Bump on this - this issue shows up for me fairly often, and it's one of the reasons I need to continue using Lean 3 - do we have a fix yet?
Kevin Buzzard (Sep 22 2023 at 14:30):
Do we have a minimised example? Is there a github issue yet? Is it covered by any of the other slowness issues which have been opened recently? I'd like to get up to speed on this one, I can't remember the details of it any more.
Bhavik Mehta (Sep 22 2023 at 14:33):
Not that I know of unfortunately, I was hoping you'd remember!
Mauricio Collares (Sep 22 2023 at 16:42):
Data/Multiset/Powerset.lean starts with a suspicious TODO:
--Porting note: TODO: Write a more efficient version
/-- A helper function for the powerset of a multiset. Given a list `l`, returns a list
of sublists of `l` as multisets. -/
def powersetAux (l : List α) : List (Multiset α) :=
(sublists l).map (↑)
#align multiset.powerset_aux Multiset.powersetAux
Mauricio Collares (Sep 22 2023 at 18:12):
I replaced the powersetAux version by a hacky port of the mathlib3 one and it seems to have fixed the timeout. It's at branch#collares/redefine-powersetAux. I'm not sure what to do with the mathlib3 version of sublistsAux (sublistsAux₃ in my branch), and there's a theorem sorried out. Help is very much welcome!
Mauricio Collares (Sep 23 2023 at 11:43):
What's interesting is that #reduce (@Fintype.card (Finpartition (∅ : Finset Unit)) (Finpartition.fintype_finset _)) (inserted after this thread's original example) runs really fast, even with the current definition of powersetAux.
Mauricio Collares (Sep 23 2023 at 12:11):
(deleted)
Mauricio Collares (Sep 23 2023 at 14:19):
Cargo-culting #7232 to std4 seems to fix the timeouts. PR at std4#271.
EDIT: Turns out it didn't, sorry for the noise. See below.
Mauricio Collares (Sep 23 2023 at 17:25):
(deleted)
Mauricio Collares (Sep 24 2023 at 06:37):
As pointed out by @Eric Rodriguez last week in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/decide.20regression/near/391860857, the slow instance in Std (docs#List.decidableBAll) is duplicated in mathlib4 (docs#List.decidableBall). The mathlib4 version is fast because it contains the workaround to lean4#2552 by @Eric Rodriguez and @Bhavik Mehta introduced in #7232; this means disabling the Std instance via attribute [-instance] List.decidableBAll suffices to make the examples in this thread run fast.
Mauricio Collares (Sep 24 2023 at 06:42):
Wait, apparently it doesn't. How is that possible?
Kevin Buzzard (Sep 24 2023 at 06:42):
Because Bhavik is very good at finding subtle issues (actually Yakov found this one but Bhavik is very good at using these sorts of things in his projects)
Mauricio Collares (Sep 24 2023 at 06:58):
This is undoubtedly true, but it also turned out I made a pretty embarrassing testing mistake by not fully reverting the changes I made while testing branch#collares/redefine-powersetAux and they were responsible for the speedup after all, unfortunately. I'll close the Std4 PR.
Mauricio Collares (Sep 26 2023 at 19:40):
Okay, let's see if I didn't mess up this time: #7388
Mauricio Collares (Sep 27 2023 at 16:50):
I just noticed something really funny about the original example. Suppose we have the original instance, that is,
import Mathlib.Order.Partition.Finpartition
open Finset
instance Finpartition.fintype_finset
{α : Type _} [DecidableEq α] (a : Finset α) : Fintype (Finpartition a) where
elems := a.powerset.powerset.image
(λ p => if h : p.SupIndep id ∧ p.sup id = a ∧ ⊥ ∉ p then ⟨p, h.1, h.2.1, h.2.2⟩ else ⊥)
complete := by
rintro p
rw [mem_image]
refine' ⟨p.parts, _, _⟩
· simp only [mem_powerset]
intros i hi
rw [mem_powerset]
exact p.le hi
· rw [dif_pos]
simp only [p.supIndep, p.supParts, p.not_bot_mem, eq_self_iff_true, not_false_iff, and_self]
Now consider the following two snippets:
1) example : @Fintype.card (Finpartition (∅ : Finset Unit)) (Finpartition.fintype_finset _) = 1 := by rfl.
2) example : @Fintype.card (Finpartition (∅ : Finset Unit)) (Finpartition.fintype_finset _) = 1 := rfl.
As reported by count_heartbeats, the first one uses 650 heartbeats and the second one uses 4865061 (!) heartbeats on master. After #7388, the first one uses 486 heartbeats and the second uses 3094. I really suspect that I'm doing something wrong, but I've tested a few times and it seems consistent.
Edit: As a corollary, make sure to use by rfl and not rfl if you're trying the @Fintype.card (Finpartition (range 3)) (Finpartition.fintype_finset _) = 5 original example with #7388!
Eric Rodriguez (Sep 27 2023 at 17:01):
Can this be done mathlibless?
Bhavik Mehta (Sep 27 2023 at 21:58):
Mauricio Collares said:
I just noticed something really funny about the original example. Suppose we have the original instance, that is,
import Mathlib.Order.Partition.Finpartition open Finset instance Finpartition.fintype_finset {α : Type _} [DecidableEq α] (a : Finset α) : Fintype (Finpartition a) where elems := a.powerset.powerset.image (λ p => if h : p.SupIndep id ∧ p.sup id = a ∧ ⊥ ∉ p then ⟨p, h.1, h.2.1, h.2.2⟩ else ⊥) complete := by rintro p rw [mem_image] refine' ⟨p.parts, _, _⟩ · simp only [mem_powerset] intros i hi rw [mem_powerset] exact p.le hi · rw [dif_pos] simp only [p.supIndep, p.supParts, p.not_bot_mem, eq_self_iff_true, not_false_iff, and_self]Now consider the following two snippets:
1)
example : @Fintype.card (Finpartition (∅ : Finset Unit)) (Finpartition.fintype_finset _) = 1 := by rfl.
2)example : @Fintype.card (Finpartition (∅ : Finset Unit)) (Finpartition.fintype_finset _) = 1 := rfl.As reported by
count_heartbeats, the first one uses 650 heartbeats and the second one uses 4865061 (!) heartbeats on master. After #7388, the first one uses 486 heartbeats and the second uses 3094. I really suspect that I'm doing something wrong, but I've tested a few times and it seems consistent.Edit: As a corollary, make sure to use
by rfland notrflif you're trying the@Fintype.card (Finpartition (range 3)) (Finpartition.fintype_finset _) = 5original example with #7388!
Woah! I'd seen examples where rfl and by rfl were different but never this different! Nice find
Kevin Buzzard (Sep 27 2023 at 23:11):
Note Sebastian's comment about this phenomenon here.
Mauricio Collares (Oct 09 2023 at 13:35):
Modulo bumping macRecDepth, the by rfl/rfl discrepancy was fixed in 9f50f44. Thank you Leo and Sebastian!
Eric Wieser (Oct 22 2023 at 10:18):
In the latest master, this now works (but is still slow):
set_option maxRecDepth 1500 in
example : @Fintype.card (Finpartition (univ : Finset (Fin 3))) (Finpartition.fintype_finset _) = 5 := rfl
Mauricio Collares (Oct 22 2023 at 10:19):
(and no need for the maxRecDepth bump if you use by rfl instead)
Last updated: Dec 20 2023 at 11:08 UTC