Prim implementation - #12
Conversation
|
This is looking nice so far! A couple of suggestions for once it's had a polishing pass:
|
|
Thank you for the feedback.
I also wanted to ask if the structure ParentTree (α : Type*) where
vertexSet : Finset α
parent : α -> α
level : α -> ℕ
incidence : ∀ v ∈ vertexSet, parent v ∈ vertexSet
ordering : ∀ v ∈ vertexSet, level v > 0 → level (parent v) < level v
root : ∀ v ∈ vertexSet, level v = 0 ↔ v = parent v
abbrev appendNodes (G : ParentTree α) (new_nodes : Finset α)
(edges : α → α) (h : ∀ v ∈ new_nodes, edges v ∈ Vₚ(G)) : ParentTree α :=
{
vertexSet := G.vertexSet ∪ new_nodes,
parent := fun v => if v ∈ G.vertexSet then G.parent v else edges v,
level := fun v => if v ∈ G.vertexSet then G.level v else (G.level (edges v) + 1),
incidence := by have := G.incidence; grind,
root := by have := G.root; grind,
ordering := by have := G.ordering; have := G.incidence; grind
}I'm finishing the details on the acyclicity proof of it. Should I make a separate PR for that definition alone? |
|
For 2) the graph definitions are already on the Your definition of
|
| open Finset WeightedSimpleGraph Sym2 | ||
|
|
||
| def is_connected (G : WeightedSimpleGraph α) : Prop := | ||
| ∀ u v: α , u ≠ v → ∃ p: Walk α, Path.IsPathIn G p |
There was a problem hiding this comment.
Maybe a typo here?
Should have p.head = u && p.tail =v
| level : α -> ℕ | ||
| incidence : ∀ v ∈ vertexSet, parent v ∈ vertexSet | ||
| ordering : ∀ v ∈ vertexSet, level v > 0 → level (parent v) < level v | ||
| root : ∀ v ∈ vertexSet, level v = 0 ↔ v = parent v |
There was a problem hiding this comment.
The ParentTree definition does not require connectedness. It can have many isolated roots. Not sure whether it's deliberate.
There was a problem hiding this comment.
I could add a Prop of the kind that there exists a unique vertex with that property or maybe have it as a theorem. My original idea was to have a theorem of the sort, if the prim is calculated on a connected graph, then the ParentTree that spans it would also be connected. If you prefer to include it in the definition I can change it.
| grind | ||
|
|
||
| @[grind →] lemma edge_antisymm_iff (G : ParentTree α) (u v : α) (hu : u ∈ Vₚ(G)) (hv :v ∈ Vₚ(G)): | ||
| u ∈ Nₚ(G, v) ↔ u ∈ Nₚ(G, v) := by |
There was a problem hiding this comment.
I'll push a change with the fixed typo. I am finishing now the proof that the tree is acyclic and the fact that each iteration of the prim, adds an edge on the spanning tree
| if h : crossing.Nonempty then | ||
| let chosen := | ||
| disjointEdges <| | ||
| minimumWeightEdges G crossing h |
There was a problem hiding this comment.
For this step, do you want to select more than one edges with min weight? I think it might be simpler to select one arbitrary edge with min weight in each iteration.
There was a problem hiding this comment.
Yeah I think choosing multiple edges might even be wrong. Will modify it!
| (edges : Finset (Edge α)) (acc : Finset (Edge α)) : | ||
| Finset (Edge α) := | ||
| if h: edges.Nonempty then | ||
| let x := h.choose |
There was a problem hiding this comment.
If x is arbitrary in h, we may terminate with selecting only one edge even if h is large.
3 participants
I am working on the prim algorithm and I wanted to make this PR for it. There is still a lot of cleanup to be done but I wanted to add this in case for early feedback