Flattening lexicographically numbered tuples

An outer coordinate j followed by an inner coordinate i becomes coordinate j * k + i. The first coordinate remains most significant: ranking the inner tuples in base n and then the outer tuple in base n ^ k gives exactly the rank of the flattened base-n tuple.

Main definitions

• Cslib.Logic.FO.Ordered.flattenTuple: outer-then-inner coordinate flattening.

Main results

• Cslib.Logic.FO.Ordered.flattenTuple_finProdFinEquiv: flattening the blocks of a tuple recovers it.
• Cslib.Logic.FO.Ordered.lexRank_flattenTuple: exact preservation of numeric rank.

References

• N. Immerman, Descriptive Complexity, Proposition 1.28 and Remark 1.32.

def Cslib.Logic.FO.Ordered.flattenTuple {α : Type u_1} {k l : ℕ} (x : Fin l → Fin k → α) : Fin (l * k) → α

Flatten nested tuples, placing the outer coordinate before the inner coordinate.

@[simp]

theorem Cslib.Logic.FO.Ordered.flattenTuple_apply {α : Type u_1} {k l : ℕ} (x : Fin l → Fin k → α) (j : Fin l) (i : Fin k) : flattenTuple x (finProdFinEquiv (j, i)) = x j i

Reading flattenTuple x at finProdFinEquiv (j, i) returns x j i.

theorem Cslib.Logic.FO.Ordered.flattenTuple_finProdFinEquiv {α : Type u_1} {k l : ℕ} (x : Fin (l * k) → α) : (flattenTuple fun (j : Fin l) (i : Fin k) => x (finProdFinEquiv (j, i))) = x

Flattening the blocks of a tuple recovers it.

theorem Cslib.Logic.FO.Ordered.flattenTuple_finProdFinEquiv_apply {α : Type u_1} {k l : ℕ} (x : Fin l → Fin k → α) (p : Fin l × Fin k) : flattenTuple x (finProdFinEquiv p) = x p.1 p.2

Reading flattenTuple x at finProdFinEquiv p returns x p.1 p.2.

theorem Cslib.Logic.FO.Ordered.lexRank_flattenTuple {n k l : ℕ} (x : Fin l → Fin k → Fin n) : lexRank (flattenTuple x) = lexRank fun (j : Fin l) => lexEquiv (x j)

Successive arbitrary-base ranks agree with the rank after outer-then-inner flattening.