Defining a Finpartition from a Setoid over a Fintype

Stream: mathlib4

[Jeremy Tan]

How can I do this?

import Mathlib.Data.Setoid.Partition

open Finset

universe u

variable {V : Type u} [Fintype V] [DecidableEq V]

def notAdjFinpartition (s : Setoid V) : Finpartition (univ : Finset V) :=
  sorry

[Jeremy Tan]

The motivationn is Turán's theorem and my proof through "Zykov symmetrisation". I've got to the point where I have the Setoid over vertices with non-adjacency as the relation: Turan.lean
Now my plan is to get a Finpartition from the Setoid, prove this is an Equipartition and finally prove the theorem as an isomorphism between any maximal graph and the relevant Turán graph. But the needed conversions from Set to Finset are stumping me

[Yaël Dillies]

Sorry, don't have time to write my thoughts, but it should be as easy as making parts be univ.image fun a ↦ univ.filter (s a).

[Jeremy Tan]

s a doesn't make sense when s is a Setoid

[Jeremy Tan]

You probably meant univ.image fun a => univ.filter <| (notAdjSetoid hmax).r a for parts but then I get failed to synthesize instance DecidablePred fun x ↦ Setoid.r a x

[Jeremy Tan]

OK, this works, but how do I get the remaining three fields?

noncomputable def notAdjFinpartition : Finpartition (univ : Finset V) where
  parts := by classical
    exact univ.image fun a => univ.filter <| (notAdjSetoid hmax).r a
  supIndep := by simp
  supParts := by simp
  not_bot_mem := by simp

[Yaël Dillies]

not_bot_mem comes from the fact that univ.filter <| (notAdjSetoid hmax).r a is nonempty since it contains a.

[Yaël Dillies]

supParts should be pretty obvious too (a ∈ univ.filter <| (notAdjSetoid hmax).r a).

[Yaël Dillies]

Finally supIndep is a bit harder, but if you've done the first two it should be pretty obvious (hint: (notAdjSetoid hmax).r is transitive).

[Jeremy Tan]

OK, this was a pain

import Mathlib.Data.Setoid.Partition

open Finset Setoid

universe u

variable {V : Type u} [Fintype V] [DecidableEq V]

noncomputable def finpartition_ofSetoid (s : Setoid V) : Finpartition (univ : Finset V) where
  parts := by classical exact univ.image fun a => univ.filter (s.r a)
  supIndep := by classical
    simp only [mem_univ, forall_true_left, supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint,
      Set.Pairwise, coe_image, coe_univ, Set.image_univ, Set.mem_range, ne_eq, forall_exists_index,
      forall_apply_eq_imp_iff]
    intro a b q
    contrapose! q
    rw [not_disjoint_iff] at q
    obtain ⟨c, ⟨d1, d2⟩⟩ := q
    rw [id_eq, mem_filter] at d1 d2
    ext y
    simp only [mem_univ, forall_true_left, mem_filter, true_and]
    exact ⟨fun r1 => s.iseqv.trans (s.iseqv.trans d2.2 (s.iseqv.symm d1.2)) r1,
           fun r2 => s.iseqv.trans (s.iseqv.trans d1.2 (s.iseqv.symm d2.2)) r2⟩
  supParts := by classical
    ext a
    simp only [sup_image, Function.comp.left_id, mem_univ, mem_sup, mem_filter, true_and, iff_true]
    use a; exact s.iseqv.refl a
  not_bot_mem := by classical
    rw [bot_eq_empty, mem_image, not_exists]
    intro a
    simp only [filter_eq_empty_iff, not_forall, mem_univ, forall_true_left, true_and, not_not]
    use a; exact s.iseqv.refl a

[Jeremy Tan]

Now that I have the Finpartition of univ : Finset V, given a : V is there a neat expression to get the part a lies in?

[Yakov Pechersky]

I suggest looking at a lot of Finpartition API built here:
https://github.com/leanprover-community/mathlib4/compare/master...aluffi#diff-b1ded7d3cd173a640508811049587f4fe2fde9d282a73fd6e0d7c51f4b710ad4

Like this:

lemma eq_of_mem_of_mem {s : Finset α} {P : Finpartition s} {x y : Finset α} (hx : x ∈ P.parts)
    (hy : y ∈ P.parts) {a : α} (hxa : a ∈ x) (hya : a ∈ y) : x = y := by
  have := P.supIndep (singleton_subset_iff.mpr hx) hy
  by_contra H
  simp only [mem_singleton, id_eq, sup_singleton] at this
  simpa using this (Ne.symm H) (singleton_subset_iff.mpr hya) (singleton_subset_iff.mpr hxa)

theorem exists_unique_mem {a : α} {s : Finset α} (P : Finpartition s) (ha : a ∈ s) :
    ∃! t, t ∈ P.parts ∧ a ∈ t := by
  obtain ⟨t, ht, ht'⟩ := P.exists_mem ha
  refine' ⟨t, ⟨ht, ht'⟩, _⟩
  rintro u ⟨hu, hu'⟩
  exact eq_of_mem_of_mem hu ht hu' ht'

[Jeremy Tan]

This is now at #8735. Still not sure what's the best way to link the Setoid and the Finpartition derived from it – I want something that directly equates the Setoid's equivalence classes and the Finpartition's parts

[Jeremy Tan]

But getting past the (computable) Finset.choose in my definition of Finpartition.part is the big obstacle. There appears to be no API around it

[Yakov Pechersky]

How does the equiv between the two work in my branch? I don't recall.

[Jeremy Tan]

OK, here's what's going on right now. I have a non-adjacency setoid over the graph vertices and a Finpartition derived from it using my old ofSetoid:

variable {G} (hmax : G.IsTuranMaximal r)

theorem notAdjEquivalence : Equivalence fun x y => ¬G.Adj x y where
  refl x := by simp
  symm xy := by simp [xy, adj_comm]
  trans xy yz := by
    rw [adj_comm] at xy
    exact G.not_adj_transitive hmax xy yz

/-- In a Turán-maximal graph, non-adjacency is an equivalence relation. -/
def notAdjSetoid : Setoid V := Setoid.mk _ (notAdjEquivalence hmax)

noncomputable def notAdjFinpartition : Finpartition (univ : Finset V) :=
  Finpartition.ofSetoid (notAdjSetoid hmax)

Now I want to prove this theorem:

theorem xxx : G.degree s = Fintype.card V -
    ((notAdjFinpartition hmax).part (a := s) (mem_univ _)).card := by
  calc
    G.degree s = (univ.filter (fun b => G.Adj s b)).card := by
      simp [← card_neighborFinset_eq_degree, neighborFinset]
    _ = Fintype.card V - (univ.filter (fun b => ¬G.Adj s b)).card :=
      eq_tsub_of_add_eq (filter_card_add_filter_neg_card_eq_card _)
    _ = _ := by
      congr
      ext v
      simp -- stuck here

The goal state after the simp is ¬Adj G s v ↔ v ∈ Finpartition.part (notAdjFinpartition hmax) _

[Jeremy Tan]

Your equiv (that I have just added to #8735 as Finpartition.equivSubtypeSetoidIsPartition) does not work as a drop-in substitute!

noncomputable def notAdjFinpartition : Finpartition (univ : Finset V) :=
  (Finpartition.equivSubtypeSetoidIsPartition V).symm ⟨(notAdjSetoid hmax).classes, ...⟩

application type mismatch
  Subtype.mk (Setoid.classes (notAdjSetoid hmax))
argument
  Setoid.classes (notAdjSetoid hmax)
has type
  Set (Set V) : Type u
but is expected to have type
  Finset (Set V) : Type u

However am I going to synth the instance Fintype ↑(Setoid.classes (notAdjSetoid hmax))?

[Jeremy Tan]

If I can get this theorem that would directly complete the proof of xxx

theorem mem_part_iff_rel (s : Setoid α) (b : α) :
    b ∈ (ofSetoid s).part (mem_univ a) ↔ s.r a b := sorry

[Yakov Pechersky]

proved