Way ConnectedComponent definition uses Quot?

Stream: graph theory

[Iván Renison]

Hi, in the definition of Quotient it says this:

/--
`Quotient α s` is the same as `Quot α r`, but it is specialized to a setoid `s`
(that is, an equivalence relation) instead of an arbitrary relation.
Prefer `Quotient` over `Quot` if your relation is actually an equivalence relation.
-/

And ConnectedComponent is defined like this:

/-- The quotient of `V` by the `SimpleGraph.Reachable` relation gives the connected
components of a graph. -/
def ConnectedComponent := Quot G.Reachable

So I'm wandering, why not Quotient instead of Quot?
We have reachable_is_equivalence that proves that G.Reachable is a equivalence relation

[Chris Wong]

I believe @Kyle Miller had some concerns with the design of Quotient.

[Kyle Miller]

When you use Quotient API, it causes all the terms to be put in terms of Quotient.mk and Setoid.r rather than your own quotient map and your own relation. Currently there's no good way to prevent this from happening except to copy the Quotient API for your own type.

Ideally we would have some typeclass that says that a particular function is a quotient map, and then have a reusable API around that.

[Eric Wieser]

The same is true when using Quot API though, right? What makes Quotient a worse implementation detail than Quot?

[Kyle Miller]

Quot.mk is similar, sure, but that still leaves Setoid.r slipping in.

[Yaël Dillies]

Kyle Miller said:

Ideally we would have some typeclass that says that a particular function is a quotient map, and then have a reusable API around that.

There's a PR doing just that, in case you weren't aware of it: #16421

[Eric Wieser]

Should Quotient have its single Setoid argument exploded into two arguments?

[Iván Renison]

I want to prove this:

lemma reachable_of_in {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V}
    (hu : u ∈ C) (hv : v ∈ C) : G.Reachable u v := sorry

But I don't find an easy proof. I expected that there should be a lemma saying something like this:

lemma aux (r : V → V → Prop) [Membership V (Quot r)] (C : Quot r) (u v : V)
    (hu : u ∈ C) (hv : v ∈ C) : r u v := sorry

But I can find a lemma saying that and I'm not able to prove it. Do you know if that lemma is valid?

[Kyle Miller]

import Mathlib.Combinatorics.SimpleGraph.Path

-- correction of `SimpleGraph.ConnectedComponent.mem_supp_iff`
@[simp]
theorem mem_supp_iff' {G : SimpleGraph V} (C : G.ConnectedComponent) (v : V) :
    v ∈ C ↔ G.connectedComponentMk v = C :=
  Iff.rfl

lemma reachable_of_in {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V}
    (hu : u ∈ C) (hv : v ∈ C) : G.Reachable u v := by
  rw [mem_supp_iff'] at hu hv
  rw [← hv] at hu
  exact SimpleGraph.ConnectedComponent.exact hu

[Kyle Miller]

Saving a line:

lemma reachable_of_in {G : SimpleGraph V} (C : G.ConnectedComponent) {u v : V}
    (hu : u ∈ C) (hv : v ∈ C) : G.Reachable u v := by
  rw [mem_supp_iff'] at hu hv
  exact SimpleGraph.ConnectedComponent.exact (hv ▸ hu)

[Iván Renison]

Thanks!

[Bhavik Mehta]

As an aside, we don't have that in a connected graph on at least two vertices the support is the whole vertex set; this might be a nice thing to do for someone!

[Aaron Liu]

This was fun

SimpleGraph.Preconnected.support_eq_univ

import Mathlib

lemma SimpleGraph.Preconnected.support_eq_univ {V : Type*} [Nontrivial V]
    {G : SimpleGraph V} (h : G.Preconnected) : G.support = Set.univ := by
  apply Set.eq_univ_iff_forall.mpr
  intro v
  apply G.mem_support.mpr
  by_contra hv
  push_neg at hv
  obtain ⟨w, hw⟩ := exists_ne v
  have p := (SimpleGraph.reachable_iff_reflTransGen v w).mp (h v w)
  induction p with
  | refl =>
    exact hw rfl
  | tail p hadj ih =>
    rw [ne_eq, imp_false, not_not] at ih
    subst ih
    exact hv _ hadj

[Kyle Miller]

A bit shorter:

SimpleGraph.Preconnected.support_eq_univ

lemma SimpleGraph.Preconnected.support_eq_univ {V : Type*} [Nontrivial V]
    {G : SimpleGraph V} (h : G.Preconnected) : G.support = Set.univ := by
  simp_rw [Set.eq_univ_iff_forall, G.mem_support]
  intro v
  obtain ⟨w, hw⟩ := exists_ne v
  obtain ⟨p⟩ := h v w
  cases p with
  | nil => contradiction
  | @cons _ w => use w