Decidability for connected components

Stream: graph theory

[Jérémie Turcotte]

Hi, I'm looking at the simple_graph part of mathlib. I'd like to add a definition for the number of connected components of a graph (say, finite), and prove various basic properties (for instance what happens when removing an edge). The obvious way of defining it is with fintype.card, but for this we need to show that connected_component is a fintype before. For this, the most obvious way would be to use fintype.of_surjective for the quot.mk function. The only issue I am getting into is the decidable_eq of the quotient, or equivalently of the decidable_rel for the relation from which the quotient was defined, i.e. decidability of whether the set of u-v walks is non-empty. Is there an easy way of doing this? (Say, assuming fintype V.) Thank you very much.

[Junyan Xu]

If you know it's finite then docs#nat.card will give the same value as docs#fintype.card. If you really want to make it computable, just add [decidable_rel r] as an argument.

[Jérémie Turcotte]

I'm not exactly sure I understand. I guess I would have liked to first prove it is necessarily finite. For the second comment, the relation isn't one I'm choosing, it's already defined using walks in graphs previously, so I don't see how I could add that as an argument. Maybe I am misunderstanding something.

[Jérémie Turcotte]

Let me note that we already assume that adjacency is decidable. On a finite graph I imagine that should quite easily imply that the existence of paths between vertices is also decidable, but maybe I'm not really understanding what is going on with this decidability stuff.

[Junyan Xu]

You don't need to prove anything to use docs#nat.card; it's just that when nat.card α = 0 it could mean either α is empty or it is infinite. When α is finite, docs#nat.card_eq_fintype_card shows nat.card agrees with fintype.card (of course you need a fintype around to talk about fintype.card, but you can always get one from finiteusing docs#fintype.of_finite).

If your relation is complicated, you can still write [decidable_rel some_complicated_expression]. If you don't want to include the argument, you can also open_locale classical which automatically fill in a classical decidability instance whenever needed.

But it seems what you're really asking is to write a decidable instance that takes [decidable_rel G.adj] and [fintype V] (and presumably [decidable_eq V] as well) and outputs decidable_rel (G.reachable u v). I think you need to write down an algorithm and it's not that straightforward. The easiest way is probably to obtain the connected component of u as a finset, then check whether v belongs to it.

[Junyan Xu]

There is some code here that defines the balls around a vertex as finsets, and your task is somewhat similar.

[Junyan Xu]

Actually docs#simple_graph.finset_walk_length is already in mathlib. It shouldn't be hard to show that for length >= fintype.card V, this is the same as the connected component.

[Junyan Xu]

@Jérémie Turcotte Here is the decidable instance for you:

import combinatorics.simple_graph.connectivity

variables {V : Type*} (G : simple_graph V) [fintype V]

lemma list.nodup.length_le_card {l : list V} (h : l.nodup) : l.length ≤ fintype.card V :=
begin
  rw list.nodup_iff_nth_le_inj at h,
  let : fin l.length → V := λ n, l.nth_le n n.2,
  convert fintype.card_le_of_injective this (λ n m he, _),
  { rw fintype.card_fin },
  { ext1, exact h n m n.2 m.2 he },
end

variables [decidable_rel G.adj] [decidable_eq V]

lemma reachable_iff_mem_finset_walk_length (u v : V) :
  G.reachable u v ↔ ∃ n : fin (fintype.card V), (G.finset_walk_length n u v).nonempty :=
begin
  split,
  { rintro ⟨p⟩,
    refine ⟨⟨p.bypass.length, _⟩, p.bypass, _⟩,
    { have := p.bypass_is_path.support_nodup.length_le_card,
      rw p.bypass.length_support at this, exact this },
    { -- why is length_eq_of_mem_finset_walk_length not an iff?
      rw [← finset.mem_coe, simple_graph.coe_finset_walk_length_eq],
      congr /- refl doesn't work! -/ } },
  { rintro ⟨_, p, _⟩, use p },
end

instance (u v : V) : decidable (G.reachable u v) :=
decidable_of_iff' _ (reachable_iff_mem_finset_walk_length G u v)

[Kyle Miller]

@Junyan Xu I'll make a PR for length_eq_of_mem_finset_walk_length.

Regarding refl not working -- the refl tactic doesn't see that the target is an eq after unfolding the has_mem.mem. You can use exact rfl instead of congr.

[Kyle Miller]

#17148 has these (added you as a coauthor @Junyan Xu, and I hope going ahead and creating this PR without checking what you'd done already is more helpful than not @Jérémie Turcotte)