Compute `card (Setoid S)`

Stream: new members

[Han Han]

Hi everyone,
I'm working on proving that Nat.card (Setoid S) > Nat.card (Set S) for a set S with 5 elements.I used Setoid.Partition.orderIso to transform the problem as computing Nat.card { C : Set (Set S) // Setoid.IsPartition C }. However, I'm not sure if there is a direct way to compute this cardinality or if an alternative approach might be more suitable.
Could someone offer guidance or suggestions on how to proceed? Thank you!

import Mathlib
theorem gt' {S : Type} (hS : Nat.card S = 5) : Nat.card (Setoid S) > Nat.card (Set S) := by
  rw [Nat.card_congr (Setoid.Partition.orderIso S).toEquiv]
  have : Nat.card { C : Set (Set S) // Setoid.IsPartition C } = 52 := by
    sorry

[Aaron Liu]

You could derive a Fintype (Setoid S) and then just compute it

[Han Han]

Okay. Now I have already derived Fintype (Setoid S), but I'm still not sure how to compute the corresponding cardinality.

import Mathlib
theorem gt' {S : Type} (hS : Nat.card S = 5) :
    Nat.card (Setoid S) > Nat.card (Set S) := by
  let _ : Finite S := Nat.finite_of_card_ne_zero (by rw [hS] ; norm_num)
  let _ : Fintype S := Fintype.ofFinite S
  let _ : Finite (Setoid S) := by
    rw [Equiv.finite_iff ((Setoid.Partition.orderIso S).toEquiv)]
    exact Subtype.finite
  let _ : Fintype (Setoid S) := Fintype.ofFinite (Setoid S)
  rw [Nat.card_eq_fintype_card]
  have : Fintype.card (Setoid S) = 52 := by sorry
  sorry

[Aaron Liu]

decide should work, and if it doesn't then decide +kernel should either work or time out.

[Aaron Liu]

If you get the Fintype from Fintype.ofFinite then it's not going to work

[Aaron Liu]

The whole point of using Fintype is so you can compute with it

[Aaron Liu]

Try using a Subtype instance and then transferring across the bijection

[Han Han]

Thanks for your guidance, but I'm now stuck trying to prove that the subtype is a fintype without using Fintype.ofFinite. Could someone please provide further assistance?

import Mathlib
theorem gt' {S : Type} (hS : Nat.card S = 5) :
    Nat.card (Setoid S) > Nat.card (Set S) := by
  rw [Nat.card_congr (Setoid.Partition.orderIso S).toEquiv]
  let this : Fintype { C : Set (Set S) // Setoid.IsPartition C } := by
      sorry
  have : Fintype.card { C : Set (Set S) // Setoid.IsPartition C } = 52 := by sorry

[Aaron Liu]

So it turns out you basically can't extract any information out of a Set computably

[Aaron Liu]

Hmmm

[Aaron Liu]

It would probably be best to do this on Finsets of a concrete type like Fin 5

[Aaron Liu]

And then transfer this using Equivs

[Kyle Miller]

(Edit: I misread this morning; I thought it was comparing to Nat.card S, not Nat.card (Set S). Very different.)

For 5 elements, maybe it's not so bad exhibiting 6 equivalence relations: the partitions could be {{1,2,3,4,5}}, {{2,3,4,5},{1}}, {{1,3,4,5},{2}}, {{1,2,4,5},{3}}, {{1,2,3,5},{4}}, {{1,2,3,4},{5}}.

This seems reasonably generalizable to n elements too.

[Eric Wieser]

#16647 is some work in this direction

[Han Han]

Aaron Liu said:

It would probably be best to do this on Finsets of a concrete type like Fin 5

Thank you for your advice. However, I'm not very familiar with the Fintype API. Even with a concrete case like Fin 5, I'm unsure how to begin proving that the subtype is a Fintype. Could you provide more guidance or an example on how to establish this?

import Mathlib

lemma gt_Fin5 : Nat.card (Setoid (Fin 5)) > Nat.card (Set (Fin 5)) := by
  let _ : Fintype (Fin 5) := Fin.fintype 5
  have : Fintype { C : Set (Set (Fin 5)) // Setoid.IsPartition C } := by
    apply Fintype.mk sorry
    sorry
  sorry

[Aaron Liu]

I tried that, but it turns out O(2^2^x) blows up even for small inputs. It would actually probably be best to prove the formula for bell numbers.

[Han Han]

Okay. Now I understand the direct computation can be heavy, but I still want to learn how to prove a Subtype is a Fintype, even if it's slow. Could you please show your proof?

[Han Han]

Eric Wieser said:

#16647 is some work in this direction

Thanks! This would be very useful.

[Ruben Van de Velde]

Maybe

@loogle Subtype, Fintype

[loogle]

:search: Fintype.subtype, Finset.subtype_univ, and 557 more

[Aaron Liu]

Han Han said:

Okay. Now I understand the direct computation can be heavy, but I still want to learn how to prove a Subtype is a Fintype, even if it's slow. Could you please show your proof?

I can't find it :(

[Aaron Liu]

I think I showed that Decidable (Setoid.IsPartition (Finset.toSet '' s.toSet)) and then mapped along a map that I had to show was injective and its image is all setoids.

[Han Han]

I don't quite get the point. What is s in this context? I guess it's some Finset, but I'm not sure which one should be used here.

[Aaron Liu]

Han Han said:

I don't quite get the point. What is s in this context? I guess it's some Finset, but I'm not sure which one should be used here.

It's forall s

[Aaron Liu]

Which has type Finset (Finset X)

[Han Han]

Okay. Now I understand what are you talking about:

import Mathlib
theorem gt' {S : Type*} (hS : Nat.card S = 5) :
    Nat.card (Setoid S) > Nat.card (Set S) := by
  have : ∀ s : Finset (Finset S),
    Decidable (Setoid.IsPartition (Finset.toSet '' s.toSet)) := sorry
  have hequiv :
    { s : Finset (Finset S) // Setoid.IsPartition (Finset.toSet '' s.toSet) }
    ≃ Setoid S := by sorry
  sorry

I will try to complete this proof.

[Aaron Liu]

Once you complete it it might take several hours or days to typecheck

[Aaron Liu]

That's why I discarded my code

[Eric Wieser]

I think you'd do better to generalize straight to the general case, rather than card S = 5

[Han Han]

Thanks for the advice. Here are my current goals:

import Mathlib
variable {S : Type*} [Fintype S]

instance (s : Finset (Finset S)) : Decidable (Setoid.IsPartition (Finset.toSet '' s.toSet)) := by sorry

def Setoid.equiv :
    Setoid S ≃ { s : Finset (Finset S) // Setoid.IsPartition (Finset.toSet '' s.toSet) } := by sorry

I will work on completing these two generalized versions.

[Aaron Liu]

I think it would be better to prove a formula for bell numbers if your goal is to solve Nat.card (Set S) < Nat.card (Setoid S)

[Han Han]

Well. You are right. I just want to learn more about Fintype or Decidable by working on this. I will also try to use bell formula to solve the original problem.

[Han Han]

After several attempts, I found the typechecking of the previous code quite annoying. However, I discovered that Finpartition.instFintypeFinset shows that (Finpartition (Finset.univ)) is a Fintype, which allows me to compute Fintype.card (Finpartition (Finset.univ)) (although it is slow). Now my question is: How can I prove that card Setoid S equals card (Finpartition (Finset.univ))? I plan to construct a bijection using Finpartition.ofSetoid, but I am stuck on proving that this map is surjective. Could someone provide some guidance on this issue?

import Mathlib

open Finpartition

variable {S : Type*} [Fintype S] [DecidableEq S]

noncomputable instance foo (s : Setoid S) : DecidableRel s.r := Classical.decRel ⇑s

lemma bijective : Function.Bijective (fun s : Setoid S ↦ Finpartition.ofSetoid s) where
  left := by
    intro x y hxy
    simp at hxy
    ext a b
    let _ : DecidableRel x.r := foo x
    let _ : DecidableRel y.r := foo y
    repeat rw [← mem_part_ofSetoid_iff_rel]
    rw [hxy]
  right := by
    intro P
    let s : Setoid S := {
      r x y := x ∈ P.part y
      iseqv := by
        constructor
        · intro x
          apply mem_part
          simp
        · intro x y hxy
          rw [mem_part_iff_part_eq_part] at hxy
          rw [hxy]
          apply mem_part
          repeat simp
        · intro x y z hxy hyz
          rw [mem_part_iff_part_eq_part] at hxy hyz
          rw [← hyz, ← hxy]
          apply mem_part
          repeat simp}
    use s
    ext t
    sorry

instance : Fintype (Finpartition (Finset.univ : Finset S)) := instFintypeFinset