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

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

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

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)

@[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)

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

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

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).