Numbering tuples over finite universes

These generic helpers number finite tuples without depending on machine encodings. The index uses the first coordinate as the least significant digit, as in Mathlib's finFunctionFinEquiv. The public names and numbering convention are unchanged from their original location in Complexity.Logics.FirstOrder.Encoding, which publicly imports this module.

Main definitions

• Cslib.Logic.tupleIndex: the colexicographic index of a tuple of natural-number digits.
• Cslib.Logic.tupleEquiv: number tuples along an enumeration of their coordinates.

Main results

• Cslib.Logic.tupleIndex_lt_iff: numerical order agrees with the highest differing coordinate.
• Cslib.Logic.tupleIndex_lt_pow_iff: indices below a power have zero higher digits.

References

• N. Immerman, Descriptive Complexity, Remark 1.32, for the distinct lexicographic convention required by ordered first-order queries.

Tuples

def Cslib.Logic.tupleIndex {n k : ℕ} (x : Fin k → Fin n) : ℕ

The index of a tuple of Fin n in the truth table of a relation of arity k: the number ∑ i, x i * n ^ i below n ^ k, the order of finFunctionFinEquiv.

theorem Cslib.Logic.tupleIndex_apply {n k : ℕ} (x : Fin k → Fin n) : tupleIndex x = ∑ i : Fin k, ↑(x i) * n ^ ↑i

tupleIndex x is the base-n sum ∑ i, x i * n ^ i.

theorem Cslib.Logic.tupleIndex_lt {n k : ℕ} (x : Fin k → Fin n) : tupleIndex x < n ^ k

Every k-tuple over Fin n has tupleIndex strictly less than n ^ k.

theorem Cslib.Logic.tupleIndex_injective {n k : ℕ} : Function.Injective tupleIndex

tupleIndex is injective.

def Cslib.Logic.tupleEquiv {ι : Type u_1} {n d : ℕ} (e : ι ≃ Fin d) : (ι → Fin n) ≃ Fin (n ^ d)

Number tuples whose coordinates are enumerated by e, using the same colexicographic indexing as tupleIndex.

@[simp]

theorem Cslib.Logic.tupleEquiv_apply_val {ι : Type u_1} {n d : ℕ} (e : ι ≃ Fin d) (x : ι → Fin n) : ↑((tupleEquiv e) x) = tupleIndex (x ∘ ⇑e.symm)

The numerical value of tupleEquiv e x is tupleIndex (x ∘ e.symm).

@[simp]

theorem Cslib.Logic.tupleEquiv_symm_apply {ι : Type u_1} {n d : ℕ} (e : ι ≃ Fin d) (u : Fin (n ^ d)) (i : ι) : (tupleEquiv e).symm u i = finFunctionFinEquiv.symm u (e i)

(tupleEquiv e).symm u at coordinate i is finFunctionFinEquiv.symm u (e i).

theorem Cslib.Logic.tupleEquiv_symm_apply_val {ι : Type u_1} {n d : ℕ} (e : ι ≃ Fin d) (u : Fin (n ^ d)) (i : ι) : ↑((tupleEquiv e).symm u i) = ↑u / n ^ ↑(e i) % n

The i-th coordinate of (tupleEquiv e).symm u is the (e i)-th base-n digit of u.

theorem Cslib.Logic.tupleIndex_symm {n k : ℕ} (i : Fin (n ^ k)) : tupleIndex (finFunctionFinEquiv.symm i) = ↑i

The tuple with a given index.

theorem Cslib.Logic.tupleIndex_comp_cast {n k l : ℕ} (h : k = l) (x : Fin l → Fin n) : tupleIndex (x ∘ Fin.cast h) = tupleIndex x

Precomposing a tuple with Fin.cast leaves its tupleIndex unchanged.

theorem Cslib.Logic.tupleIndex_snoc {n k : ℕ} (x : Fin (k + 1) → Fin n) : tupleIndex x = tupleIndex (x ∘ Fin.castSucc) + ↑(x (Fin.last k)) * n ^ k

Separate the highest-weight digit (x (Fin.last k) : ℕ) * n ^ k of tupleIndex x.

theorem Cslib.Logic.tupleIndex_eq_of_high_zero {n a k : ℕ} (ha : a ≤ k) {x : Fin k → Fin n} : (∀ (i : Fin k), a ≤ ↑i → ↑(x i) = 0) → tupleIndex x = tupleIndex fun (j : Fin a) => x (Fin.castLE ha j)

When all coordinates of x : Fin k → Fin n at indices ≥ a are zero, tupleIndex x equals the index of its prefix of length a.

theorem Cslib.Logic.tupleIndex_lt_pow_iff {n a k : ℕ} : a ≤ k → ∀ (x : Fin k → Fin n), tupleIndex x < n ^ a ↔ ∀ (i : Fin k), a ≤ ↑i → ↑(x i) = 0

For a ≤ k, a k-tuple has index < n ^ a iff all coordinates at indices ≥ a are zero.

theorem Cslib.Logic.tupleIndex_lt_iff {n k : ℕ} (x y : Fin k → Fin n) : tupleIndex x < tupleIndex y ↔ ∃ (i : Fin k), x i < y i ∧ ∀ (j : Fin k), i < j → x j = y j

The numerical order on tupleIndex is the colexicographic order on Fin k → Fin n (comparing at the most significant coordinate where the tuples differ).