structure Hex.GraphIso.Perm (n : Nat) : Type

A permutation of the vertex set Fin n, stored as the array of images: vertex i maps to vec[i]. The two proof fields record that the array is duplicate-free and contains every vertex; both are decidable, and carrying both makes the inverse constructible directly.

• vec : Vector (Fin n) n

  The image array: vertex i maps to vec[i].

• nodup : self.vec.toList.Nodup

  The image array has no duplicate entries.

• complete (i : Fin n) : i ∈ self.vec.toList

  Every vertex occurs in the image array.

@[inline]

def Hex.GraphIso.Perm.get {n : Nat} (p : Perm n) (i : Fin n) : Fin n

Apply a permutation to a vertex.

Equations

• p.get i = p.vec[i]

@[instance_reducible]

instance Hex.GraphIso.Perm.instCoeFunForallFin {n : Nat} : CoeFun (Perm n) fun (x : Perm n) => Fin n → Fin n

Equations

• Hex.GraphIso.Perm.instCoeFunForallFin = { coe := Hex.GraphIso.Perm.get }

theorem Hex.GraphIso.Perm.get_toList {n : Nat} (p : Perm n) (i : Fin n) : p.vec.toList[↑i] = p.get i

theorem Hex.GraphIso.Perm.get_ne {n : Nat} (p : Perm n) {i j : Fin n} (h : i ≠ j) : p.get i ≠ p.get j

Distinct vertices have distinct images.

theorem Hex.GraphIso.Perm.get_inj {n : Nat} (p : Perm n) {i j : Fin n} (h : p.get i = p.get j) : i = j

A permutation is injective.

theorem Hex.GraphIso.Perm.get_surj {n : Nat} (p : Perm n) (i : Fin n) : ∃ (j : Fin n), p.get j = i

A permutation is surjective.

theorem Hex.GraphIso.Perm.ext_vec {n : Nat} {p q : Perm n} (h : p.vec = q.vec) : p = q

Two permutations with the same image array are equal.

theorem Hex.GraphIso.Perm.ext {n : Nat} {p q : Perm n} (h : ∀ (i : Fin n), p.get i = q.get i) : p = q

Extensional equality of permutations.

theorem Hex.GraphIso.Perm.ext_iff {n : Nat} {p q : Perm n} : p = q ↔ ∀ (i : Fin n), p.get i = q.get i

@[instance_reducible]

instance Hex.GraphIso.Perm.instDecidableEq {n : Nat} : DecidableEq (Perm n)

Equations

• p.instDecidableEq q = if h : p.vec = q.vec then isTrue ⋯ else isFalse ⋯

theorem Hex.GraphIso.Perm.nodup_ofFn_toList {n : Nat} {f : Fin n → Fin n} (hf : ∀ (i j : Fin n), f i = f j → i = j) : (Vector.ofFn f).toList.Nodup

The image array of every vertex in order is duplicate-free and complete whenever the entry function is injective and surjective.

theorem Hex.GraphIso.Perm.complete_ofFn_toList {n : Nat} {f : Fin n → Fin n} (hf : ∀ (i : Fin n), ∃ (j : Fin n), f j = i) (i : Fin n) : i ∈ (Vector.ofFn f).toList

def Hex.GraphIso.Perm.ofFn {n : Nat} (f : Fin n → Fin n) (hinj : ∀ (i j : Fin n), f i = f j → i = j) (hsurj : ∀ (i : Fin n), ∃ (j : Fin n), f j = i) : Perm n

Build a permutation from an injective-and-surjective entry function.

Equations

• Hex.GraphIso.Perm.ofFn f hinj hsurj = { vec := Hex.Vector.ofFn' f, nodup := ⋯, complete := ⋯ }

@[simp]

theorem Hex.GraphIso.Perm.get_ofFn {n : Nat} (f : Fin n → Fin n) (hinj : ∀ (i j : Fin n), f i = f j → i = j) (hsurj : ∀ (i : Fin n), ∃ (j : Fin n), f j = i) (i : Fin n) : (ofFn f hinj hsurj).get i = f i

def Hex.GraphIso.Perm.ofVector? {n : Nat} (v : Vector (Fin n) n) : Option (Perm n)

Checked construction: accepts exactly the duplicate-free complete vertex arrays.

Equations

• Hex.GraphIso.Perm.ofVector? v = if h : v.toList.Nodup ∧ ∀ (i : Fin n), i ∈ v.toList then some { vec := v, nodup := ⋯, complete := ⋯ } else none

theorem Hex.GraphIso.Perm.isSome_ofVector? {n : Nat} (v : Vector (Fin n) n) : (ofVector? v).isSome = true ↔ v.toList.Nodup ∧ ∀ (i : Fin n), i ∈ v.toList

theorem Hex.GraphIso.Perm.vec_of_ofVector? {n : Nat} {v : Vector (Fin n) n} {p : Perm n} (h : ofVector? v = some p) : p.vec = v

def Hex.GraphIso.Perm.id (n : Nat) : Perm n

The identity permutation.

Equations

• Hex.GraphIso.Perm.id n = Hex.GraphIso.Perm.ofFn (fun (i : Fin n) => i) ⋯ ⋯

@[simp]

theorem Hex.GraphIso.Perm.get_id {n : Nat} (i : Fin n) : (Perm.id n).get i = i

def Hex.GraphIso.Perm.comp {n : Nat} (p q : Perm n) : Perm n

Composition: (p.comp q).get i = p.get (q.get i).

Equations

• p.comp q = Hex.GraphIso.Perm.ofFn (fun (i : Fin n) => p.get (q.get i)) ⋯ ⋯

@[simp]

theorem Hex.GraphIso.Perm.get_comp {n : Nat} (p q : Perm n) (i : Fin n) : (p.comp q).get i = p.get (q.get i)

@[inline]

def Hex.GraphIso.Perm.scatterStep {n : Nat} (p : Perm n) (v : Vector (Fin n) n) (i : Fin n) : Vector (Fin n) n

One scatter step: record i at position p.get i.

Equations

• p.scatterStep v i = v.set (↑(p.get i)) i ⋯

def Hex.GraphIso.Perm.invVec {n : Nat} (p : Perm n) : Vector (Fin n) n

The image array of the inverse, built by one scatter pass over the vertices: each i is written at position p.get i. Every position is written, because p is surjective.

Equations

• p.invVec = List.foldl p.scatterStep (Hex.Vector.ofFn' fun (i : Fin n) => i) (List.finRange n)

theorem Hex.GraphIso.Perm.getElem_foldl_scatterStep_of_forall_ne {n : Nat} (p : Perm n) (l : List (Fin n)) (v : Vector (Fin n) n) (q : Fin n) : (∀ (j : Fin n), j ∈ l → p.get j ≠ q) → (List.foldl p.scatterStep v l)[↑q] = v[↑q]

A scatter pass leaves untouched every position that is not the image of an element of the list.

theorem Hex.GraphIso.Perm.getElem_foldl_scatterStep {n : Nat} (p : Perm n) (l : List (Fin n)) (v : Vector (Fin n) n) {i : Fin n} : i ∈ l → (List.foldl p.scatterStep v l)[↑(p.get i)] = i

A scatter pass writes i at position p.get i for every i in the list.

def Hex.GraphIso.Perm.preimage {n : Nat} (p : Perm n) (i : Fin n) : Fin n

The vertex mapping to i, read off the scattered inverse array.

Equations

• p.preimage i = p.invVec[↑i]

@[simp]

theorem Hex.GraphIso.Perm.preimage_get {n : Nat} (p : Perm n) (i : Fin n) : p.preimage (p.get i) = i

@[simp]

theorem Hex.GraphIso.Perm.get_preimage {n : Nat} (p : Perm n) (i : Fin n) : p.get (p.preimage i) = i

theorem Hex.GraphIso.Perm.preimage_inj {n : Nat} (p : Perm n) {i j : Fin n} (h : p.preimage i = p.preimage j) : i = j

theorem Hex.GraphIso.Perm.nodup_toList {n : Nat} {v : Vector (Fin n) n} (hv : ∀ (i j : Fin n), v[↑i] = v[↑j] → i = j) : v.toList.Nodup

The image array of a permutation is duplicate-free whenever its entries are pairwise distinct.

def Hex.GraphIso.Perm.inv {n : Nat} (p : Perm n) : Perm n

The inverse permutation: the scattered inverse array.

Equations

• p.inv = { vec := p.invVec, nodup := ⋯, complete := ⋯ }

theorem Hex.GraphIso.Perm.get_inv {n : Nat} (p : Perm n) (i : Fin n) : p.inv.get i = p.preimage i

@[simp]

theorem Hex.GraphIso.Perm.get_inv_get {n : Nat} (p : Perm n) (i : Fin n) : p.get (p.inv.get i) = i

@[simp]

theorem Hex.GraphIso.Perm.inv_get_get {n : Nat} (p : Perm n) (i : Fin n) : p.inv.get (p.get i) = i

@[simp]

theorem Hex.GraphIso.Perm.comp_id {n : Nat} (p : Perm n) : p.comp (Perm.id n) = p

@[simp]

theorem Hex.GraphIso.Perm.id_comp {n : Nat} (p : Perm n) : (Perm.id n).comp p = p

theorem Hex.GraphIso.Perm.comp_assoc {n : Nat} (p q r : Perm n) : (p.comp q).comp r = p.comp (q.comp r)

@[simp]

theorem Hex.GraphIso.Perm.comp_inv_self {n : Nat} (p : Perm n) : p.comp p.inv = Perm.id n

@[simp]

theorem Hex.GraphIso.Perm.inv_comp_self {n : Nat} (p : Perm n) : p.inv.comp p = Perm.id n

@[simp]

theorem Hex.GraphIso.Perm.inv_inv {n : Nat} (p : Perm n) : p.inv.inv = p

@[simp]

theorem Hex.GraphIso.Perm.inv_id {n : Nat} : (Perm.id n).inv = Perm.id n

theorem Hex.GraphIso.Perm.inv_comp {n : Nat} (p q : Perm n) : (p.comp q).inv = q.inv.comp p.inv

def Hex.GraphIso.Perm.ofNatArray? (n : Nat) (a : Array Nat) : Option (Perm n)

Checked permutation construction from raw entries, for literal data emitted by tactics: entries must be in range, duplicate-free, and complete.

Equations

• Hex.GraphIso.Perm.ofNatArray? n a = if h : a.size = n ∧ ∀ (i : Nat) (hi : i < a.size), a[i] < n then Hex.GraphIso.Perm.ofVector? (Hex.Vector.ofFn' fun (i : Fin n) => ⟨a[↑i], ⋯⟩) else none

structure Hex.GraphIso.Label (n : Nat) : Type

A canonical-labelling result array in nauty's canonlab convention: l[i] is the old vertex placed at new position i. The underlying data is the same duplicate-free complete vertex array as Perm. The wrapper marks the direction.

• perm : Perm n

  The underlying bijection sending each new position to the old vertex placed there.

@[instance_reducible]

instance Hex.GraphIso.Label.instDecidableEq {n : Nat} : DecidableEq (Label n)

Equations

• l.instDecidableEq m = if h : l.perm = m.perm then isTrue ⋯ else isFalse ⋯

@[inline]

def Hex.GraphIso.Label.get {n : Nat} (l : Label n) (i : Fin n) : Fin n

The old vertex at new position i.

Equations

• l.get i = l.perm.get i

@[instance_reducible]

instance Hex.GraphIso.Label.instGetElemFinTrue {n : Nat} : GetElem (Label n) (Fin n) (Fin n) fun (x : Label n) (x_1 : Fin n) => True

Equations

• Hex.GraphIso.Label.instGetElemFinTrue = { getElem := fun (l : Hex.GraphIso.Label n) (i : Fin n) (x : True) => l.get i }

@[simp]

theorem Hex.GraphIso.Label.getElem_eq_get {n : Nat} (l : Label n) (i : Fin n) : l[i] = l.get i

theorem Hex.GraphIso.Label.ext {n : Nat} {l m : Label n} (h : ∀ (i : Fin n), l.get i = m.get i) : l = m

theorem Hex.GraphIso.Label.ext_iff {n : Nat} {l m : Label n} : l = m ↔ ∀ (i : Fin n), l.get i = m.get i

def Hex.GraphIso.Label.ofVector? {n : Nat} (v : Vector (Fin n) n) : Option (Label n)

Checked construction from a vertex array.

Equations

• Hex.GraphIso.Label.ofVector? v = Option.map Hex.GraphIso.Label.mk (Hex.GraphIso.Perm.ofVector? v)

def Hex.GraphIso.Label.id (n : Nat) : Label n

The identity labelling.

Equations

• Hex.GraphIso.Label.id n = { perm := Hex.GraphIso.Perm.id n }

@[simp]

theorem Hex.GraphIso.Label.get_id {n : Nat} (i : Fin n) : (Label.id n).get i = i

def Hex.GraphIso.Label.comp {n : Nat} (l m : Label n) : Label n

Sequential composition: relabelling by l and then by m is relabelling by l.comp m, with (l.comp m).get i = l.get (m.get i).

Equations

• l.comp m = { perm := l.perm.comp m.perm }

@[simp]

theorem Hex.GraphIso.Label.get_comp {n : Nat} (l m : Label n) (i : Fin n) : (l.comp m).get i = l.get (m.get i)

def Hex.GraphIso.Label.toPerm {n : Nat} (l : Label n) : Perm n

The forward permutation of a labelling: old vertex v moves to the new position where l placed it.

Equations

• l.toPerm = l.perm.inv

@[simp]

theorem Hex.GraphIso.Label.get_toPerm_get {n : Nat} (l : Label n) (i : Fin n) : l.get (l.toPerm.get i) = i

@[simp]

theorem Hex.GraphIso.Label.toPerm_get_get {n : Nat} (l : Label n) (i : Fin n) : l.toPerm.get (l.get i) = i

def Hex.GraphIso.Label.ofArray? (n : Nat) (lab : Array Nat) : Option (Label n)

Checked construction from a raw array of vertex numbers: none unless the array has length n, entries below n, and describes a permutation.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Label.ofVector?_perm_vec {n : Nat} {v : Vector (Fin n) n} {l : Label n} (h : ofVector? v = some l) : l.perm.vec = v

theorem Hex.GraphIso.Label.ofArray?_bounds {n : Nat} {lab : Array Nat} {l : Label n} (h : ofArray? n lab = some l) : lab.size = n ∧ ∀ (v : Nat), v ∈ lab → v < n

theorem Hex.GraphIso.Label.ofArray?_get {n : Nat} {lab : Array Nat} {l : Label n} (h : ofArray? n lab = some l) (i : Nat) (hi : i < n) : ↑(l.get ⟨i, hi⟩) = lab[i]!

A checked labelling reads back the raw array entrywise.

def Hex.GraphIso.Perm.toLabel {n : Nat} (p : Perm n) : Label n

The labelling of a forward permutation: new position i holds the old vertex mapped to i.

Equations

• p.toLabel = { perm := p.inv }

@[simp]

theorem Hex.GraphIso.Perm.get_toLabel {n : Nat} (p : Perm n) (i : Fin n) : p.toLabel.get i = p.inv.get i

@[simp]

theorem Hex.GraphIso.Perm.toLabel_toPerm {n : Nat} (p : Perm n) : p.toLabel.toPerm = p

@[simp]

theorem Hex.GraphIso.Perm.toPerm_toLabel {n : Nat} (l : Label n) : l.toPerm.toLabel = l