The order on an expanded universe #

An exponential expansion's sentences see the order of the structure they expand (DescriptiveComplexity.ExpExpansion). To compose an expansion with anything that reads its order – which is what a complete problem for an exponential class needs – that order must in turn be definable by a first-order sentence over the base. It is, and this file builds it: the analogue, one level up, of DescriptiveComplexity.tagTupleOrder and DescriptiveComplexity.FOInterpretation.ordExtend.

The order #

Points of the expanded universe are tagged block assignments. Order them by tag first – statically, by an arbitrary linear order on the finite tag type – and then by reading an assignment as a binary number: ρ is below σ when, at the least atom where they differ, σ holds and ρ does not.

“Atom” here means a relation variable of the block together with a tuple of elements. Arities differ from variable to variable, so the atoms are indexed by a dependent sum; this file avoids it by padding every tuple to the block's maximal arity (DescriptiveComplexity.blockArityBound), which turns the index type into a plain product B.ι × (Fin D → A) – exactly the shape DescriptiveComplexity.tagTupleOrder already orders. Padding loses nothing: an assignment is determined by the atoms it makes true (DescriptiveComplexity.SOBlock.atomSet_injective), since every tuple of the relevant arity is the prefix of some padded tuple.

Layers #

DescriptiveComplexity.setLinearOrder – the binary-number order on the subsets of any finite linearly ordered index type, obtained from Mathlib's Pi.Lex on functions to Bool, so that transitivity and totality are inherited rather than proved.
DescriptiveComplexity.SOBlock.atomSet – an assignment read as such a subset, and its injectivity.
DescriptiveComplexity.ExpExpansion.mapLinearOrder – the two put together with the tag, and transported to the subtype X.Map A.

The defining formula and its realization lemma live in DescriptiveComplexity.Exponential.OrdFormula; this file is the semantics it is proved against.

The binary-number order on subsets of a finite linear order #

source

@[instance_reducible]

noncomputable def DescriptiveComplexity.setLinearOrder (I : Type) [LinearOrder I] [Finite I] :

LinearOrder (I → Prop)

The binary-number order on subsets of a finite linearly ordered index type: one subset is below another when, at the least index where they differ, the second contains it and the first does not. Lifted from Pi.Lex, so the linear-order axioms come for free.

Equations

DescriptiveComplexity.setLinearOrder I = LinearOrder.lift' DescriptiveComplexity.setKey✝ ⋯

Instances For

Dependency graph

source

theorem DescriptiveComplexity.setLinearOrder_lt_iff {I : Type} [LinearOrder I] [Finite I] (S T : I → Prop) :

S < T ↔ ∃ (i : I), (∀ j < i, S j ↔ T j) ∧ ¬S i ∧ T i

What the order says, unfolded.

Dependency graph

An assignment read as a set of padded atoms #

source

@[reducible, inline]

abbrev DescriptiveComplexity.SOBlock.AtomIx (B : SOBlock) (A : Type) :

Type

The index of a padded atom of a block: a relation variable together with a tuple of the block's maximal arity, of which only the first B.arity i coordinates are read. A plain product, deliberately: the honest index type is a dependent sum, and padding trades it for a shape DescriptiveComplexity.tagTupleOrder already orders.

Equations

B.AtomIx A = (B.ι × (Fin (DescriptiveComplexity.blockArityBound B) → A))

Instances For

Dependency graph

source

def DescriptiveComplexity.SOBlock.atomSet (B : SOBlock) {A : Type} (ρ : B.Assignment A) :

B.AtomIx A → Prop

The padded atoms an assignment makes true.

Equations

B.atomSet ρ p = ρ p.1 fun (j : Fin (B.arity p.1)) => p.2 (Fin.castLE ⋯ j)

Instances For

Dependency graph

source

@[instance_reducible]

noncomputable def DescriptiveComplexity.SOBlock.atomIxLinearOrder (B : SOBlock) (A : Type) [LinearOrder A] :

LinearOrder (B.AtomIx A)

The padded atoms are linearly ordered: the relation variable first, in an arbitrary order on the finite index type of the block, then the tuple lexicographically. This is DescriptiveComplexity.tagTupleOrder at Tag := B.ι, written directly as a lift into B.ι ×ₗ Lex (Fin D → A) so that its strict order unfolds by DescriptiveComplexity.prodLex_lt_iff without a detour through DescriptiveComplexity.tagTupleLe.

Equations

B.atomIxLinearOrder A = LinearOrder.lift' (fun (p : B.AtomIx A) => toLex (p.1, toLex p.2)) ⋯

Instances For

Dependency graph

source

def DescriptiveComplexity.SOBlock.atomLt (B : SOBlock) {A : Type} [LinearOrder A] (p q : B.AtomIx A) :

Prop

The order on padded atoms as a plain relation. Consumers use this rather than <: AtomIx is a product, so the product's own order instances would compete with DescriptiveComplexity.SOBlock.atomIxLinearOrder and < would resolve ambiguously. All the instance juggling is confined to this file.

Equations

B.atomLt p q = (p.1 < q.1 ∨ p.1 = q.1 ∧ toLex p.2 < toLex q.2)

Instances For

Dependency graph

source

theorem DescriptiveComplexity.SOBlock.atomIx_lt_iff (B : SOBlock) {A : Type} [LinearOrder A] (p q : B.AtomIx A) :

p < q ↔ B.atomLt p q

What the order on padded atoms is: the plain relation above.

Dependency graph

source

theorem DescriptiveComplexity.SOBlock.atomSet_injective (B : SOBlock) {A : Type} [Nonempty A] :

Function.Injective B.atomSet

An assignment is determined by the padded atoms it makes true: every tuple of the relevant arity is the prefix of a padded tuple, so nothing is lost by the padding.

Dependency graph

source

theorem DescriptiveComplexity.SOBlock.atomSet_lt_iff (B : SOBlock) {A : Type} [LinearOrder A] [Finite A] (ρ σ : B.Assignment A) :

B.atomSet ρ < B.atomSet σ ↔ ∃ (p : B.AtomIx A), (∀ (q : B.AtomIx A), B.atomLt q p → (B.atomSet ρ q ↔ B.atomSet σ q)) ∧ ¬B.atomSet ρ p ∧ B.atomSet σ p

The comparison of two assignments, packaged: the binary-number order on their padded atoms, stated entirely in terms of DescriptiveComplexity.SOBlock.atomLt so that no consumer has to resolve an order instance on a product.

Dependency graph