deciding connectivity

Stream: Is there code for X?

[Noah G. Singer]

Hi, what is the easiest way to prove that a fixed finite simple graph is connected? For instance, the following complains about not being decidable:

def e1 : Sym2 (Fin 3) := Sym2.mk (0, 1)
def e2 : Sym2 (Fin 3) := Sym2.mk (1, 2)
def G := SimpleGraph.fromEdgeSet {e1, e2}

theorem X : SimpleGraph.Connected G := by
  decide

Is there code for finite graphs / relations somewhere?

[Kyle Miller]

docs#SimpleGraph.instDecidableConnected exists, though no guarantees it's anything like a good algorithm

[Kyle Miller]

If you satisfy its hypotheses, then decide might work.

[Noah G. Singer]

Oh wow, nice. I tried searching for Decidable on the SimpleGraph page itself and that didn't find anything, but I guess this is in a subpage. No worries on the good algorithm, I just need it to check that some small graph (whose edges correspond to certain lemmas) is connected :)

[Kyle Miller]

It's worth taking a look at Archive/Wiedijk100Theorems/Konigsberg.lean to see an example of a concrete graph with a computation done with it.

[Kyle Miller]

Here's a start. However, decide fails because the instances aren't written correctly.

def G_edges : List (Sym2 (Fin 3)) :=
  [s(0, 1), s(1, 2)]
def G_adj (v w : Fin 3) : Bool := s(v, w) ∈ G_edges
def G : SimpleGraph (Fin 3) where
  Adj v w := G_adj v w
  symm := by
    dsimp [Symmetric, G_adj]
    decide
  loopless := by
    dsimp [Irreflexive, G_adj]
    decide

instance : DecidableRel G.Adj := fun a b => inferInstanceAs <| Decidable (G_adj a b)

theorem X : SimpleGraph.Connected G := by
  decide
/- error
...
After unfolding the instance 'SimpleGraph.instDecidableConnected', reduction got stuck at the
'Decidable' instance
  ⋯ ▸ ⋯.mpr inferInstance
...
-/

[Kyle Miller]

It's fixable though:

open SimpleGraph in
instance : Decidable G.Connected :=
  decidable_of_iff G.Preconnected <| by
    rw [connected_iff, ← Finset.univ_nonempty_iff]
    simp

theorem X : SimpleGraph.Connected G := by
  decide

[Kyle Miller]

Would you be interested in making a mathlib PR to fix this Decidable G.Connected instance like so?

[Kyle Miller]

It needs to use decidable_of_iff rather than rewriting the type.

[Noah G. Singer]

Let me take a stab... I am new :)

[Noah G. Singer]

it's still complaining that Preconnected isn't decidable :) should I try and fix that too?

[Kyle Miller]

I think this is the replacement for the instance in Connectivity/WalkCounting.lean:

instance : Decidable G.Connected :=
  decidable_of_iff (G.Preconnected ∧ (Finset.univ : Finset V).Nonempty) <| by
    rw [connected_iff, ← Finset.univ_nonempty_iff]

[Noah G. Singer]

OK awesome yeah. I didn't realize I had to fix it in the Mathlib file directly. Can do the PR

[Noah G. Singer]

https://github.com/leanprover-community/mathlib4/pull/20013

[Noah G. Singer]

Thanks @Kyle Miller ! Fwiw, I am working with @Cayden Codel and some other folks on formalizing some group theory I have been doing recently. Hopefully we will be contributing to Mathlib some more in the future!

[Kyle Miller]

I just sent you a mathlib invite @Noah G. Singer. The CI expects every PR to originate from a branch in the mathlib project itself (I tried overriding it with some button clicking as a maintainer, but that didn't seem to work). Would you mind creating a new PR?

[Noah G. Singer]

done