Forests and Mathlib simple graphs

Bridge between the edge-set forests of BKAR.Forest and Mathlib's SimpleGraph API. Associates to a finite edge set the simple graph it generates, translates adjacency, walks, and acyclicity back and forth (SimpleGraph.IsAcyclic), and derives the graph-theoretic facts used elsewhere: existence and uniqueness of simple paths in an acyclic edge set, and stability of acyclicity under adding an edge between distinct components.

theorem BKAR.simpleGraph_isAcyclic_sup_edge_of_not_reachable {V : Type u_1} {G : SimpleGraph V} {x y : V} (hG : G.IsAcyclic) (hxy : ¬G.Reachable x y) : (G ⊔ SimpleGraph.edge x y).IsAcyclic

def BKAR.EdgePath.edgeSetGraph {V : Type u_1} (S : Finset (Edge V)) : SimpleGraph V

The simple graph whose edge set is the underlying Sym2 image of S.

Equations

• BKAR.EdgePath.edgeSetGraph S = SimpleGraph.fromEdgeSet {x : Sym2 V | ∃ e ∈ S, ↑e = x}

theorem BKAR.EdgePath.edgeSetGraph_adj_of_mem_between {V : Type u_1} {S : Finset (Edge V)} {e : Edge V} {i j : V} (he : e ∈ S) (hbetween : e.Between i j) : (edgeSetGraph S).Adj i j

theorem BKAR.EdgePath.exists_mem_between_of_edgeSetGraph_adj {V : Type u_1} {S : Finset (Edge V)} {i j : V} (h : (edgeSetGraph S).Adj i j) : ∃ e ∈ S, e.Between i j

noncomputable def BKAR.EdgePath.edgeOfAdj {V : Type u_1} {S : Finset (Edge V)} {i j : V} (h : (edgeSetGraph S).Adj i j) : Edge V

The local edge selected by an adjacency in edgeSetGraph S.

Equations

• BKAR.EdgePath.edgeOfAdj h = Classical.choose ⋯

theorem BKAR.EdgePath.edgeOfAdj_mem {V : Type u_1} {S : Finset (Edge V)} {i j : V} (h : (edgeSetGraph S).Adj i j) : edgeOfAdj h ∈ S

theorem BKAR.EdgePath.edgeOfAdj_between {V : Type u_1} {S : Finset (Edge V)} {i j : V} (h : (edgeSetGraph S).Adj i j) : (edgeOfAdj h).Between i j

theorem BKAR.EdgePath.edge_adj_iff_between {V : Type u_1} (e : Edge V) {i j : V} : (SimpleGraph.edge e.left e.right).Adj i j ↔ e.Between i j

theorem BKAR.EdgePath.edgeSetGraph_insert {V : Type u_1} [DecidableEq V] (S : Finset (Edge V)) (e : Edge V) : edgeSetGraph (insert e S) = edgeSetGraph S ⊔ SimpleGraph.edge e.left e.right

theorem BKAR.EdgePath.IsPath.exists_walk {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} : IsPath S γ i j → ∃ (p : (edgeSetGraph S).Walk i j), p.edges = List.map (fun (e : Edge V) => ↑e) γ

theorem BKAR.EdgePath.IsSimplePath.exists_walk_isTrail {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} (h : IsSimplePath S γ i j) : ∃ (p : (edgeSetGraph S).Walk i j), p.edges = List.map (fun (e : Edge V) => ↑e) γ ∧ p.IsTrail

theorem BKAR.EdgePath.IsSimplePath.exists_graph_path_of_isAcyclic {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} (hG : (edgeSetGraph S).IsAcyclic) (h : IsSimplePath S γ i j) : ∃ (p : (edgeSetGraph S).Path i j), (↑p).edges = List.map (fun (e : Edge V) => ↑e) γ

theorem BKAR.EdgePath.IsSimplePath.unique_of_isAcyclic {V : Type u_1} {S : Finset (Edge V)} {γ₁ γ₂ : List (Edge V)} {i j : V} (hG : (edgeSetGraph S).IsAcyclic) (h₁ : IsSimplePath S γ₁ i j) (h₂ : IsSimplePath S γ₂ i j) : γ₁ = γ₂

def BKAR.EdgePath.Walk.toEdgePath {V : Type u_1} {S : Finset (Edge V)} {i j : V} (p : (edgeSetGraph S).Walk i j) : List (Edge V)

Convert a Mathlib walk in edgeSetGraph S back to a local edge-list.

Equations

• BKAR.EdgePath.Walk.toEdgePath SimpleGraph.Walk.nil = []
• BKAR.EdgePath.Walk.toEdgePath (SimpleGraph.Walk.cons h p_2) = BKAR.EdgePath.edgeOfAdj h :: BKAR.EdgePath.Walk.toEdgePath p_2

theorem BKAR.EdgePath.Walk.toEdgePath_isPath {V : Type u_1} {S : Finset (Edge V)} {i j : V} (p : (edgeSetGraph S).Walk i j) : IsPath S (toEdgePath p) i j

theorem BKAR.EdgePath.Walk.toEdgePath_edges {V : Type u_1} {S : Finset (Edge V)} {i j : V} (p : (edgeSetGraph S).Walk i j) : List.map (fun (e : Edge V) => ↑e) (toEdgePath p) = p.edges

theorem BKAR.EdgePath.Walk.toEdgePath_isSimplePath_of_isTrail {V : Type u_1} {S : Finset (Edge V)} {i j : V} {p : (edgeSetGraph S).Walk i j} (hp : p.IsTrail) : IsSimplePath S (toEdgePath p) i j

theorem BKAR.EdgePath.Walk.toEdgePath_isSimplePath_of_isPath {V : Type u_1} {S : Finset (Edge V)} {i j : V} {p : (edgeSetGraph S).Walk i j} (hp : p.IsPath) : IsSimplePath S (toEdgePath p) i j

theorem BKAR.AcyclicEdgeSetData.edgeSetGraph_isAcyclic {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) : (EdgePath.edgeSetGraph S).IsAcyclic

theorem BKAR.AcyclicEdgeSetData.inSameComponent_of_edgeSetGraph_reachable {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {i j : V} (h : (EdgePath.edgeSetGraph S).Reachable i j) : data.inSameComponent i j

theorem BKAR.AcyclicEdgeSetData.inSameComponent_trans {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {i j k : V} (hij : data.inSameComponent i j) (hjk : data.inSameComponent j k) : data.inSameComponent i k

theorem BKAR.AcyclicEdgeSetData.inSameComponent_iff_of_between {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {e : Edge V} {i j : V} (hbetween : e.Between i j) : data.inSameComponent e.left e.right ↔ data.inSameComponent i j

theorem BKAR.AcyclicEdgeSetData.isAcyclicEdgeSet_insert_of_not_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {e : Edge V} (hnot : ¬data.inSameComponent e.left e.right) : IsAcyclicEdgeSet (insert e S)

theorem BKAR.AcyclicEdgeSetData.acyclic_insert_iff {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {e : Edge V} (he : e ∉ S) : IsAcyclicEdgeSet (insert e S) ↔ ¬data.inSameComponent e.left e.right

def BKAR.AcyclicEdgeSetData.toForest {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) : Forest V

Upgrade any acyclicity certificate to a Forest representative certificate.

Equations

• data.toForest = { edges := S, acyclic := data, acyclic_insert_iff' := ⋯ }

theorem BKAR.AcyclicEdgeSetData.toForest_edges {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) : data.toForest.edges = S

theorem BKAR.Forest.inSameComponent_trans {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {i j k : V} (hij : F.inSameComponent i j) (hjk : F.inSameComponent j k) : F.inSameComponent i k