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

The bitset with bit v set exactly for the members v.

Equations

• s.toNat = Array.foldr (fun (limb acc : Nat) => acc <<< 63 ||| limb) 0 s.limbs

theorem Hex.GraphIso.Nauty.VSet.testBit_toNat {n : Nat} (s : VSet n) (v : Nat) : s.toNat.testBit v = s.mem v

theorem Hex.GraphIso.Nauty.VSet.toNat_lt {n : Nat} (s : VSet n) : s.toNat < 2 ^ n

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

theorem Hex.GraphIso.Nauty.VSet.toNat_empty {n : Nat} : empty.toNat = 0

theorem Hex.GraphIso.Nauty.VSet.toNat_insert {n : Nat} (s : VSet n) (v : Nat) : (s.insert v).toNat = NatSet.insert n s.toNat v

theorem Hex.GraphIso.Nauty.VSet.toNat_erase {n : Nat} (s : VSet n) (v : Nat) : (s.erase v).toNat = NatSet.erase n s.toNat v

theorem Hex.GraphIso.Nauty.VSet.toNat_inter {n : Nat} (s t : VSet n) : (s.inter t).toNat = s.toNat &&& t.toNat

theorem Hex.GraphIso.Nauty.VSet.toNat_union {n : Nat} (s t : VSet n) : (s.union t).toNat = s.toNat ||| t.toNat

theorem Hex.GraphIso.Nauty.VSet.toNat_xor {n : Nat} (s t : VSet n) : (s.xor t).toNat = s.toNat ^^^ t.toNat

theorem Hex.GraphIso.Nauty.VSet.card_eq_popCount {n : Nat} (s : VSet n) : s.card = popCount s.toNat

theorem Hex.GraphIso.Nauty.VSet.cardInter_eq_popCount {n : Nat} (s t : VSet n) : s.cardInter t = popCount (s.toNat &&& t.toNat)

theorem Hex.GraphIso.Nauty.VSet.interIsEmpty_eq_and {n : Nat} (s t : VSet n) : s.interIsEmpty t = (s.toNat &&& t.toNat == 0)

theorem Hex.GraphIso.Nauty.VSet.subset_eq_and {n : Nat} (s t : VSet n) : s.subset t = (s.toNat &&& t.toNat == s.toNat)

theorem Hex.GraphIso.Nauty.VSet.nextElem_toNat {n : Nat} (s : VSet n) (pos : Option Nat) : s.nextElem pos = NatSet.nextElem s.toNat pos

theorem Hex.GraphIso.Nauty.VSet.rowCmp_toNat {n : Nat} (s t : VSet n) : s.rowCmp t = NatSet.rowCmp s.toNat t.toNat

theorem Hex.GraphIso.Nauty.VSet.toNat_image {n : Nat} (σ : Nat → Nat) (s : VSet n) : (image σ s).toNat = NatSet.image n σ s.toNat

theorem Hex.GraphIso.Nauty.VSet.toNat_foldl_insert {n : Nat} (g : Nat → Nat) (l : List Nat) (init : VSet n) : (List.foldl (fun (w : VSet n) (o : Nat) => w.insert (g o)) init l).toNat = List.foldl (fun (w o : Nat) => NatSet.insert n w (g o)) init.toNat l

theorem Hex.GraphIso.Nauty.VSet.toNat_foldl_insert_if {n : Nat} (f : Nat → Bool) (l : List Nat) (init : VSet n) : (List.foldl (fun (s : VSet n) (v : Nat) => if f v = true then s.insert v else s) init l).toNat = List.foldl (fun (s v : Nat) => if f v = true then NatSet.insert n s v else s) init.toNat l

theorem Hex.GraphIso.Nauty.VSet.toNat_ofFn {n : Nat} (f : Nat → Bool) : (ofFn f).toNat = List.foldl (fun (s v : Nat) => if f v = true then NatSet.insert n s v else s) 0 (List.range n)

def Hex.GraphIso.Nauty.VSet.ofNat {n : Nat} (x : Nat) : VSet n

The packed set of a bitset.

Equations

• Hex.GraphIso.Nauty.VSet.ofNat x = Hex.GraphIso.Nauty.VSet.ofFn fun (v : Nat) => x.testBit v

theorem Hex.GraphIso.Nauty.VSet.mem_ofNat {n : Nat} (x v : Nat) : (ofNat x).mem v = (decide (v < n) && x.testBit v)

theorem Hex.GraphIso.Nauty.VSet.toNat_ofNat {n x : Nat} (h : x < 2 ^ n) : (ofNat x).toNat = x

theorem Hex.GraphIso.Nauty.VSet.ofNat_toNat {n : Nat} (s : VSet n) : ofNat s.toNat = s

@[instance_reducible]

instance Hex.GraphIso.Nauty.VSet.instRepr {n : Nat} : Repr (VSet n)

Equations

• Hex.GraphIso.Nauty.VSet.instRepr = { reprPrec := fun (s : Hex.GraphIso.Nauty.VSet n) (x : Nat) => repr s.toNat }