CubicPathwidth.Alg.Proofs2.X2RelabelExists

Source file CubicPathwidth/Alg/Proofs2/X2RelabelExists.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2

/-!
Stage 2 task X2: `RelabelExists`.

Every well-formed graph `G` is a relabelling of a simple graph on `Fin G.numNodes`:
`e i := G.nodes[i]` is injective (the node list is duplicate-free), its range is the
node set, and `S := SimpleGraph.fromRel (fun i j => G.Adj (e i) (e j))` has adjacency
exactly `G.Adj (e i) (e j)` (symmetry gives the `∨`, looplessness gives `i ≠ j`).
-/

namespace CubicPathwidth.Alg

open Graph

namespace X2

/-- The `i`-th node of `G` in its node list. -/
def nodeAt (G : Graph) (i : Fin G.numNodes) : Nat := G.nodes[i.val]'i.isLt

theorem nodeAt_injective {G : Graph} (hG : G.WF) : Function.Injective (nodeAt G) := by
  intro i j h
  apply Fin.ext
  have h' : G.nodes[i.val]'i.isLt = G.nodes[j.val]'j.isLt := h
  exact (hG.nodup.getElem_inj_iff).1 h'

theorem nodeAt_mem (G : Graph) (i : Fin G.numNodes) : nodeAt G i ∈ G.nodes :=
  List.getElem_mem i.isLt

end X2

/-- Every well-formed graph has a relabelling onto `Fin numNodes`. -/
theorem relabelExists : RelabelExists := by
  intro G hG
  refine ⟨SimpleGraph.fromRel fun i j => G.Adj (X2.nodeAt G i) (X2.nodeAt G j),
    X2.nodeAt G, ?_, ?_, ?_⟩
  · exact X2.nodeAt_injective hG
  · intro v
    constructor
    · intro hv
      obtain ⟨k, hk, hkv⟩ := List.mem_iff_getElem.1 hv
      exact ⟨⟨k, hk⟩, hkv⟩
    · rintro ⟨i, rfl⟩
      exact X2.nodeAt_mem G i
  · intro i j
    simp only [SimpleGraph.fromRel_adj]
    constructor
    · rintro ⟨_, h | h⟩
      · exact h
      · exact hG.symm _ _ h
    · intro h
      refine ⟨fun hij => ?_, Or.inl h⟩
      subst hij
      exact hG.loopless _ h

#print axioms CubicPathwidth.Alg.relabelExists

end CubicPathwidth.Alg