def Hex.Perm.compVec {n : Nat} (p q : Perm n) : Vector (Fin n) n

The image vector of p.comp q, as one pass over q's images.

Equations

• p.compVec q = Vector.mk (Array.map (fun (j : Fin n) => p.vec[j]) q.vec.toArray) ⋯

theorem Hex.Perm.compVec_eq {n : Nat} (p q : Perm n) : p.compVec q = (p.comp q).vec

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

Perm.comp for compiled code.

Equations

• p.compImpl q = { vec := p.compVec q, nodup := ⋯, complete := ⋯ }

@[csimp]

theorem Hex.Perm.comp_eq_compImpl : @comp = @compImpl

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

invVec for compiled code: the same scatter pass as a Fin.foldl, with no intermediate list. It starts from p's own image vector rather than the identity, since the pass writes every position.

Equations

• p.invVecImpl = Fin.foldl n p.scatterStep p.vec

theorem Hex.Perm.scatter_finRange_eq {n : Nat} (p : Perm n) (v w : Vector (Fin n) n) : List.foldl p.scatterStep v (List.finRange n) = List.foldl p.scatterStep w (List.finRange n)

A scatter pass over every point writes every position, so its result does not depend on the starting vector.

@[csimp]

theorem Hex.Perm.invVec_eq_invVecImpl : @invVec = @invVecImpl

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

Perm.inv for compiled code.

Equations

• p.invImpl = { vec := p.invVecImpl, nodup := ⋯, complete := ⋯ }

@[csimp]

theorem Hex.Perm.inv_eq_invImpl : @inv = @invImpl