The k-pebble game between two structures

DescriptiveComplexity.Invariant.Pebble refines a relation between k-tuples of one structure, which is all the Abiteboul–Vianu development needs: it asks which tuples a definition can tell apart. Separating a Boolean query needs the same game played across two structures, and that is what this file builds – the same chain, the same coinduction, the same stabilization, with the two sides now living in different types.

The pieces mirror their one-structure originals one for one: DescriptiveComplexity.EquivK₂ is the limit of DescriptiveComplexity.pebbleStage₂, greatest by DescriptiveComplexity.le_equivK₂, a fixed point on finite types (DescriptiveComplexity.equivK₂_iff, whence the game moves DescriptiveComplexity.EquivK₂.update), and unchanged by expanding both sides with relations it already refines (DescriptiveComplexity.equivK₂_inf_eq) – the lemma that carries invariance through the stages of an induction.

Instantiated at agreement on the atomic type (DescriptiveComplexity.atomicAgreeOn₂) and at bare sets, it collapses: DescriptiveComplexity.equivK₂_bare – over the empty vocabulary, k-tuples of two sets with k elements each are equivalent as soon as they have the same equality pattern, whatever the two sizes. That is the sentence-level counterpart of DescriptiveComplexity.equivK_bare, and the reason a k-variable induction cannot count.

The chain

@[reducible, inline]

abbrev DescriptiveComplexity.PebbleRel₂ (M N : Type) (k : ℕ) : Type

A relation between k-tuples of two types: the positions of the two-structure k-pebble game.

Equations

• DescriptiveComplexity.PebbleRel₂ M N k = ((Fin k → M) → (Fin k → N) → Prop)

def DescriptiveComplexity.PebbleRel₂.Le {M N : Type} {k : ℕ} (E E' : PebbleRel₂ M N k) : Prop

Pointwise implication of two-structure relations.

Equations

• E.Le E' = ∀ (a : Fin k → M) (b : Fin k → N), E a b → E' a b

def DescriptiveComplexity.PebbleBackForth₂ {M N : Type} {k : ℕ} (E : PebbleRel₂ M N k) : PebbleRel₂ M N k

The back-and-forth condition of the two-structure k-pebble game: the pebble the spoiler moves, on either structure, can be answered on the other.

Equations

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

def DescriptiveComplexity.pebbleRefine₂ {M N : Type} {k : ℕ} (E₀ E : PebbleRel₂ M N k) : PebbleRel₂ M N k

One round of refinement.

Equations

• DescriptiveComplexity.pebbleRefine₂ E₀ E a b = (E₀ a b ∧ DescriptiveComplexity.PebbleBackForth₂ E a b)

theorem DescriptiveComplexity.pebbleBackForth₂_mono {M N : Type} {k : ℕ} {E E' : PebbleRel₂ M N k} (h : E.Le E') : (PebbleBackForth₂ E).Le (PebbleBackForth₂ E')

theorem DescriptiveComplexity.pebbleRefine₂_mono {M N : Type} {k : ℕ} (E₀ : PebbleRel₂ M N k) {E E' : PebbleRel₂ M N k} (h : E.Le E') : (pebbleRefine₂ E₀ E).Le (pebbleRefine₂ E₀ E')

def DescriptiveComplexity.pebbleStage₂ {M N : Type} {k : ℕ} (E₀ : PebbleRel₂ M N k) : ℕ → PebbleRel₂ M N k

The descending refinement chain.

Equations

• DescriptiveComplexity.pebbleStage₂ E₀ 0 = fun (x : Fin k → M) (x_1 : Fin k → N) => True
• DescriptiveComplexity.pebbleStage₂ E₀ n.succ = DescriptiveComplexity.pebbleRefine₂ E₀ (DescriptiveComplexity.pebbleStage₂ E₀ n)

def DescriptiveComplexity.EquivK₂ {M N : Type} {k : ℕ} (E₀ : PebbleRel₂ M N k) : PebbleRel₂ M N k

k-pebble equivalence between two structures: the limit of the refinement chain.

Equations

• DescriptiveComplexity.EquivK₂ E₀ a b = ∀ (n : ℕ), DescriptiveComplexity.pebbleStage₂ E₀ n a b

theorem DescriptiveComplexity.pebbleStage₂_succ_le {M N : Type} {k : ℕ} (E₀ : PebbleRel₂ M N k) (n : ℕ) : (pebbleStage₂ E₀ (n + 1)).Le (pebbleStage₂ E₀ n)

theorem DescriptiveComplexity.pebbleStage₂_le_of_le {M N : Type} {k : ℕ} (E₀ : PebbleRel₂ M N k) {m n : ℕ} (hmn : m ≤ n) : (pebbleStage₂ E₀ n).Le (pebbleStage₂ E₀ m)

theorem DescriptiveComplexity.EquivK₂.initial {M N : Type} {k : ℕ} {E₀ : PebbleRel₂ M N k} {a : Fin k → M} {b : Fin k → N} (h : EquivK₂ E₀ a b) : E₀ a b

The limit is below the initial relation.

theorem DescriptiveComplexity.le_equivK₂ {M N : Type} {k : ℕ} {E₀ E : PebbleRel₂ M N k} (h : E.Le (pebbleRefine₂ E₀ E)) : E.Le (EquivK₂ E₀)

Coinduction: a relation below its own refinement is below the limit – how a pair is ever proved equivalent.

Stabilization

theorem DescriptiveComplexity.exists_pebbleStage₂_succ_eq {M N : Type} {k : ℕ} [Finite M] [Finite N] (E₀ : PebbleRel₂ M N k) : ∃ n ≤ Nat.card ((Fin k → M) × (Fin k → N)), pebbleStage₂ E₀ (n + 1) = pebbleStage₂ E₀ n

theorem DescriptiveComplexity.pebbleRefine₂_equivK₂ {M N : Type} {k : ℕ} [Finite M] [Finite N] (E₀ : PebbleRel₂ M N k) : pebbleRefine₂ E₀ (EquivK₂ E₀) = EquivK₂ E₀

On finite structures the limit is a fixed point of the refinement.

theorem DescriptiveComplexity.equivK₂_iff {M N : Type} {k : ℕ} [Finite M] [Finite N] (E₀ : PebbleRel₂ M N k) (a : Fin k → M) (b : Fin k → N) : EquivK₂ E₀ a b ↔ E₀ a b ∧ PebbleBackForth₂ (EquivK₂ E₀) a b

The interface characterization: consumers use this, never the stages.

theorem DescriptiveComplexity.EquivK₂.update {M N : Type} {k : ℕ} {E₀ : PebbleRel₂ M N k} [Finite M] [Finite N] {a : Fin k → M} {b : Fin k → N} (h : EquivK₂ E₀ a b) (i : Fin k) (c : M) : ∃ (d : N), EquivK₂ E₀ (Function.update a i c) (Function.update b i d)

The game move, from the left.

theorem DescriptiveComplexity.EquivK₂.update_right {M N : Type} {k : ℕ} {E₀ : PebbleRel₂ M N k} [Finite M] [Finite N] {a : Fin k → M} {b : Fin k → N} (h : EquivK₂ E₀ a b) (i : Fin k) (d : N) : ∃ (c : M), EquivK₂ E₀ (Function.update a i c) (Function.update b i d)

The game move, from the right.

Monotonicity and expansion

theorem DescriptiveComplexity.pebbleStage₂_mono {M N : Type} {k : ℕ} {E₀ E₀' : PebbleRel₂ M N k} (h : E₀'.Le E₀) (n : ℕ) : (pebbleStage₂ E₀' n).Le (pebbleStage₂ E₀ n)

theorem DescriptiveComplexity.equivK₂_mono {M N : Type} {k : ℕ} {E₀ E₀' : PebbleRel₂ M N k} (h : E₀'.Le E₀) : (EquivK₂ E₀').Le (EquivK₂ E₀)

theorem DescriptiveComplexity.equivK₂_inf_eq {M N : Type} {k : ℕ} [Finite M] [Finite N] {E₀ E₀' : PebbleRel₂ M N k} (hle : E₀'.Le E₀) (hinv : (EquivK₂ E₀).Le E₀') : EquivK₂ E₀' = EquivK₂ E₀

The expansion lemma: refining the initial relation by anything the limit already refines does not change the limit – so expanding both structures by relations the equivalence cannot see leaves it alone.

Agreement on the atomic type, across two structures

def DescriptiveComplexity.atomicAgreeOn₂ {L : FirstOrder.Language} (S : Set ((n : ℕ) × L.Relations n)) (M N : Type) [L.Structure M] [L.Structure N] (k : ℕ) : PebbleRel₂ M N k

Agreement on the atomic type between tuples of two structures: the same equalities between coordinates, and the same base relations of the family S at every selection of coordinates.

Equations

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

The bare case

theorem DescriptiveComplexity.equivK₂_bare {M N : Type} {k : ℕ} [FirstOrder.Language.empty.Structure M] [FirstOrder.Language.empty.Structure N] [Finite M] [Finite N] {S : Set ((n : ℕ) × FirstOrder.Language.empty.Relations n)} (hM : k ≤ Nat.card M) (hN : k ≤ Nat.card N) {v : Fin k → M} {w : Fin k → N} (hpat : ∀ (p q : Fin k), v p = v q ↔ w p = w q) : EquivK₂ (atomicAgreeOn₂ S M N k) v w

Two bare sets with k elements each are indistinguishable by k pebbles: over the empty vocabulary, tuples with the same equality pattern are ≡ᵏ-equivalent across the two sets, however far apart their sizes. The strategy is the one of DescriptiveComplexity.exists_update_pattern, played on both sides at once.