instance DecidableRel (ReflTransGen r)

Stream: Is there code for X?

[Chris Wong]

Does a decidable instance for docs#ReflTransGen exist?

I see there's docs#SimpleGraph.instDecidableRelReachable for not for ReflTransGen itself.

#xy: I'm defining a quotient from a collection of subsets, as part of defining graph contraction. For induction, I'd like to prove that contraction results in a smaller graph, i.e. Fintype.card (Quotient (Setoid.fromSets S)) ≤ Fintype.card α. But that uses docs#Quotient.fintype which in turn requires that the setoid is decidable. While I can use Nat.card instead, the rest of the graph theory library uses Fintype, so I'd like to match that.

import Mathlib

open Relation

variable {α : Type*}

def Setoid.fromSets (S : Set (Set α)) : Setoid α where
  r := ReflTransGen fun a b ↦ ∃ s ∈ S, a ∈ s ∧ b ∈ s
  iseqv := {
    refl := fun a ↦ ReflTransGen.refl
    trans := ReflTransGen.trans
    symm := fun h ↦ ReflTransGen.symmetric (by tauto) h
  }

theorem Setoid.card_quotient_fromSets_le [Fintype α] (S : Set (Set α)) :
    Fintype.card (Quotient (Setoid.fromSets S)) ≤ Fintype.card α :=
  sorry

[Kyle Miller]

It's not decidable in general, but it's decidable if the type is a Fintype and the relation has the property that the sets {y | r x y} are Fintypes for each x.

You probably don't need an actual decidable instance though, even if you use Fintype.card, since you can use classical

[Chris Wong]

Yeah, I took a stab at this and got stuck. I think my problem was that ReflTransGen doesn't carry data, so I couldn't reason about the length of the path, which is how the Reachable proof works. I'll just stick with classical for now.

[Chris Wong]

BTW, docs#Fintype.card_quotient_lt is very useful!