36.8. The Mathlib correspondence🔗

HexGraphIsoTheory relates the executable coloured graphs to Mathlib's SimpleGraph and extends the same graph_iso syntax to closed ground SimpleGraph terms. The two families below are parametrised and deliberately have different vertex types (Fin 2 × Fin p, a rim/spoke coordinate, for the generalized Petersen graph, and the two-element subsets of Fin 5 for the Kneser graph), so the positive goal genuinely enumerates two unrelated finite types and returns a SimpleGraph.Iso, rather than recognizing a definitional equality. graph_iso is a decision procedure on closed ground instances, so the parameters must be literals at the use site.

structure

Hex.GraphIso.Mathlib.Colored.{u} (V : Type u) (k : ℕ) [Fintype V] :
  Type u
Hex.GraphIso.Mathlib.Colored.{u}
  (V : Type u) (k : ℕ) [Fintype V] :
  Type u

A finite simple graph with an ordered vertex colouring by Fin k in which every colour is used. This is the Mathlib-side counterpart of Hex.GraphIso.Colored: the colouring need not be proper, and an isomorphism has to preserve each colour index.

Constructor

Hex.GraphIso.Mathlib.Colored.mk.{u}

Fields

graph : SimpleGraph V

The underlying Mathlib graph.

color : V → Fin k

The ordered colour of each vertex.

onto : Function.Surjective self.color

Every colour is used.

def

Hex.GraphIso.Mathlib.encode.{u} {V : Type u} [Fintype V] {k n : ℕ}
  (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] : Hex.GraphIso.Colored n k
Hex.GraphIso.Mathlib.encode.{u}
  {V : Type u} [Fintype V] {k n : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Colored n k

The executable image of a coloured Mathlib graph along a chosen finite enumeration.

theorem

Hex.GraphIso.Mathlib.colored_iso_iff_canon_eq.{u, v} {V : Type u}
  {W : Type v} [Fintype V] [Fintype W] {k n : ℕ}
  {G : Hex.GraphIso.Mathlib.Colored V k}
  {H : Hex.GraphIso.Mathlib.Colored W k} [DecidableRel G.graph.Adj]
  [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) :
  G.Isomorphic H ↔
    Hex.GraphIso.canon (Hex.GraphIso.Mathlib.encode eV G) =
      Hex.GraphIso.canon (Hex.GraphIso.Mathlib.encode eW H)
Hex.GraphIso.Mathlib.colored_iso_iff_canon_eq.{u,
    v}
  {V : Type u} {W : Type v} [Fintype V]
  [Fintype W] {k n : ℕ}
  {G : Hex.GraphIso.Mathlib.Colored V k}
  {H : Hex.GraphIso.Mathlib.Colored W k}
  [DecidableRel G.graph.Adj]
  [DecidableRel H.graph.Adj]
  (eV : V ≃ Fin n) (eW : W ≃ Fin n) :
  G.Isomorphic H ↔
    Hex.GraphIso.canon
        (Hex.GraphIso.Mathlib.encode eV
          G) =
      Hex.GraphIso.canon
        (Hex.GraphIso.Mathlib.encode eW H)

Two coloured Mathlib graphs are isomorphic exactly when their encodings have equal canonical forms. The right-hand side is a decidable equality of executable values, so this reduces a Mathlib isomorphism question to running the canonical labelling.

open Hex.GraphIso.Mathlib

namespace HexGraphIsoTheoryChapterExample

def gpetersen (p q : Nat) :
    SimpleGraph (Fin 2 × Fin p) where
  Adj v w :=
    v ≠ w ∧
      ((v.1 = 0 ∧ w.1 = 0 ∧
          (w.2.val = (v.2.val + 1) % p ∨
            v.2.val = (w.2.val + 1) % p)) ∨
       (v.1 = 1 ∧ w.1 = 1 ∧
          (w.2.val = (v.2.val + q) % p ∨
            v.2.val = (w.2.val + q) % p)) ∨
       (v.1 ≠ w.1 ∧ v.2 = w.2))
  symm := ⟨byp:ℕq:ℕ⊢ ∀ (a b : Fin 2 × Fin p),
  a ≠ b ∧
      (a.1 = 0 ∧ b.1 = 0 ∧ (↑b.2 = (↑a.2 + 1) % p ∨ ↑a.2 = (↑b.2 + 1) % p) ∨
        a.1 = 1 ∧ b.1 = 1 ∧ (↑b.2 = (↑a.2 + q) % p ∨ ↑a.2 = (↑b.2 + q) % p) ∨ a.1 ≠ b.1 ∧ a.2 = b.2) →
    b ≠ a ∧
      (b.1 = 0 ∧ a.1 = 0 ∧ (↑a.2 = (↑b.2 + 1) % p ∨ ↑b.2 = (↑a.2 + 1) % p) ∨
        b.1 = 1 ∧ a.1 = 1 ∧ (↑a.2 = (↑b.2 + q) % p ∨ ↑b.2 = (↑a.2 + q) % p) ∨ b.1 ≠ a.1 ∧ b.2 = a.2) grindAll goals completed! 🐙⟩
  loopless := ⟨byp:ℕq:ℕ⊢ ∀ (a : Fin 2 × Fin p),
  ¬(a ≠ a ∧
      (a.1 = 0 ∧ a.1 = 0 ∧ (↑a.2 = (↑a.2 + 1) % p ∨ ↑a.2 = (↑a.2 + 1) % p) ∨
        a.1 = 1 ∧ a.1 = 1 ∧ (↑a.2 = (↑a.2 + q) % p ∨ ↑a.2 = (↑a.2 + q) % p) ∨ a.1 ≠ a.1 ∧ a.2 = a.2)) grindAll goals completed! 🐙⟩

instance (p q : Nat) : DecidableRel (gpetersen p q).Adj :=
  fun _ _ => inferInstanceAs (Decidable (_ ∧ _))

def kneser (m r : Nat) :
    SimpleGraph {s : Finset (Fin m) // s.card = r} where
  Adj s t := Disjoint s.val t.val ∧ s ≠ t
  symm := ⟨bym:ℕr:ℕ⊢ ∀ (a b : { s // s.card = r }), Disjoint ↑a ↑b ∧ a ≠ b → Disjoint ↑b ↑a ∧ b ≠ a grindAll goals completed! 🐙⟩
  loopless := ⟨bym:ℕr:ℕ⊢ ∀ (a : { s // s.card = r }), ¬(Disjoint ↑a ↑a ∧ a ≠ a) grindAll goals completed! 🐙⟩

instance (m r : Nat) : DecidableRel (kneser m r).Adj :=
  fun _ _ => inferInstanceAs (Decidable (_ ∧ _))

example : Nonempty (gpetersen 5 2 ≃g kneser 5 2) := by⊢ Nonempty (gpetersen 5 2 ≃g kneser 5 2)
  graph_isoAll goals completed! 🐙

example : IsEmpty (gpetersen 5 2 ≃g gpetersen 5 1) := by⊢ IsEmpty (gpetersen 5 2 ≃g gpetersen 5 1)
  graph_isoAll goals completed! 🐙

end HexGraphIsoTheoryChapterExample

Neither proof requires an external nauty installation, and no proof path uses native_decide or introduces an axiom.

36.8.1. Automorphism groups🔗

For a Mathlib-side coloured graph G, its colour-preserving automorphism group is the type Colored.Iso G G. The theory companion gives this type a Group instance and lets it act on the vertices. A choice of enumeration e : V ≃ Fin n then identifies it, as a group, with the subgroup of executable permutations that preserve the encoded graph.

def

Hex.GraphIso.Mathlib.autEquiv.{u} {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  G.Iso G ≃* ↥(Hex.GraphIso.Aut.group (Hex.GraphIso.Mathlib.encode e G))
Hex.GraphIso.Mathlib.autEquiv.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  G.Iso G ≃*
    ↥(Hex.GraphIso.Aut.group
        (Hex.GraphIso.Mathlib.encode e G))

Encoding is an isomorphism of full automorphism groups.

The decoded list autos e G contains colour-preserving self-isomorphisms. Its completeness theorem is stated directly with Mathlib's Subgroup.closure: every element of Colored.Iso G G belongs to the subgroup generated by that list.

def

Hex.GraphIso.Mathlib.autos.{u} {V : Type u} [Fintype V] {k n : ℕ}
  (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] : List (G.Iso G)
Hex.GraphIso.Mathlib.autos.{u}
  {V : Type u} [Fintype V] {k n : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  List (G.Iso G)

The automorphism generators found by Hex.GraphIso.Aut.gens on the encoding, decoded as colour-preserving self-isomorphisms of the Mathlib graph. Each entry is an automorphism, by Hex.GraphIso.Aut.gens_isIso and isoOfIsIso. autos_complete proves that this list generates the full automorphism group.

theorem

Hex.GraphIso.Mathlib.autos_complete.{u} {V : Type u} [Fintype V]
  {n k : ℕ} (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] (f : G.Iso G) :
  f ∈ Subgroup.closure {g | g ∈ Hex.GraphIso.Mathlib.autos e G}
Hex.GraphIso.Mathlib.autos_complete.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj]
  (f : G.Iso G) :
  f ∈
    Subgroup.closure
      {g |
        g ∈
          Hex.GraphIso.Mathlib.autos e G}

Every colour-preserving automorphism belongs to the subgroup generated by the decoded list.

The reported orbit array also describes the action of the full group, not merely the action of the generators encountered before a particular point in the search. Equality of two stored representatives is equivalent to the existence of a colour-preserving self-isomorphism carrying one vertex to the other. The quotient equivalence exposes the same fact in Mathlib's group-action vocabulary.

theorem

Hex.GraphIso.Mathlib.autos_sameOrbit.{u} {V : Type u} [Fintype V]
  {n k : ℕ} (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] (v w : V) :
  (Hex.GraphIso.Aut.orbits (Hex.GraphIso.Mathlib.encode e G))[↑(e v)]! =
      (Hex.GraphIso.Aut.orbits
          (Hex.GraphIso.Mathlib.encode e G))[↑(e w)]! ↔
    ∃ f, f.graphIso v = w
Hex.GraphIso.Mathlib.autos_sameOrbit.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] (v w : V) :
  (Hex.GraphIso.Aut.orbits
          (Hex.GraphIso.Mathlib.encode e
            G))[↑(e v)]! =
      (Hex.GraphIso.Aut.orbits
          (Hex.GraphIso.Mathlib.encode e
            G))[↑(e w)]! ↔
    ∃ f, f.graphIso v = w

The reported partition is exactly the full automorphism orbit relation.

def

Hex.GraphIso.Mathlib.autOrbitEquiv.{u} {V : Type u} [Fintype V]
  {n k : ℕ} (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  MulAction.orbitRel.Quotient (G.Iso G) V ≃
    MulAction.orbitRel.Quotient
      (↥(Hex.GraphIso.Aut.group (Hex.GraphIso.Mathlib.encode e G)))
      (Fin n)
Hex.GraphIso.Mathlib.autOrbitEquiv.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  MulAction.orbitRel.Quotient (G.Iso G)
      V ≃
    MulAction.orbitRel.Quotient
      (↥(Hex.GraphIso.Aut.group
          (Hex.GraphIso.Mathlib.encode e
            G)))
      (Fin n)

Encoding preserves the full automorphism orbit quotient.

Finally, the two numerical results have exact cardinality theorems. autNumOrbits e G is the cardinality of the orbit quotient for the action of Colored.Iso G G on V, and autOrder e G is the cardinality of Colored.Iso G G itself.

theorem

Hex.GraphIso.Mathlib.autNumOrbits_card.{u} {V : Type u} [Fintype V]
  {n k : ℕ} (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.autNumOrbits e G =
    Nat.card (MulAction.orbitRel.Quotient (G.Iso G) V)
Hex.GraphIso.Mathlib.autNumOrbits_card.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.autNumOrbits e G =
    Nat.card
      (MulAction.orbitRel.Quotient
        (G.Iso G) V)

The reported orbit count equals the cardinality of the Mathlib-facing full automorphism orbit quotient.

theorem

Hex.GraphIso.Mathlib.autOrder_card.{u} {V : Type u} [Fintype V]
  {n k : ℕ} (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.autOrder e G = Nat.card (G.Iso G)
Hex.GraphIso.Mathlib.autOrder_card.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.autOrder e G =
    Nat.card (G.Iso G)

The reported order equals the cardinality of the Mathlib-facing colour-preserving automorphism group.

36.8.2. Choosing sparse search from Mathlib🔗

The direct graph_iso extension on Mathlib graphs uses the dense encoding. To select sparse nauty, apply Sparse.encode_iso_iff and then use graph_iso on the resulting native sparse goal. Both enumerations may be chosen independently. The theorem transports the answer back to the original coloured Mathlib graphs.

Here two presentations of a five-cycle use steps of one and two in Fin 5. A path on the same five vertices supplies a negative example. The definitions and claims are on the Mathlib side; the sparse encoding appears only inside the proofs.

namespace HexGraphIsoSparseTheoryExample

def cycle : SimpleGraph (Fin 5) :=
  SimpleGraph.fromRel fun i j => j = i + 1
def star : SimpleGraph (Fin 5) :=
  SimpleGraph.fromRel fun i j => j = i + 2
def path : SimpleGraph (Fin 5) :=
  SimpleGraph.fromRel fun i j => j.val = i.val + 1

instance : DecidableRel cycle.Adj := fun _ _ =>
  decidable_of_iff _ (SimpleGraph.fromRel_adj ..).symm
instance : DecidableRel star.Adj := fun _ _ =>
  decidable_of_iff _ (SimpleGraph.fromRel_adj ..).symm
instance : DecidableRel path.Adj := fun _ _ =>
  decidable_of_iff _ (SimpleGraph.fromRel_adj ..).symm

def uncoloured (G : SimpleGraph (Fin 5)) :
    Hex.GraphIso.Mathlib.Colored (Fin 5) 1 :=
  ⟨G, fun _ => 0, fun c => ⟨0, Subsingleton.elim _ c⟩⟩

instance (G : SimpleGraph (Fin 5)) [DecidableRel G.Adj] :
    DecidableRel (uncoloured G).graph.Adj :=
  inferInstanceAs (DecidableRel G.Adj)

example : (uncoloured cycle).Isomorphic
    (uncoloured star) := by⊢ (uncoloured cycle).Isomorphic (uncoloured star)
  apply (Sparse.encode_iso_iff
    (Equiv.refl (Fin 5)) (Equiv.swap (0 : Fin 5) 4)).mpr⊢ Sparse.Isomorphic (Sparse.encode (Equiv.refl (Fin 5)) (uncoloured cycle))
  (Sparse.encode (Equiv.swap 0 4) (uncoloured star))
  graph_isoAll goals completed! 🐙

example : ¬ (uncoloured cycle).Isomorphic
    (uncoloured path) := by⊢ ¬(uncoloured cycle).Isomorphic (uncoloured path)
  rw [Sparse.encode_iso_iff
    (Equiv.refl (Fin 5)) (Equiv.refl (Fin 5))⊢ ¬Sparse.Isomorphic (Sparse.encode (Equiv.refl (Fin 5)) (uncoloured cycle))
    (Sparse.encode (Equiv.refl (Fin 5)) (uncoloured path))]⊢ ¬Sparse.Isomorphic (Sparse.encode (Equiv.refl (Fin 5)) (uncoloured cycle))
    (Sparse.encode (Equiv.refl (Fin 5)) (uncoloured path))
  graph_isoAll goals completed! 🐙

end HexGraphIsoSparseTheoryExample

Sparse.encode constructs sorted neighbour rows without allocating a dense matrix. Given only an arbitrary decidable adjacency relation, it still tests vertex pairs. For input already available as an edge list, the native SparseGraph.ofEdges constructor avoids that quadratic enumeration.

Sparse.iso_iff_canon_eq characterizes Mathlib isomorphism by equality of the computed sparse forms, and Sparse.canon_encode_eq proves independence from the chosen enumeration. A successful isomorphism search can also be decoded directly with Sparse.isoOfFindIso.

The automorphism operations have the same Mathlib interpretations as their dense counterparts. Sparse.autEquiv identifies the colour-preserving Mathlib automorphism group with the executable sparse permutation subgroup. Sparse.autos_complete states generation using Subgroup.closure, and Sparse.autos_sameOrbit identifies the computed representatives with the full group action. The numerical results are exact cardinalities:

theorem

Hex.GraphIso.Mathlib.Sparse.autNumOrbits_card.{u} {V : Type u}
  [Fintype V] {n k : ℕ} (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k) [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.Sparse.autNumOrbits e G =
    Nat.card (MulAction.orbitRel.Quotient (G.Iso G) V)
Hex.GraphIso.Mathlib.Sparse.autNumOrbits_card.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.Sparse.autNumOrbits
      e G =
    Nat.card
      (MulAction.orbitRel.Quotient
        (G.Iso G) V)

The native sparse orbit count equals the number of full Mathlib automorphism orbits, including empty graphs and arbitrary enumerations.

theorem

Hex.GraphIso.Mathlib.Sparse.autOrder_card.{u} {V : Type u} [Fintype V]
  {n k : ℕ} (e : V ≃ Fin n) (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.Sparse.autOrder e G = Nat.card (G.Iso G)
Hex.GraphIso.Mathlib.Sparse.autOrder_card.{u}
  {V : Type u} [Fintype V] {n k : ℕ}
  (e : V ≃ Fin n)
  (G : Hex.GraphIso.Mathlib.Colored V k)
  [DecidableRel G.graph.Adj] :
  Hex.GraphIso.Mathlib.Sparse.autOrder e
      G =
    Nat.card (G.Iso G)

The product accumulated by the native sparse traversal is the order of the full Mathlib automorphism group for any chosen enumeration.