def Hex.GraphIso.Nauty.limbCount (n : Nat) : Nat

The number of 63-bit limbs holding n vertices.

Equations

• Hex.GraphIso.Nauty.limbCount n = (n + 62) / 63

theorem Hex.GraphIso.Nauty.lt_limbCount_mul {n v : Nat} (h : v < n) : v / 63 < limbCount n

theorem Hex.GraphIso.Nauty.limbCount_pos {n : Nat} (h : 0 < n) : 0 < limbCount n

structure Hex.GraphIso.Nauty.Renaming (n : Nat) : Type

A vertex renaming: injective everywhere and range-preserving in both directions. Images under renamings are the equivariance the search theory works with.

• toFun : Nat → Nat

  The underlying vertex map.

• inj (a b : Nat) : self.toFun a = self.toFun b → a = b

  Global injectivity.

• maps (v : Nat) : v < n ↔ self.toFun v < n

  The vertex range is preserved in both directions.

@[instance_reducible]

instance Hex.GraphIso.Nauty.instCoeFunRenamingForallNat {n : Nat} : CoeFun (Renaming n) fun (x : Renaming n) => Nat → Nat

Equations

• Hex.GraphIso.Nauty.instCoeFunRenamingForallNat = { coe := Hex.GraphIso.Nauty.Renaming.toFun }

structure Hex.GraphIso.Nauty.VSet (n : Nat) : Type

A vertex set over n vertices: limbCount n limbs, each an unboxed 63-bit word, with no vertex at or above n.

• limbs : Array Nat

  The limbs, least significant first.

• size_eq : self.limbs.size = limbCount n
• bounded (i : Nat) : self.limbs[i]! < 2 ^ 63
• clear_of_ge (v : Nat) : n ≤ v → self.limbs[v / 63]!.testBit (v % 63) = false

@[inline]

def Hex.GraphIso.Nauty.VSet.mem {n : Nat} (s : VSet n) (v : Nat) : Bool

Membership: the specification lens of the whole interface.

Equations

• s.mem v = s.limbs[v / 63]!.testBit (v % 63)

theorem Hex.GraphIso.Nauty.VSet.mem_lt {n : Nat} {s : VSet n} {v : Nat} (h : s.mem v = true) : v < n

theorem Hex.GraphIso.Nauty.VSet.mem_of_ge {n : Nat} {s : VSet n} {v : Nat} (h : n ≤ v) : s.mem v = false

theorem Hex.GraphIso.Nauty.VSet.limbs_ext {n : Nat} {s t : VSet n} (h : s.limbs = t.limbs) : s = t

@[instance_reducible]

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

Equality compares the limb arrays. Hex.instDecidableEqArray keeps the comparison kernel-reducible across the module boundary.

Equations

• s.instDecidableEq t = if h : s.limbs = t.limbs then isTrue ⋯ else isFalse ⋯

theorem Hex.GraphIso.Nauty.VSet.ext {n : Nat} {s t : VSet n} (h : ∀ (v : Nat), s.mem v = t.mem v) : s = t

Sets with the same members are equal.

theorem Hex.GraphIso.Nauty.VSet.ext_iff {n : Nat} {s t : VSet n} : s = t ↔ ∀ (v : Nat), s.mem v = t.mem v

structure Hex.GraphIso.Nauty.VSet.Wf (n : Nat) (limbs : Array Nat) : Prop

A limb array is well formed for n vertices when it has limbCount n limbs, every limb is a 63-bit word, and no bit at or above n is set. The runtime never checks this. Each operation preserves it by proof.

• size_eq : limbs.size = limbCount n
• bounded (i : Nat) : limbs[i]! < 2 ^ 63
• clear_of_ge (v : Nat) : n ≤ v → limbs[v / 63]!.testBit (v % 63) = false

@[inline]

def Hex.GraphIso.Nauty.VSet.ofLimbs {n : Nat} (limbs : Array Nat) (h : Wf n limbs) : VSet n

Assemble a set from a well-formed limb array.

Equations

• Hex.GraphIso.Nauty.VSet.ofLimbs limbs h = { limbs := limbs, size_eq := ⋯, bounded := ⋯, clear_of_ge := ⋯ }

theorem Hex.GraphIso.Nauty.VSet.wf {n : Nat} (s : VSet n) : Wf n s.limbs

@[simp]

theorem Hex.GraphIso.Nauty.VSet.limbs_ofLimbs {n : Nat} (limbs : Array Nat) (h : Wf n limbs) : (ofLimbs limbs h).limbs = limbs

theorem Hex.GraphIso.Nauty.VSet.mem_ofLimbs {n : Nat} (limbs : Array Nat) (h : Wf n limbs) (v : Nat) : (ofLimbs limbs h).mem v = limbs[v / 63]!.testBit (v % 63)

theorem Hex.GraphIso.Nauty.VSet.wf_replicate_zero {n : Nat} : Wf n (Array.replicate (limbCount n) 0)

def Hex.GraphIso.Nauty.VSet.empty {n : Nat} : VSet n

The empty set.

Equations

• Hex.GraphIso.Nauty.VSet.empty = Hex.GraphIso.Nauty.VSet.ofLimbs (Array.replicate (Hex.GraphIso.Nauty.limbCount n) 0) ⋯

@[instance_reducible]

instance Hex.GraphIso.Nauty.VSet.instInhabited {n : Nat} : Inhabited (VSet n)

Equations

• Hex.GraphIso.Nauty.VSet.instInhabited = { default := Hex.GraphIso.Nauty.VSet.empty }

@[simp]

theorem Hex.GraphIso.Nauty.VSet.mem_empty {n : Nat} (v : Nat) : empty.mem v = false

theorem Hex.GraphIso.Nauty.VSet.eq_empty_iff {n : Nat} {s : VSet n} : s = empty ↔ ∀ (v : Nat), s.mem v = false

theorem Hex.GraphIso.Nauty.VSet.wf_set_or {n : Nat} {limbs : Array Nat} (h : Wf n limbs) {v : Nat} (hv : v < n) : Wf n (limbs.set! (v / 63) (limbs[v / 63]! ||| 1 <<< (v % 63)))

def Hex.GraphIso.Nauty.VSet.insert {n : Nat} (s : VSet n) (v : Nat) : VSet n

Insert a vertex.

Equations

• s.insert v = if hv : v < n then Hex.GraphIso.Nauty.VSet.ofLimbs (s.limbs.set! (v / 63) (s.limbs[v / 63]! ||| 1 <<< (v % 63))) ⋯ else s

theorem Hex.GraphIso.Nauty.VSet.mem_insert {n : Nat} (s : VSet n) (v w : Nat) : (s.insert v).mem w = (s.mem w || v == w && decide (v < n))

theorem Hex.GraphIso.Nauty.VSet.mem_insert_of_lt {n : Nat} (s : VSet n) {v : Nat} (hv : v < n) (w : Nat) : (s.insert v).mem w = (s.mem w || v == w)

theorem Hex.GraphIso.Nauty.VSet.mem_insert_self {n : Nat} (s : VSet n) {v : Nat} (hv : v < n) : (s.insert v).mem v = true

theorem Hex.GraphIso.Nauty.VSet.mem_insert_mono {n : Nat} (s : VSet n) {u : Nat} (w : Nat) (h : s.mem u = true) : (s.insert w).mem u = true

theorem Hex.GraphIso.Nauty.VSet.insert_of_ge {n : Nat} (s : VSet n) {v : Nat} (hv : n ≤ v) : s.insert v = s

theorem Hex.GraphIso.Nauty.VSet.wf_erase_step {n : Nat} {limbs : Array Nat} (h : Wf n limbs) {v : Nat} (hv : v < n) : Wf n (limbs.set! (v / 63) (limbs[v / 63]! ^^^ 1 <<< (v % 63)))

def Hex.GraphIso.Nauty.VSet.erase {n : Nat} (s : VSet n) (v : Nat) : VSet n

Delete a vertex.

Equations

• s.erase v = if hv : v < n then if s.mem v = true then Hex.GraphIso.Nauty.VSet.ofLimbs (s.limbs.set! (v / 63) (s.limbs[v / 63]! ^^^ 1 <<< (v % 63))) ⋯ else s else s

theorem Hex.GraphIso.Nauty.VSet.mem_erase {n : Nat} (s : VSet n) (v w : Nat) : (s.erase v).mem w = (s.mem w && !v == w)

def Hex.GraphIso.Nauty.VSet.zipLimbs {n : Nat} (op : Nat → Nat → Nat) (s t : VSet n) : Array Nat

The limbwise combination of two packed sets. Hex.Array.zipWith' reduces in the kernel where Lean's own Array.zipWith stalls, and compiles to the same loop.

Equations

• Hex.GraphIso.Nauty.VSet.zipLimbs op s t = Hex.Array.zipWith' op s.limbs t.limbs

theorem Hex.GraphIso.Nauty.VSet.size_zipLimbs {n : Nat} (op : Nat → Nat → Nat) (s t : VSet n) : (zipLimbs op s t).size = limbCount n

theorem Hex.GraphIso.Nauty.VSet.getElem!_zipLimbs {n : Nat} (op : Nat → Nat → Nat) (s t : VSet n) (i : Nat) (hi : i < limbCount n) : (zipLimbs op s t)[i]! = op s.limbs[i]! t.limbs[i]!

theorem Hex.GraphIso.Nauty.VSet.getElem!_zipLimbs_of_ge {n : Nat} (op : Nat → Nat → Nat) (s t : VSet n) (i : Nat) (hi : limbCount n ≤ i) : (zipLimbs op s t)[i]! = 0

theorem Hex.GraphIso.Nauty.VSet.getElem!_limbs_of_ge {n : Nat} (s : VSet n) (i : Nat) (hi : limbCount n ≤ i) : s.limbs[i]! = 0

theorem Hex.GraphIso.Nauty.VSet.wf_zipLimbs {n : Nat} (op : Nat → Nat → Nat) (hop : ∀ (a b : Nat), a < 2 ^ 63 → b < 2 ^ 63 → op a b < 2 ^ 63) (hbit : ∀ (a b j : Nat), (op a b).testBit j = true → a.testBit j = true ∨ b.testBit j = true) (s t : VSet n) : Wf n (zipLimbs op s t)

def Hex.GraphIso.Nauty.VSet.inter {n : Nat} (s t : VSet n) : VSet n

Intersection.

Equations

• s.inter t = Hex.GraphIso.Nauty.VSet.ofLimbs (Hex.GraphIso.Nauty.VSet.zipLimbs (fun (x1 x2 : Nat) => x1 &&& x2) s t) ⋯

theorem Hex.GraphIso.Nauty.VSet.mem_inter {n : Nat} (s t : VSet n) (w : Nat) : (s.inter t).mem w = (s.mem w && t.mem w)

def Hex.GraphIso.Nauty.VSet.union {n : Nat} (s t : VSet n) : VSet n

Union.

Equations

• s.union t = Hex.GraphIso.Nauty.VSet.ofLimbs (Hex.GraphIso.Nauty.VSet.zipLimbs (fun (x1 x2 : Nat) => x1 ||| x2) s t) ⋯

theorem Hex.GraphIso.Nauty.VSet.mem_union {n : Nat} (s t : VSet n) (w : Nat) : (s.union t).mem w = (s.mem w || t.mem w)

def Hex.GraphIso.Nauty.VSet.xor {n : Nat} (s t : VSet n) : VSet n

Symmetric difference.

Equations

• s.xor t = Hex.GraphIso.Nauty.VSet.ofLimbs (Hex.GraphIso.Nauty.VSet.zipLimbs (fun (x1 x2 : Nat) => x1 ^^^ x2) s t) ⋯

theorem Hex.GraphIso.Nauty.VSet.mem_xor {n : Nat} (s t : VSet n) (w : Nat) : (s.xor t).mem w = (s.mem w ^^ t.mem w)

theorem Hex.GraphIso.Nauty.VSet.mem_eq {n : Nat} (s : VSet n) (v : Nat) : s.mem v = s.limbs[v / 63]!.testBit (v % 63)

theorem Hex.GraphIso.Nauty.VSet.testBit_limb {n : Nat} (s : VSet n) (i j : Nat) (hj : j < 63) : s.limbs[i]!.testBit j = s.mem (63 * i + j)

theorem Hex.GraphIso.Nauty.VSet.testBit_limb_of_ge {n : Nat} (s : VSet n) (i j : Nat) (hj : 63 ≤ j) : s.limbs[i]!.testBit j = false

theorem Hex.GraphIso.Nauty.VSet.limb_eq_of_mem {n : Nat} {s t : VSet n} (i : Nat) (h : ∀ (j : Nat), j < 63 → s.mem (63 * i + j) = t.mem (63 * i + j)) : s.limbs[i]! = t.limbs[i]!

theorem Hex.GraphIso.Nauty.VSet.limb_eq_zero_iff {n : Nat} (s : VSet n) (i : Nat) : s.limbs[i]! = 0 ↔ ∀ (j : Nat), j < 63 → s.mem (63 * i + j) = false

theorem Hex.GraphIso.Nauty.VSet.mem_of_ge_limbCount {n : Nat} (s : VSet n) {v : Nat} (h : limbCount n ≤ v / 63) : s.mem v = false

theorem Hex.GraphIso.Nauty.VSet.limbs_toList_eq {n : Nat} (s : VSet n) : s.limbs.toList = List.map (fun (i : Nat) => s.limbs[i]!) (List.range (limbCount n))

def Hex.GraphIso.Nauty.VSet.limbMembers {n : Nat} (s : VSet n) (i : Nat) : List Nat

The members of limb i, in order, as vertex numbers.

Equations

• s.limbMembers i = List.map (fun (x : Nat) => 63 * i + x) (List.filter s.limbs[i]!.testBit (List.range 63))

theorem Hex.GraphIso.Nauty.VSet.filter_range'_limb {n : Nat} (s : VSet n) (i : Nat) : List.filter s.mem (List.range' (63 * i) 63) = s.limbMembers i

theorem Hex.GraphIso.Nauty.VSet.filter_range_blocks {n : Nat} (s : VSet n) (k : Nat) : List.filter s.mem (List.range (63 * k)) = List.flatMap s.limbMembers (List.range k)

The members below 63 * k, as the concatenation of the limb blocks.

theorem Hex.GraphIso.Nauty.VSet.filter_range_eq_blocks {n : Nat} (s : VSet n) : List.filter s.mem (List.range n) = List.flatMap s.limbMembers (List.range (limbCount n))

@[specialize #[]]

def Hex.GraphIso.Nauty.VSet.foldLimbs {n : Nat} {α : Sort u_1} (f : Nat → Nat → α → α) (s t : VSet n) (init : α) : α

Fold a function of corresponding limb pairs over all limbs.

Equations

• Hex.GraphIso.Nauty.VSet.foldLimbs f s t init = Hex.GraphIso.Nauty.VSet.foldLimbs.go f s t s.limbs.size 0 init

def Hex.GraphIso.Nauty.VSet.foldLimbs.go {n : Nat} {α : Sort u_1} (f : Nat → Nat → α → α) (s t : VSet n) : Nat → Nat → α → α

Equations

• Hex.GraphIso.Nauty.VSet.foldLimbs.go f s t 0 a✝¹ a✝ = a✝
• Hex.GraphIso.Nauty.VSet.foldLimbs.go f s t fuel.succ a✝¹ a✝ = Hex.GraphIso.Nauty.VSet.foldLimbs.go f s t fuel (a✝¹ + 1) (f s.limbs[a✝¹]! t.limbs[a✝¹]! a✝)

@[specialize #[]]

def Hex.GraphIso.Nauty.VSet.allLimbs {n : Nat} (p : Nat → Nat → Bool) (s t : VSet n) : Bool

Whether every limb satisfies a predicate of the limb pair, with early exit.

Equations

• Hex.GraphIso.Nauty.VSet.allLimbs p s t = Hex.GraphIso.Nauty.VSet.allLimbs.go p s t s.limbs.size 0

def Hex.GraphIso.Nauty.VSet.allLimbs.go {n : Nat} (p : Nat → Nat → Bool) (s t : VSet n) : Nat → Nat → Bool

Equations

• Hex.GraphIso.Nauty.VSet.allLimbs.go p s t 0 a✝ = true
• Hex.GraphIso.Nauty.VSet.allLimbs.go p s t fuel.succ a✝ = (p s.limbs[a✝]! t.limbs[a✝]! && Hex.GraphIso.Nauty.VSet.allLimbs.go p s t fuel (a✝ + 1))

def Hex.GraphIso.Nauty.VSet.card {n : Nat} (s : VSet n) : Nat

The number of members.

Equations

• s.card = Array.foldl (fun (acc x : Nat) => acc + Hex.GraphIso.Nauty.popCount x) 0 s.limbs

def Hex.GraphIso.Nauty.VSet.cardInter {n : Nat} (s t : VSet n) : Nat

card (s.inter t) without materializing the intersection.

Equations

• s.cardInter t = Hex.GraphIso.Nauty.VSet.foldLimbs (fun (a b acc : Nat) => acc + Hex.GraphIso.Nauty.popCount (a &&& b)) s t 0

def Hex.GraphIso.Nauty.VSet.isEmpty {n : Nat} (s : VSet n) : Bool

Emptiness.

Equations

• s.isEmpty = s.limbs.all fun (x : Nat) => x == 0

def Hex.GraphIso.Nauty.VSet.interIsEmpty {n : Nat} (s t : VSet n) : Bool

isEmpty (s.inter t) without materializing the intersection.

Equations

• s.interIsEmpty t = Hex.GraphIso.Nauty.VSet.allLimbs (fun (a b : Nat) => a &&& b == 0) s t

def Hex.GraphIso.Nauty.VSet.subset {n : Nat} (s t : VSet n) : Bool

Containment: every member of s is a member of t.

Equations

• s.subset t = Hex.GraphIso.Nauty.VSet.allLimbs (fun (a b : Nat) => a &&& b == a) s t

def Hex.GraphIso.Nauty.VSet.countBelow {n : Nat} (s : VSet n) (k : Nat) : Nat

The number of members below a bound: the counting specification of card.

Equations

• s.countBelow k = List.countP s.mem (List.range k)

theorem Hex.GraphIso.Nauty.VSet.card_eq_sum {n : Nat} (s : VSet n) : s.card = (List.map (fun (i : Nat) => popCount s.limbs[i]!) (List.range (limbCount n))).sum

theorem Hex.GraphIso.Nauty.VSet.popCount_limb {n : Nat} (s : VSet n) (i : Nat) : popCount s.limbs[i]! = (s.limbMembers i).length

theorem Hex.GraphIso.Nauty.VSet.card_eq_countBelow {n : Nat} (s : VSet n) : s.card = s.countBelow n

theorem Hex.GraphIso.Nauty.VSet.cardInter_eq {n : Nat} (s t : VSet n) : s.cardInter t = (s.inter t).card

theorem Hex.GraphIso.Nauty.VSet.allLimbs_iff {n : Nat} (p : Nat → Nat → Bool) (s t : VSet n) : allLimbs p s t = true ↔ ∀ (i : Nat), i < limbCount n → p s.limbs[i]! t.limbs[i]! = true

theorem Hex.GraphIso.Nauty.VSet.isEmpty_iff {n : Nat} {s : VSet n} : s.isEmpty = true ↔ s = empty

theorem Hex.GraphIso.Nauty.VSet.interIsEmpty_eq {n : Nat} (s t : VSet n) : s.interIsEmpty t = (s.inter t).isEmpty

theorem Hex.GraphIso.Nauty.VSet.subset_iff {n : Nat} {s t : VSet n} : s.subset t = true ↔ ∀ (v : Nat), s.mem v = true → t.mem v = true

theorem Hex.GraphIso.Nauty.VSet.subset_iff_inter {n : Nat} {s t : VSet n} : s.subset t = true ↔ s.inter t = s

def Hex.GraphIso.Nauty.VSet.firstFrom {n : Nat} (s : VSet n) : Nat → Nat → Option Nat

The least vertex at or after limb i, if any.

Equations

• s.firstFrom 0 x✝ = none
• s.firstFrom fuel.succ x✝ = if (s.limbs[x✝]! != 0) = true then some (63 * x✝ + Hex.GraphIso.Nauty.lowBit s.limbs[x✝]!) else s.firstFrom fuel (x✝ + 1)

def Hex.GraphIso.Nauty.VSet.minElem {n : Nat} (s : VSet n) : Nat

The least member, or 0 for the empty set (callers guard on nonemptiness). This is nauty's FIRSTBITNZ over the words.

Equations

• s.minElem = (s.firstFrom s.limbs.size 0).getD 0

def Hex.GraphIso.Nauty.VSet.nextElem {n : Nat} (s : VSet n) (pos : Option Nat) : Option Nat

The least member greater than pos, or none: nauty's nextelement, iterating a set in ascending vertex order. pos = none starts from the least member.

Equations

• One or more equations did not get rendered due to their size.
• s.nextElem none = s.firstFrom s.limbs.size 0

theorem Hex.GraphIso.Nauty.VSet.lowBit_lt_of_lt {x k : Nat} (hx : x < 2 ^ k) (h0 : x ≠ 0) : lowBit x < k

theorem Hex.GraphIso.Nauty.VSet.firstFrom_some {n : Nat} (s : VSet n) (fuel i v : Nat) : s.firstFrom fuel i = some v → s.mem v = true ∧ 63 * i ≤ v ∧ ∀ (w : Nat), 63 * i ≤ w → w < v → s.mem w = false

What a firstFrom hit is: a member at or after the start limb with no member in between.

theorem Hex.GraphIso.Nauty.VSet.firstFrom_none {n : Nat} (s : VSet n) (fuel i : Nat) : s.firstFrom fuel i = none → ∀ (w : Nat), 63 * i ≤ w → w < 63 * (i + fuel) → s.mem w = false

A firstFrom miss: no member from the start limb to the fuel's end.

theorem Hex.GraphIso.Nauty.VSet.firstFrom_full_none {n : Nat} {s : VSet n} (h : s.firstFrom s.limbs.size 0 = none) : s = empty

theorem Hex.GraphIso.Nauty.VSet.mem_minElem {n : Nat} {s : VSet n} (h : s ≠ empty) : s.mem s.minElem = true

theorem Hex.GraphIso.Nauty.VSet.not_mem_of_lt_minElem {n : Nat} {s : VSet n} {v : Nat} (h : v < s.minElem) : s.mem v = false

theorem Hex.GraphIso.Nauty.VSet.minElem_eq_of {n : Nat} {s : VSet n} {d : Nat} (hd : s.mem d = true) (hlow : ∀ (i : Nat), i < d → s.mem i = false) : s.minElem = d

@[simp]

theorem Hex.GraphIso.Nauty.VSet.minElem_empty {n : Nat} : empty.minElem = 0

def Hex.GraphIso.Nauty.VSet.scanStart : Option Nat → Nat

The lower bound of a nextElem scan.

Equations

• Hex.GraphIso.Nauty.VSet.scanStart none = 0
• Hex.GraphIso.Nauty.VSet.scanStart (some p) = p + 1

def Hex.GraphIso.Nauty.VSet.IsNextFrom {n : Nat} (s : VSet n) (a v : Nat) : Prop

The scan property: v is the least member at or after a.

Equations

• s.IsNextFrom a v = (s.mem v = true ∧ a ≤ v ∧ ∀ (w : Nat), a ≤ w → w < v → s.mem w = false)

theorem Hex.GraphIso.Nauty.VSet.IsNextFrom.unique {n : Nat} {s : VSet n} {a v v' : Nat} (h : s.IsNextFrom a v) (h' : s.IsNextFrom a v') : v = v'

theorem Hex.GraphIso.Nauty.VSet.nextElem_some {n : Nat} {s : VSet n} {pos : Option Nat} {v : Nat} (h : s.nextElem pos = some v) : s.IsNextFrom (scanStart pos) v

theorem Hex.GraphIso.Nauty.VSet.nextElem_none {n : Nat} {s : VSet n} {pos : Option Nat} (h : s.nextElem pos = none) (w : Nat) : scanStart pos ≤ w → s.mem w = false

theorem Hex.GraphIso.Nauty.VSet.nextElem_eq_some_iff {n : Nat} {s : VSet n} {pos : Option Nat} {v : Nat} : s.nextElem pos = some v ↔ s.mem v = true ∧ scanStart pos ≤ v ∧ ∀ (w : Nat), scanStart pos ≤ w → w < v → s.mem w = false

theorem Hex.GraphIso.Nauty.VSet.nextElem_eq_none_iff {n : Nat} {s : VSet n} {pos : Option Nat} : s.nextElem pos = none ↔ ∀ (w : Nat), scanStart pos ≤ w → s.mem w = false

theorem Hex.GraphIso.Nauty.VSet.nextElem_mem {n : Nat} {s : VSet n} {pos : Option Nat} {v : Nat} (h : s.nextElem pos = some v) : s.mem v = true

theorem Hex.GraphIso.Nauty.VSet.nextElem_none_eq_minElem {n : Nat} {s : VSet n} (h : s ≠ empty) : s.nextElem none = some s.minElem

def Hex.GraphIso.Nauty.VSet.toList {n : Nat} (s : VSet n) : List Nat

The members in ascending order, one byte-chunked word walk per limb.

Equations

• s.toList = (Hex.GraphIso.Nauty.VSet.toList.go s s.limbs.size 0 []).reverse

def Hex.GraphIso.Nauty.VSet.toList.go {n : Nat} (s : VSet n) : Nat → Nat → List Nat → List Nat

Equations

• Hex.GraphIso.Nauty.VSet.toList.go s 0 a✝¹ a✝ = a✝
• Hex.GraphIso.Nauty.VSet.toList.go s fuel.succ a✝¹ a✝ = Hex.GraphIso.Nauty.VSet.toList.go s fuel (a✝¹ + 1) (Hex.GraphIso.Nauty.toListGo (63 * a✝¹) 63 s.limbs[a✝¹]! a✝)

theorem Hex.GraphIso.Nauty.VSet.toList_eq {n : Nat} (s : VSet n) : s.toList = List.filter s.mem (List.range n)

theorem Hex.GraphIso.Nauty.VSet.mem_toList {n : Nat} {s : VSet n} {v : Nat} : v ∈ s.toList ↔ s.mem v = true

def Hex.GraphIso.Nauty.VSet.rowCmp {n : Nat} (s t : VSet n) : Ordering

The row order.

Equations

• s.rowCmp t = Hex.GraphIso.Nauty.VSet.rowCmp.go s t s.limbs.size 0

def Hex.GraphIso.Nauty.VSet.rowCmp.go {n : Nat} (s t : VSet n) : Nat → Nat → Ordering

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.VSet.rowCmp.go s t 0 a✝ = Ordering.eq

theorem Hex.GraphIso.Nauty.VSet.rowCmp_go_eq_of {n : Nat} {s t : VSet n} (fuel i : Nat) : (∀ (k : Nat), k < fuel → s.limbs[i + k]! = t.limbs[i + k]!) → rowCmp.go s t fuel i = Ordering.eq

The outcome of the limb scan from i with fuel limbs. Equal prefixes give .eq. Otherwise the first differing limb decides, by its least differing bit.

theorem Hex.GraphIso.Nauty.VSet.rowCmp_go_ne_of {n : Nat} {s t : VSet n} (fuel i k : Nat) : k < fuel → (∀ (k' : Nat), k' < k → s.limbs[i + k']! = t.limbs[i + k']!) → s.limbs[i + k]! ≠ t.limbs[i + k]! → rowCmp.go s t fuel i = if s.limbs[i + k]!.testBit (lowBit (s.limbs[i + k]! ^^^ t.limbs[i + k]!)) = true then Ordering.gt else Ordering.lt

theorem Hex.GraphIso.Nauty.VSet.rowCmp_eq_iff {n : Nat} {s t : VSet n} : s.rowCmp t = Ordering.eq ↔ s = t

theorem Hex.GraphIso.Nauty.VSet.rowCmp_gt_iff {n : Nat} {s t : VSet n} : s.rowCmp t = Ordering.gt ↔ ∃ (d : Nat), s.mem d = true ∧ t.mem d = false ∧ ∀ (i : Nat), i < d → s.mem i = t.mem i

theorem Hex.GraphIso.Nauty.VSet.rowCmp_lt_iff {n : Nat} {s t : VSet n} : s.rowCmp t = Ordering.lt ↔ ∃ (d : Nat), s.mem d = false ∧ t.mem d = true ∧ ∀ (i : Nat), i < d → s.mem i = t.mem i

theorem Hex.GraphIso.Nauty.VSet.rowCmp_gt_iff_lt {n : Nat} {s t : VSet n} : s.rowCmp t = Ordering.gt ↔ t.rowCmp s = Ordering.lt

theorem Hex.GraphIso.Nauty.VSet.rowCmp_gt_trans {n : Nat} {s t u : VSet n} (h1 : s.rowCmp t = Ordering.gt) (h2 : t.rowCmp u = Ordering.gt) : s.rowCmp u = Ordering.gt

The row order is transitive.

def Hex.GraphIso.Nauty.VSet.ofFn {n : Nat} (f : Nat → Bool) : VSet n

The set of vertices below n satisfying a predicate.

Equations

• Hex.GraphIso.Nauty.VSet.ofFn f = List.foldl (fun (s : Hex.GraphIso.Nauty.VSet n) (v : Nat) => if f v = true then s.insert v else s) Hex.GraphIso.Nauty.VSet.empty (List.range n)

theorem Hex.GraphIso.Nauty.VSet.mem_foldl_insert_if {n : Nat} (f : Nat → Bool) (l : List Nat) (init : VSet n) (w : Nat) : (List.foldl (fun (s : VSet n) (v : Nat) => if f v = true then s.insert v else s) init l).mem w = (init.mem w || l.contains w && f w && decide (w < n))

Membership after a guarded insertion fold.

theorem Hex.GraphIso.Nauty.VSet.mem_ofFn {n : Nat} (f : Nat → Bool) (v : Nat) : (ofFn f).mem v = (decide (v < n) && f v)

def Hex.GraphIso.Nauty.VSet.ofList {n : Nat} (l : List Nat) : VSet n

The set of the vertices of a list.

Equations

• Hex.GraphIso.Nauty.VSet.ofList l = List.foldl Hex.GraphIso.Nauty.VSet.insert Hex.GraphIso.Nauty.VSet.empty l

theorem Hex.GraphIso.Nauty.VSet.mem_foldl_insert {n : Nat} (l : List Nat) (init : VSet n) (w : Nat) : (List.foldl insert init l).mem w = (init.mem w || l.contains w && decide (w < n))

theorem Hex.GraphIso.Nauty.VSet.mem_ofList {n : Nat} (l : List Nat) (v : Nat) : (ofList l).mem v = (decide (v < n) && l.contains v)

def Hex.GraphIso.Nauty.VSet.ofFnLimb {n : Nat} (f : Nat → Bool) (base : Nat) : Nat → Nat → Nat

One limb of ofFn: Horner accumulation over the limb's vertices, most significant first, so the accumulator stays a scalar throughout.

Equations

• Hex.GraphIso.Nauty.VSet.ofFnLimb f base 0 x✝ = x✝
• Hex.GraphIso.Nauty.VSet.ofFnLimb f base fuel.succ x✝ = Hex.GraphIso.Nauty.VSet.ofFnLimb f base fuel (2 * x✝ + if base + fuel < n ∧ f (base + fuel) = true then 1 else 0)

def Hex.GraphIso.Nauty.VSet.ofFnLimbs {n : Nat} (f : Nat → Bool) : Nat → Array Nat → Array Nat

The limbs of ofFn, least significant first.

Equations

• Hex.GraphIso.Nauty.VSet.ofFnLimbs f 0 x✝ = x✝
• Hex.GraphIso.Nauty.VSet.ofFnLimbs f i.succ x✝ = Hex.GraphIso.Nauty.VSet.ofFnLimbs f i (x✝.push (Hex.GraphIso.Nauty.VSet.ofFnLimb f (63 * x✝.size) 63 0))

theorem Hex.GraphIso.Nauty.VSet.mem_ofFnFast_limbs {n : Nat} (f : Nat → Bool) (v : Nat) : (ofFnLimbs f (limbCount n) #[])[v / 63]!.testBit (v % 63) = (decide (v < n) && f v)

theorem Hex.GraphIso.Nauty.VSet.wf_ofFnLimbs {n : Nat} (f : Nat → Bool) : Wf n (ofFnLimbs f (limbCount n) #[])

def Hex.GraphIso.Nauty.VSet.ofFnFast {n : Nat} (f : Nat → Bool) : VSet n

ofFn built one limb at a time: allocation-free and without the List.range fold.

Equations

• Hex.GraphIso.Nauty.VSet.ofFnFast f = Hex.GraphIso.Nauty.VSet.ofLimbs (Hex.GraphIso.Nauty.VSet.ofFnLimbs f (Hex.GraphIso.Nauty.limbCount n) #[]) ⋯

@[csimp]

theorem Hex.GraphIso.Nauty.VSet.ofFn_eq_ofFnFast : @ofFn = @ofFnFast

def Hex.GraphIso.Nauty.VSet.image {n : Nat} (σ : Nat → Nat) (s : VSet n) : VSet n

The image of a set under a vertex map, dropping targets outside the range: nauty's permset.

Equations

• Hex.GraphIso.Nauty.VSet.image σ s = List.foldl (fun (t : Hex.GraphIso.Nauty.VSet n) (v : Nat) => if s.mem v = true then t.insert (σ v) else t) Hex.GraphIso.Nauty.VSet.empty (List.range n)

theorem Hex.GraphIso.Nauty.VSet.mem_foldl_image {n : Nat} (σ : Nat → Nat) (s : VSet n) (l : List Nat) (init : VSet n) (w : Nat) : (List.foldl (fun (t : VSet n) (v : Nat) => if s.mem v = true then t.insert (σ v) else t) init l).mem w = (init.mem w || l.any fun (v : Nat) => s.mem v && σ v == w && decide (σ v < n))

theorem Hex.GraphIso.Nauty.VSet.mem_image {n : Nat} (σ : Nat → Nat) (s : VSet n) (w : Nat) : (image σ s).mem w = (List.range n).any fun (v : Nat) => s.mem v && σ v == w && decide (σ v < n)

def Hex.GraphIso.Nauty.VSet.imageLimb {n : Nat} (σ : Nat → Nat) (base : Nat) : Nat → Nat → VSet n → VSet n

The set bits of one limb, by repeated lowest-bit extraction, each inserted through σ.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.VSet.imageLimb σ base 0 x✝¹ x✝ = x✝

def Hex.GraphIso.Nauty.VSet.imageFast {n : Nat} (σ : Nat → Nat) (s : VSet n) : VSet n

image walking the set bits of each limb by repeated lowest-bit extraction, so the cost is proportional to the members and the limbs, never to n bit tests.

Equations

• Hex.GraphIso.Nauty.VSet.imageFast σ s = Hex.GraphIso.Nauty.VSet.imageFast.go✝ σ s s.limbs.size 0 Hex.GraphIso.Nauty.VSet.empty

@[csimp]

theorem Hex.GraphIso.Nauty.VSet.image_eq_imageFast : @image = @imageFast

@[inline]

def Hex.GraphIso.Nauty.VSet.permset {n : Nat} (s : VSet n) (perm : Array Nat) : VSet n

The image under a permutation array: nauty's permset.

Equations

• s.permset perm = Hex.GraphIso.Nauty.VSet.image (fun (x : Nat) => perm[x]!) s

@[simp]

theorem Hex.GraphIso.Nauty.VSet.image_empty {n : Nat} (σ : Nat → Nat) : image σ empty = empty

theorem Hex.GraphIso.Nauty.VSet.mem_image_apply {n : Nat} (σ : Renaming n) (s : VSet n) {v : Nat} (hv : v < n) : (image σ.toFun s).mem (σ.toFun v) = s.mem v

Membership transports along a renaming.

theorem Hex.GraphIso.Nauty.VSet.image_insert {n : Nat} (σ : Renaming n) (s : VSet n) {v : Nat} (hv : v < n) : image σ.toFun (s.insert v) = (image σ.toFun s).insert (σ.toFun v)

Images commute with insertion of a vertex.

theorem Hex.GraphIso.Nauty.VSet.image_inter {n : Nat} (σ : Renaming n) (s t : VSet n) : image σ.toFun (s.inter t) = (image σ.toFun s).inter (image σ.toFun t)

Images commute with intersection, for a renaming.

theorem Hex.GraphIso.Nauty.VSet.image_inj {n : Nat} (σ : Renaming n) {s t : VSet n} (h : image σ.toFun s = image σ.toFun t) : s = t

Images under a renaming are injective.

theorem Hex.GraphIso.Nauty.VSet.image_eq_empty_iff {n : Nat} (σ : Renaming n) {s : VSet n} : image σ.toFun s = empty ↔ s = empty

theorem Hex.GraphIso.Nauty.VSet.interIsEmpty_image {n : Nat} (σ : Renaming n) (s t : VSet n) : (image σ.toFun s).interIsEmpty (image σ.toFun t) = s.interIsEmpty t

Emptiness of an intersection is preserved by a renaming.

theorem Hex.GraphIso.Nauty.VSet.subset_image {n : Nat} (σ : Renaming n) (s t : VSet n) : (image σ.toFun s).subset (image σ.toFun t) = s.subset t

Containment is preserved by a renaming.

theorem Hex.GraphIso.Nauty.VSet.card_image {n : Nat} (σ : Renaming n) (s : VSet n) : (image σ.toFun s).card = s.card

The member count is preserved by a renaming.