32.7. The Mathlib correspondence🔗

HexGraphIsoMathlib 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 HexGraphIsoMathlibChapterExample

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 HexGraphIsoMathlibChapterExample

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

32.7.1. Automorphism groups🔗

For a Mathlib-side coloured graph G, its colour-preserving automorphism group is the type Colored.Iso G G. The Mathlib bridge 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.