def Hex.Matrix.permutationVectors (n : Nat) : List (Vector (Fin n) n)

Enumerate the permutations of Fin n as length-n vectors.

The recursion uses Hex.Vector.map' rather than Vector.map so that the enumeration, and hence the Leibniz determinant built on it, reduces in the kernel downstream of this module; core's Vector.map delegates to the unexposed Array.map loop and stalls there.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.permutationVectors 0 = [#v[]]

theorem Hex.Matrix.permutationVectors_succ {n : Nat} : permutationVectors (n + 1) = List.flatMap (fun (v : Vector (Fin n) n) => List.map (fun (i : Fin (n + 1)) => insertAt (Fin.last n) (Vector.map Fin.castSucc v) i) (List.finRange (n + 1))) (permutationVectors n)

The size-n+1 enumeration, restated with core's Vector.map.

Symbolic proofs about the enumeration want this form. It is not the defining equation: Hex.Vector.map' and Vector.map are propositionally equal by Hex.Vector.map'_eq_map, not definitionally, which is why unfolding Hex.Matrix.permutationVectors no longer closes these goals by rfl.

Rewriting with this leaves a term core's Vector.map blocks in the kernel, so a proof that finishes with decide +kernel must leave Hex.Matrix.permutationVectors folded rather than reach for it.

def Hex.Matrix.inversionCount {n : Nat} : List (Fin n) → Nat

Count inversions in a permutation written as a list.

Equations

• Hex.Matrix.inversionCount [] = 0
• Hex.Matrix.inversionCount (x_1 :: xs) = List.foldl (fun (acc : Nat) (y : Fin n) => acc + if y < x_1 then 1 else 0) 0 xs + Hex.Matrix.inversionCount xs

theorem Hex.Matrix.permutationVectors_complete {n : Nat} {perm : Vector (Fin n) n} (hnodup : perm.toList.Nodup) : perm ∈ permutationVectors n

Every duplicate-free length-n vector of Fin n appears in permutationVectors n. This gives the completeness half of the local permutation enumeration used by the Leibniz determinant.

theorem Hex.Matrix.permutationVectors_nodup {n : Nat} {perm : Vector (Fin n) n} (hmem : perm ∈ permutationVectors n) : perm.toList.Nodup

Every vector enumerated by permutationVectors n is duplicate-free, so each listed vector really represents a permutation of Fin n.

theorem Hex.Matrix.permutationVectors_nodup_list {n : Nat} : (permutationVectors n).Nodup

The permutation enumeration itself has no duplicate vectors. This lets determinant proofs compare sums over permutationVectors by list permutation rather than by quotienting repeated terms.