def Hex.PermGroup.Kernel.imagesDistinct (n : Nat) : List Nat → Nat → Bool

Bitset check that l lists distinct values below n, none of them in seen.

Equations

• Hex.PermGroup.Kernel.imagesDistinct n [] x✝ = true
• Hex.PermGroup.Kernel.imagesDistinct n (x_2 :: xs) x✝ = (x_2.blt n && ((x✝.shiftRight x_2).land 1).beq 0 && Hex.PermGroup.Kernel.imagesDistinct n xs (x✝.lor (Nat.shiftLeft 1 x_2)))

def Hex.PermGroup.Kernel.imagesOk (n : Nat) (l : List Nat) : Bool

l is the image list of a permutation of Fin n, checked in time linear in n.

Equations

• Hex.PermGroup.Kernel.imagesOk n l = (l.length.beq n && Hex.PermGroup.Kernel.imagesDistinct n l 0)

def Hex.PermGroup.Kernel.packList (n : Nat) (l : List Nat) : Nat

The packing of an image list.

Equations

• Hex.PermGroup.Kernel.packList n l = Hex.PermGroup.Kernel.packFn (Hex.PermGroup.Kernel.width n) (fun (i : Nat) => l.getD i 0) n

theorem Hex.PermGroup.Kernel.imagesDistinct_spec (n : Nat) (l : List Nat) (seen : Nat) : imagesDistinct n l seen = true → (∀ (x : Nat), x ∈ l → x < n ∧ seen.testBit x = false) ∧ l.Nodup

theorem Hex.PermGroup.Kernel.imagesOk_spec {n : Nat} {l : List Nat} (h : imagesOk n l = true) : l.length = n ∧ (∀ (x : Nat), x ∈ l → x < n) ∧ l.Nodup

theorem Hex.PermGroup.Kernel.mem_of_imagesOk {n : Nat} {l : List Nat} (h : imagesOk n l = true) {i : Nat} (hi : i < n) : i ∈ l

Every value below n occurs in an accepted image list.

theorem Hex.PermGroup.Kernel.ofNatArray_permOfImages {n : Nat} {l : List Nat} (h : imagesOk n l = true) : ∃ (p : Perm n), Perm.ofNatArray? n l.toArray = some p

theorem Hex.PermGroup.Kernel.val_get_of_ofNatArray? {n : Nat} {a : Array Nat} {p : Perm n} (h : Perm.ofNatArray? n a = some p) (i : Fin n) : ↑(p.get i) = a[↑i]!

The entries of a checked raw permutation array.

theorem Hex.PermGroup.Kernel.pack_ofImages {n : Nat} {l : List Nat} (h : imagesOk n l = true) : pack (Perm.ofImages n l) = packList n l