Composition of ordered first-order reductions

Transitivity of P ≤ᶠᵒ[≤] Q (DescriptiveComplexity.OrderedFOReduction.trans), and the mixed variants with plain FO reductions.

The obstacle to composing two ordered reductions with the plain composition of DescriptiveComplexity.Composition is that the outer reduction's formulas mention the order of the intermediate structure, which is not part of the inner interpretation's output. The fix is classical: the interpreted universe Tag × A^dim carries a linear order that is first-order definable from the order of A – the lexicographic order comparing tags first (by an arbitrary fixed linear order on the finite tag type; tag comparisons are static, i.e., resolved at formula-construction time), then the tuple coordinates in order.

Concretely:

• DescriptiveComplexity.tagTupleLe is the lexicographic order on Tag × (Fin d → A), bundled as DescriptiveComplexity.tagTupleOrder : LinearOrder (Tag × (Fin d → A)) (via Mathlib's Prod.Lex and Pi.Lex);
• DescriptiveComplexity.lexLeF is the corresponding first-order formula over the ordered expansion, with realization lemma DescriptiveComplexity.realize_lexLeF;
• DescriptiveComplexity.FOInterpretation.ordExtend extends an interpretation with target L₂ to one with target L₂.sum Language.order, interpreting the order symbol by lexLeF; the interpreted structure is isomorphic to the original one equipped with the lexicographic order (DescriptiveComplexity.FOInterpretation.ordExtendLEquiv);
• DescriptiveComplexity.OrderedFOReduction.trans composes the outer interpretation with the extended inner one, using FOInterpretation.comp;
• DescriptiveComplexity.FOReduction.toOrdered upgrades a plain FO reduction to an ordered one (lifting its formulas along LHom.sumInl), giving the mixed transitivity variants DescriptiveComplexity.OrderedFOReduction.trans_fo and DescriptiveComplexity.FOReduction.trans_ordered, and Trans instances for all combinations.

A linear order on any finite type

@[instance_reducible]

noncomputable def DescriptiveComplexity.finiteLinearOrder (T : Type) [Finite T] : LinearOrder T

An arbitrary linear order on a finite type, obtained by pulling back the order of Fin n along an arbitrary enumeration. Used to order tags.

Equations

• DescriptiveComplexity.finiteLinearOrder T = LinearOrder.lift' ⇑(Fintype.equivFin T) ⋯

The lexicographic order on tagged tuples

def DescriptiveComplexity.tupLeLex {d : ℕ} {A : Type} [LinearOrder A] (x y : Fin d → A) : Prop

Lexicographic comparison of tuples: equality, or agreement up to a position where the left tuple is smaller.

Equations

• DescriptiveComplexity.tupLeLex x y = (x = y ∨ ∃ (j : Fin d), (∀ i < j, x i = y i) ∧ x j < y j)

def DescriptiveComplexity.tagTupleLe {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] (p q : Tag × (Fin d → A)) : Prop

The lexicographic order on tagged tuples: tags first, then the coordinates in order.

Equations

• DescriptiveComplexity.tagTupleLe p q = (p.1 < q.1 ∨ p.1 = q.1 ∧ DescriptiveComplexity.tupLeLex p.2 q.2)

def DescriptiveComplexity.lexEmbed {Tag : Type} {d : ℕ} {A : Type} (p : Tag × (Fin d → A)) : Lex (Tag × Lex (Fin d → A))

Embedding into Mathlib's lexicographic order types.

Equations

• DescriptiveComplexity.lexEmbed p = toLex (p.1, toLex p.2)

theorem DescriptiveComplexity.lexEmbed_injective {Tag : Type} {d : ℕ} {A : Type} : Function.Injective lexEmbed

@[instance_reducible]

noncomputable def DescriptiveComplexity.tagTupleOrder {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] : LinearOrder (Tag × (Fin d → A))

The lexicographic linear order on tagged tuples, lifted along lexEmbed; its ≤ is characterized by tagTupleLe_iff.

Equations

• DescriptiveComplexity.tagTupleOrder = LinearOrder.lift' DescriptiveComplexity.lexEmbed ⋯

theorem DescriptiveComplexity.tagTupleLe_iff_le {Tag : Type} [LinearOrder Tag] {d : ℕ} {A : Type} [LinearOrder A] (p q : Tag × (Fin d → A)) : tagTupleLe p q ↔ p ≤ q

The relation tagTupleLe is the ≤ of tagTupleOrder. (Public companion to the private tagTupleLe_iff, for use in relativized composition.)

First-order formulas for the lexicographic order

def DescriptiveComplexity.oEqF {L : FirstOrder.Language} {α : Type} (x y : α) : (L.sum FirstOrder.Language.order).Formula α

x = y, as a formula over the ordered expansion.

Equations

• DescriptiveComplexity.oEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.oLeF {L : FirstOrder.Language} {α : Type} (x y : α) : (L.sum FirstOrder.Language.order).Formula α

x ≤ y, as a formula over the ordered expansion.

Equations

• DescriptiveComplexity.oLeF x y = FirstOrder.Language.leSymb.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.oLtF {L : FirstOrder.Language} {α : Type} (x y : α) : (L.sum FirstOrder.Language.order).Formula α

x < y, as a formula over the ordered expansion.

Equations

• DescriptiveComplexity.oLtF x y = DescriptiveComplexity.oLeF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.oEqF x y)

noncomputable def DescriptiveComplexity.lexTupleLeF (L : FirstOrder.Language) (d : ℕ) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)

Lexicographic comparison of two d-tuples (the two arguments of a binary relation), as a formula over the ordered expansion.

Equations

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

noncomputable def DescriptiveComplexity.lexLeF (L : FirstOrder.Language) {Tag : Type} [LinearOrder Tag] (d : ℕ) (t₁ t₂ : Tag) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin d)

The full lexicographic comparison of tagged tuples, as a formula over the ordered expansion: the tags are compared statically.

Equations

• DescriptiveComplexity.lexLeF L d t₁ t₂ = if t₁ = t₂ then DescriptiveComplexity.lexTupleLeF L d else if t₁ < t₂ then ⊤ else ⊥

theorem DescriptiveComplexity.realize_lexLeF {L : FirstOrder.Language} {A : Type} [L.Structure A] [LinearOrder A] {Tag : Type} [LinearOrder Tag] {d : ℕ} {t₁ t₂ : Tag} {v : Fin 2 × Fin d → A} : (lexLeF L d t₁ t₂).Realize v ↔ tagTupleLe (t₁, fun (i : Fin d) => v (0, i)) (t₂, fun (i : Fin d) => v (1, i))

Extending an interpretation with the lexicographic order

noncomputable def DescriptiveComplexity.FOInterpretation.ordExtend {L₁ L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (I : FOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) : FOInterpretation (L₁.sum FirstOrder.Language.order) (L₂.sum FirstOrder.Language.order) T d

Extension of an interpretation over an ordered base to one whose target carries the order vocabulary, interpreted by the lexicographic order on tagged tuples.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.FOInterpretation.mapLinearOrder {L₁ L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (I : FOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) (A : Type) [LinearOrder A] : LinearOrder (I.Map A)

The lexicographic linear order on the interpreted universe.

Equations

• I.mapLinearOrder A = DescriptiveComplexity.tagTupleOrder

noncomputable def DescriptiveComplexity.FOInterpretation.ordExtendLEquiv {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] {d : ℕ} (I : FOInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) (A : Type) [L₁.Structure A] [LinearOrder A] : (L₂.sum FirstOrder.Language.order).Equiv (I.ordExtend.Map A) (I.Map A)

The extended interpretation produces exactly the original interpreted structure equipped with the lexicographic order: the identity map is an isomorphism over the ordered expansion of the target language.

Equations

• I.ordExtendLEquiv A = { toEquiv := Equiv.refl (I.ordExtend.Map A), map_fun' := ⋯, map_rel' := ⋯ }

Transitivity

noncomputable def DescriptiveComplexity.OrderedFOReduction.trans {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : OrderedFOReduction P Q) (f : OrderedFOReduction Q R) : OrderedFOReduction P R

Transitivity of ordered FO reductions: if P ≤ᶠᵒ[≤] Q and Q ≤ᶠᵒ[≤] R, then P ≤ᶠᵒ[≤] R. The intermediate structure is ordered by the lexicographic order on tagged tuples, which is first-order definable from the order of the input.

Equations

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

noncomputable def DescriptiveComplexity.FOReduction.toOrdered {L₁ L₂ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} (g : FOReduction P Q) : OrderedFOReduction P Q

A plain FO reduction is in particular an ordered FO reduction: lift its defining formulas to the ordered expansion (they simply ignore the order).

Equations

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

noncomputable def DescriptiveComplexity.OrderedFOReduction.trans_fo {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : OrderedFOReduction P Q) (f : FOReduction Q R) : OrderedFOReduction P R

Mixed transitivity: an ordered FO reduction followed by a plain one.

Equations

• g.trans_fo f = g.trans f.toOrdered

noncomputable def DescriptiveComplexity.FOReduction.trans_ordered {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : FOReduction P Q) (f : OrderedFOReduction Q R) : OrderedFOReduction P R

Mixed transitivity: a plain FO reduction followed by an ordered one.

Equations

• g.trans_ordered f = g.toOrdered.trans f

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemOrderedFOReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans OrderedFOReduction OrderedFOReduction OrderedFOReduction

Trans instance for ordered FO reductions, enabling calc chains.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemOrderedFOReductionFOReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans OrderedFOReduction FOReduction OrderedFOReduction

Mixed transitivity: an ordered FO reduction followed by a plain one.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemFOReductionOrderedFOReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans FOReduction OrderedFOReduction OrderedFOReduction

Mixed transitivity: a plain FO reduction followed by an ordered one.

Equations

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