Graph theory and Kruskal's algorithm

Stream: general

[Ayush Priyadarshi]

I wanted to convert a Finset of edges to a List
How can I do that
This is a part of implementation of the Kruskal's Algorithm in Lean

/-- A weight function on the edges of a simple graph assigns a natural number
    to each edge `(u, v)` with a proof that they are adjacent. -/
def EdgeWeight := ∀ {u v : V}, G.Adj u v → ℕ

/-- A weight function on the edges of a simple graph assigns a natural number
    to each edge `e` with a proof that `e` is in the edge set. -/
def EdgeWeight' := ∀ { e : Sym2 V}, e ∈ G.edgeSet → ℕ

Above is how I defined a weight function on a graph.
Basically I can a computable function which takes either Vertex set or edgeset as an input and returns a List (in sym2 V) as an output.

[Johannes Tantow]

docs#Finset.toList. This uses the axiom of choice though, but this is probably not possible without it. If your type is linearly ordered, you can always take the smallest/largest out of it.

[Johannes Tantow]

Do you want to use Kruskal in practice or only prove something about that

[Kim Morrison]

(Note Finset is defined in Mathlib, so this is the wrong channel for this question.)

[Ayush Priyadarshi]

I am implementing the Kruskal's algorithm algorithmically.
In one of the parts as I am computing a MST(minimum spanning tree) for a graph.
but for obtaining the minimum weight of an edge , I will either use a sort function or a Min function both of which I have created.
But for that I need to define a linear order on this set.
How do I do that?
About this question
Do you want to use Kruskal in practice or only prove something about that
I am implementing it in practice and proving it's optimality.

[Notification Bot]

This topic was moved here from #batteries > Graph theory and Kruskal's algorithm by Kim Morrison.

[Kim Morrison]

@Ayush Priyadarshi, note I have moved this thread, as it did not belong in the batteries channel.

[Ayush Priyadarshi]

I want to convert G.edgeset to a List
And then use this function below to give me an edge of minimum weight.

def List.minBy? (l : List α) (f : α → Nat) : Option α :=
  match l with
  | [] => none
  | x :: xs =>
    match xs.minBy? f with
    | none => some x
    | some y =>
      if f x < f y then
        some x
      else
        some y

def myWeightFn : String → Nat
  | "alpha" => 1
  | "beta" => 2
  | "gamma" => 3
  | "delta" => 1
  | _ => 100  -- fallback for unmatched strings

#eval List.minBy? ["alpha", "beta", "gamma", "delta"] myWeightFn -- some "delta"

[Johannes Tantow]

I wouldn't store the graph as a finset then. In practice the graph will be ordered as the input in some way anyway. You could use a list.

[Johannes Tantow]

Or alternatively I used hashmaps to represent a graph (as an adjacency list)

[Ayush Priyadarshi]

But i still want to use functions defined in SimpleGraph Module in mathlib like isAcyclic
which are defined for sets as G.edgeset only and not a list
I need a way to switch back and forth between computation and existentiality in vague terms.

[Johannes Tantow]

You can have an effective graph model you work with and a translation to the mathlib model to prove stuff

[Ayush Priyadarshi]

Wouldn't i need both in the same model if i wanted to compute and prove optimality both.

[Johannes Tantow]

I don't see why. You define an internal graph representation(IGR) and a map transform: IGR -> mathlib graph. (Using AC this also works backwards). Then you show that for any input transform(kruskal(G)) is the minimal spanning tree for transform(G)

[Ruben Van de Velde]

There's docs#Finset.sort , right?

[Johannes Tantow]

But then you need basically a linear order again on the type

[Siddhartha Gadgil]

@Ayush Priyadarshi
Given a linear order on the type, here is code to make the list if needed. In practice you can make vertices subsets of something like Nat which is ordered.

import Mathlib

variable {V : Type u} [LinearOrder V]

def Finset.toOrderedList (s : Finset V) : List V :=
  if p:s.Nonempty then
    let head := s.min' p
    let tail := s.erase head
    have : tail.card < s.card := by
      apply Finset.card_erase_lt_of_mem
      apply Finset.min'_mem
    head :: Finset.toOrderedList tail
  else []
termination_by s.card

[Bhavik Mehta]

docs#Finset.sort would be the usual way of doing that