Finite structures as concrete data

FirstOrder.Language.FinStruct: a finite structure over a finitely presented relational vocabulary, as a piece of data a machine can hold – a universe Fin (n + 1) and a list of Boolean tables, one per relation symbol. This is the passage from isomorphism classes to a Primcodable type that ComputablePred needs, and it is built once for the whole catalog rather than per problem.

The two ingredients

• FirstOrder.Language.FinVocab L: the vocabulary L presented as data – finitely many relation symbols, numbered by Fin numSyms, with their arities. Every vocabulary of the catalog qualifies.
• FirstOrder.Language.FinStruct V: a universe size and a table. The universe is Fin (univSize + 1), hence nonempty by construction: complexity notions in this library read a problem only on nonempty finite structures, and Fin (n + 1) is moreover already linearly ordered, which is what an ordered reduction needs (≤ᶠᵒ[≤]) with no order to encode.

The representation decision

The table is a List (List Bool) – one row per symbol, one entry per tuple, tuples numbered little-endian in base card – and not a dependent function (Fin k → Fin n) → Bool. Dependent function tables are pleasant semantically and painful to prove Primrec facts about, and everything downstream of this file is Primrec facts. Out-of-range lookups return false, so every piece of data denotes a structure and no well-formedness side condition ever has to be carried.

Numbering tuples

def FirstOrder.Language.tupleIdx (c : ℕ) : List ℕ → ℕ

The number of a tuple of digits, little-endian in base c.

Equations

• FirstOrder.Language.tupleIdx c [] = 0
• FirstOrder.Language.tupleIdx c (a :: l) = a + c * FirstOrder.Language.tupleIdx c l

def FirstOrder.Language.digitAt (c t j : ℕ) : ℕ

The j-th digit of t in base c.

Equations

• FirstOrder.Language.digitAt c t j = t / c ^ j % c

@[simp]

theorem FirstOrder.Language.tupleIdx_nil (c : ℕ) : tupleIdx c [] = 0

@[simp]

theorem FirstOrder.Language.tupleIdx_cons (c a : ℕ) (l : List ℕ) : tupleIdx c (a :: l) = a + c * tupleIdx c l

theorem FirstOrder.Language.digitAt_lt {c : ℕ} (hc : 0 < c) (t j : ℕ) : digitAt c t j < c

theorem FirstOrder.Language.tupleIdx_lt {c : ℕ} {l : List ℕ} : (∀ a ∈ l, a < c) → tupleIdx c l < c ^ l.length

A tuple of digits in base c numbers below c ^ length.

theorem FirstOrder.Language.digitAt_tupleIdx {c : ℕ} {l : List ℕ} : (∀ a ∈ l, a < c) → ∀ {j : ℕ}, j < l.length → digitAt c (tupleIdx c l) j = l.getD j 0

The digits of the number of a tuple are the tuple back.

theorem FirstOrder.Language.mod_mul_split (c m v : ℕ) : v % (c * m) = v % c + c * (v / c % m)

Splitting a remainder along a product of moduli.

theorem FirstOrder.Language.tupleIdx_ofFn_digitAt (c d v : ℕ) : tupleIdx c (List.ofFn fun (j : Fin d) => digitAt c v ↑j) = v % c ^ d

The number of the tuple of the digits of v is v, up to the number of digits taken. The converse roundtrip of FirstOrder.Language.digitAt_tupleIdx.

Finitely presented vocabularies

structure FirstOrder.Language.FinVocab (L : Language) : Type

A finitely presented relational vocabulary: the relation symbols of L numbered by Fin numSyms, with their arities. Reading a symbol off its number (sym) and numbering a symbol (index) are mutually inverse, so the presentation loses nothing.

Every vocabulary of the catalog is of this shape: Language.turing has 12 symbols of arity at most 2, Language.finsat 14 of arity at most 3. The presentations are closed under Language.sum (FirstOrder.Language.FinVocab.sum), which is what lets the second-order machinery – whose vocabularies are sums of the instance's with a block's – be encoded by the same means.

• numSyms : ℕ

  The number of relation symbols.

• symOf : Fin self.numSyms → (n : ℕ) × L.Relations n

  The symbol with a given number, together with its arity.

• index {n : ℕ} : L.Relations n → Fin self.numSyms

  The number of a symbol.

• symOf_index {n : ℕ} (R : L.Relations n) : self.symOf (self.index R) = ⟨n, R⟩

  Reading back the symbol with the number of a symbol gives it back.

• index_symOf (i : Fin self.numSyms) : self.index (self.symOf i).snd = i

  Numbering the symbol with a given number gives that number back.

@[reducible, inline]

abbrev FirstOrder.Language.FinVocab.arity {L : Language} (V : L.FinVocab) (i : Fin V.numSyms) : ℕ

The arity of the symbol with a given number.

Equations

• V.arity i = (V.symOf i).fst

@[reducible, inline]

abbrev FirstOrder.Language.FinVocab.sym {L : Language} (V : L.FinVocab) (i : Fin V.numSyms) : L.Relations (V.arity i)

The symbol with a given number.

Equations

• V.sym i = (V.symOf i).snd

theorem FirstOrder.Language.FinVocab.arity_index {L : Language} (V : L.FinVocab) {n : ℕ} (R : L.Relations n) : V.arity (V.index R) = n

theorem FirstOrder.Language.FinVocab.sym_index {L : Language} (V : L.FinVocab) {n : ℕ} (R : L.Relations n) : V.sym (V.index R) ≍ R

theorem FirstOrder.Language.FinVocab.index_sym {L : Language} (V : L.FinVocab) (i : Fin V.numSyms) : V.index (V.sym i) = i

theorem FirstOrder.Language.FinVocab.sym_index_eq {L : Language} (V : L.FinVocab) {n : ℕ} (R : L.Relations n) (h : V.arity (V.index R) = n) : h ▸ V.sym (V.index R) = R

The arity of a symbol, as read from its number, is its arity: the shape in which the dependency is discharged in practice.

Concrete finite structures

structure FirstOrder.Language.FinStruct {L : Language} (V : L.FinVocab) : Type

A concrete finite structure over the finitely presented vocabulary V: a universe size and a table of Booleans, one row per relation symbol.

The universe is Fin (univSize + 1), so it is nonempty by construction; the row of an n-ary symbol is read at the number of the tuple, little-endian in base card. Anything out of range reads false, so every pair of a number and a list of lists of Booleans denotes a structure.

• univSize : ℕ

  One less than the size of the universe.

• table : List (List Bool)

  The tables of the relations, one row per symbol.

@[reducible, inline]

abbrev FirstOrder.Language.FinStruct.card {L : Language} {V : L.FinVocab} (s : FinStruct V) : ℕ

The size of the universe of a concrete finite structure.

Equations

• s.card = s.univSize + 1

@[reducible, inline]

abbrev FirstOrder.Language.FinStruct.Univ {L : Language} {V : L.FinVocab} (s : FinStruct V) : Type

The universe of a concrete finite structure: nonempty and linearly ordered by construction.

Equations

• s.Univ = Fin s.card

def FirstOrder.Language.FinStruct.relMapBool {L : Language} {V : L.FinVocab} (s : FinStruct V) {n : ℕ} (R : L.Relations n) (x : Fin n → s.Univ) : Bool

The table lookup: does the relation R hold of the tuple x?

Equations

• s.relMapBool R x = (s.table.getD ↑(V.index R) []).getD (FirstOrder.Language.tupleIdx s.card (List.ofFn fun (j : Fin n) => ↑(x j))) false

theorem FirstOrder.Language.FinStruct.relMapBool_eq {L : Language} {V : L.FinVocab} (s : FinStruct V) {n : ℕ} (R : L.Relations n) (x : Fin n → s.Univ) : s.relMapBool R x = (s.table.getD ↑(V.index R) []).getD (tupleIdx s.card (List.ofFn fun (j : Fin n) => ↑(x j))) false

@[instance_reducible]

instance FirstOrder.Language.FinStruct.instStructure {L : Language} {V : L.FinVocab} [L.IsRelational] (s : FinStruct V) : L.Structure s.Univ

The structure a piece of data denotes.

Equations

• s.instStructure = { funMap := fun {n : ℕ} (f : L.Functions n) => isEmptyElim f, RelMap := fun {n : ℕ} (R : L.Relations n) (x : Fin n → s.Univ) => s.relMapBool R x = true }

theorem FirstOrder.Language.FinStruct.relMap_iff {L : Language} {V : L.FinVocab} [L.IsRelational] (s : FinStruct V) {n : ℕ} (R : L.Relations n) (x : Fin n → s.Univ) : Structure.RelMap R x ↔ s.relMapBool R x = true

@[instance_reducible]

instance FirstOrder.Language.FinStruct.decidableRelMap {L : Language} {V : L.FinVocab} [L.IsRelational] (s : FinStruct V) {n : ℕ} (R : L.Relations n) (x : Fin n → s.Univ) : Decidable (Structure.RelMap R x)

Equations

• s.decidableRelMap R x = instDecidableEqBool (s.relMapBool R x) true

Building a concrete structure from a table

theorem FirstOrder.Language.FinStruct.heq_relArgs {L : Language} {α : Type} {m n : ℕ} (h : m = n) (R : L.Relations m) (R' : L.Relations n) (hR : R ≍ R') (g : {k : ℕ} → L.Relations k → (Fin k → α) → Bool) (y : Fin m → α) (x : Fin n → α) (hy : ∀ (j : Fin m), y j = x (Fin.cast h j)) : g R y = g R' x

Reading a symbol through its number: a Boolean reading of relations, applied to the symbol read back from a number, is the reading of the symbol itself – the one place the arity dependency of FirstOrder.Language.FinVocab has to be discharged.

def FirstOrder.Language.FinStruct.ofTable {L : Language} (V : L.FinVocab) (k : ℕ) (f : {n : ℕ} → L.Relations n → (Fin n → Fin (k + 1)) → Bool) : FinStruct V

The concrete structure over a universe Fin (k + 1) whose relations are given by the Boolean function f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.FinStruct.univSize_ofTable {L : Language} (V : L.FinVocab) (k : ℕ) (f : {n : ℕ} → L.Relations n → (Fin n → Fin (k + 1)) → Bool) : (ofTable V k f).univSize = k

theorem FirstOrder.Language.FinStruct.relMapBool_ofTable {L : Language} (V : L.FinVocab) (k : ℕ) (f : {n : ℕ} → L.Relations n → (Fin n → Fin (k + 1)) → Bool) {n : ℕ} (R : L.Relations n) (x : Fin n → Fin (k + 1)) : (ofTable V k fun {n : ℕ} => f).relMapBool R x = f R x

The table is read back as it was written.

def FirstOrder.Language.FinStruct.ofEquiv {L : Language} [L.IsRelational] {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (Structure.RelMap R x)] (V : L.FinVocab) (k : ℕ) (e : Fin (k + 1) ≃ A) : FinStruct V

Every finite nonempty structure is presented by a table, along a chosen numbering of its universe: ofTable transported along e, with the numbering itself an L-isomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.FinStruct.relMapBool_ofEquiv {L : Language} [L.IsRelational] {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (Structure.RelMap R x)] (V : L.FinVocab) (k : ℕ) (e : Fin (k + 1) ≃ A) {n : ℕ} (R : L.Relations n) (x : Fin n → (ofEquiv V k e).Univ) : (ofEquiv V k e).relMapBool R x = decide (Structure.RelMap R fun (j : Fin n) => e (x j))

The table of FirstOrder.Language.FinStruct.ofEquiv reads the relations of the structure it was built from.

def FirstOrder.Language.FinStruct.equivOfEquiv {L : Language} [L.IsRelational] {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (Structure.RelMap R x)] (V : L.FinVocab) (k : ℕ) (e : Fin (k + 1) ≃ A) : L.Equiv (ofEquiv V k e).Univ A

The numbering used by FirstOrder.Language.FinStruct.ofEquiv is an isomorphism onto the structure it builds.

Equations

• FirstOrder.Language.FinStruct.equivOfEquiv V k e = { toEquiv := e, map_fun' := ⋯, map_rel' := ⋯ }

Concrete instances are a Primcodable type

Everything a machine has to hold about an instance is a natural number and a list of lists of Booleans, so the coding is Mathlib's, with nothing to prove beyond the three projections being primitive recursive.

def FirstOrder.Language.FinStruct.equivProd {L : Language} (V : L.FinVocab) : FinStruct V ≃ ℕ × List (List Bool)

The coding of a concrete finite structure as a pair.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance FirstOrder.Language.FinStruct.instPrimcodable {L : Language} (V : L.FinVocab) : Primcodable (FinStruct V)

Concrete finite structures are a Primcodable type: the object ComputablePred and REPred are defined on.

Equations

• FirstOrder.Language.FinStruct.instPrimcodable V = Primcodable.ofEquiv (ℕ × List (List Bool)) (FirstOrder.Language.FinStruct.equivProd V)

theorem FirstOrder.Language.FinStruct.primrec_equivProd {L : Language} (V : L.FinVocab) : Primrec ⇑(equivProd V)

theorem FirstOrder.Language.FinStruct.primrec_univSize {L : Language} (V : L.FinVocab) : Primrec fun (s : FinStruct V) => s.univSize

theorem FirstOrder.Language.FinStruct.primrec_card {L : Language} (V : L.FinVocab) : Primrec fun (s : FinStruct V) => s.card

theorem FirstOrder.Language.FinStruct.primrec_table {L : Language} (V : L.FinVocab) : Primrec fun (s : FinStruct V) => s.table

theorem FirstOrder.Language.FinStruct.primrec_mk {L : Language} (V : L.FinVocab) : Primrec₂ fun (n : ℕ) (t : List (List Bool)) => { univSize := n, table := t }

def DescriptiveComplexity.DecisionProblem.toPred {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) (V : L.FinVocab) : FirstOrder.Language.FinStruct V → Prop

The set of concrete instances a decision problem denotes. This is the object ComputablePred and REPred are about: a problem is an isomorphism-closed property of finite structures, and the numbering of FirstOrder.Language.FinStruct turns it into a property of a Primcodable type, with nothing to write per problem.

Equations

• P.toPred V s = P.Holds s.Univ

theorem DescriptiveComplexity.toPred_ofEquiv {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) (V : L.FinVocab) {A : Type} [L.Structure A] [(n : ℕ) → (R : L.Relations n) → (x : Fin n → A) → Decidable (FirstOrder.Language.Structure.RelMap R x)] (k : ℕ) (e : Fin (k + 1) ≃ A) : P.toPred V (FirstOrder.Language.FinStruct.ofEquiv V k e) ↔ P.Holds A

The concrete instances capture the problem: a finite nonempty structure is a yes-instance exactly when some – equivalently, any – numbering of it is. Isomorphism-invariance of a decision problem is what makes this true.

theorem DescriptiveComplexity.exists_finStruct {L : FirstOrder.Language} [L.IsRelational] (V : L.FinVocab) (A : Type) [L.Structure A] [Finite A] [Nonempty A] : ∃ (s : FirstOrder.Language.FinStruct V), Nonempty (L.Equiv s.Univ A)

Every finite nonempty structure is isomorphic to a concrete one.