Zulip Chat Archive

Stream: graph theory

Topic: Decidability for connected components

Jérémie Turcotte (Oct 19 2022 at 02:31):

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 (Oct 19 2022 at 02:36):

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 (Oct 19 2022 at 02:43):

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 (Oct 19 2022 at 02:52):

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 (Oct 19 2022 at 03:02):

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 (Oct 19 2022 at 03:08):

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

Junyan Xu (Oct 19 2022 at 03:15):

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 (Oct 19 2022 at 04:17):

@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 :=
  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 },

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 :=
  { 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 },

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

Kyle Miller (Oct 25 2022 at 07:52):

@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 (Oct 25 2022 at 10:10):

#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)

Last updated: Dec 20 2023 at 11:08 UTC