Walking a finite linear order, first-order

Shared machinery for constructions that traverse a finite linear order – or the lexicographic order on tuples – one step at a time, with each step described by a first-order guard over the ordered expansion L.sum Language.order.

Two clients, one technique. The SO-Horn definition of HORN-SAT (DescriptiveComplexity.Problems.HornSat.Definability) assembles the unbounded body of an input clause by walking the order of its elements; the translation of FO(LFP) into SO-Horn (DescriptiveComplexity.FixedPointHorn) walks the lexicographic order of stage and valuation tuples to derive the complement of a fixed point. Both need the same three ingredients, provided here:

• guards: formulas DescriptiveComplexity.minF, DescriptiveComplexity.maxF, DescriptiveComplexity.succF – being minimal, maximal, the immediate successor – and their tuple analogues DescriptiveComplexity.minTupF, DescriptiveComplexity.maxTupF, DescriptiveComplexity.succTupF for the lexicographic order, with realization lemmas phrased purely in terms of the order of the structure;
• induction: DescriptiveComplexity.order_induction, walking any finite linear order from its minimum along immediate successors – applied not only to the universe of a structure but to lexicographic tuple orders over it;
• the bridge to Lex: the coordinatewise conditions realized by the tuple guards characterize bottom, top and covering (DescriptiveComplexity.tupSucc_iff_covBy…) in Lex (Fin D → A), and DescriptiveComplexity.prodLex_covBy_iff/DescriptiveComplexity.finCovBy_iff do the same for the lexicographic product heading a static index; so a walk described by guards is a walk along covers of a bona fide finite linear order.

Finally DescriptiveComplexity.orank – the rank of an element of a finite linear order, the number of its strict predecessors – converts that walk into arithmetic: rank 0 at the bottom (DescriptiveComplexity.orank_eq_zero), +1 along a cover (DescriptiveComplexity.orank_covBy), Nat.card - 1 at the top (DescriptiveComplexity.orank_isTop). This is how a fixed-point stage indexed by a tuple is matched with the ℕ-indexed stages of DescriptiveComplexity.derivesIn.

Order guards

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

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

Equations

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

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

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

Equations

• DescriptiveComplexity.ltF x y = DescriptiveComplexity.leF x y ⊓ FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.leF y x)

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

The variable x holds a minimum.

Equations

• DescriptiveComplexity.minF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.leF (Sum.inl x) (Sum.inr 0))

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

The variable x holds a maximum.

Equations

• DescriptiveComplexity.maxF x = FirstOrder.Language.Formula.iAlls (Fin 1) (DescriptiveComplexity.leF (Sum.inr 0) (Sum.inl x))

noncomputable def DescriptiveComplexity.succF {L : FirstOrder.Language} {α : Type} (w z : α) : (L.sum FirstOrder.Language.order).Formula α

w holds the immediate predecessor of z.

Equations

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

@[simp]

theorem DescriptiveComplexity.realize_leF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x y : α) : (leF x y).Realize v ↔ v x ≤ v y

@[simp]

theorem DescriptiveComplexity.realize_ltF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x y : α) : (ltF x y).Realize v ↔ v x < v y

@[simp]

theorem DescriptiveComplexity.realize_minF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x : α) : (minF x).Realize v ↔ ∀ (a : A), v x ≤ a

@[simp]

theorem DescriptiveComplexity.realize_maxF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (x : α) : (maxF x).Realize v ↔ ∀ (a : A), a ≤ v x

@[simp]

theorem DescriptiveComplexity.realize_succF {L : FirstOrder.Language} {α A : Type} [L.Structure A] [LinearOrder A] {v : α → A} (w z : α) : (succF w z).Realize v ↔ v w < v z ∧ ∀ (a : A), ¬(v w < a ∧ a < v z)

Immediate predecessors, and induction along a finite linear order

theorem DescriptiveComplexity.exists_succ_of_not_min {A : Type} [LinearOrder A] [Finite A] {z : A} (hz : ¬∀ (a : A), z ≤ a) : ∃ w < z, ∀ (a : A), ¬(w < a ∧ a < z)

In a finite linear order, an element that is not a minimum has an immediate predecessor.

theorem DescriptiveComplexity.order_induction {A : Type} [LinearOrder A] [Finite A] {P : A → Prop} (hmin : ∀ (z : A), (∀ (a : A), z ≤ a) → P z) (hstep : ∀ (w z : A), w < z → (∀ (a : A), ¬(w < a ∧ a < z)) → P w → P z) (z : A) : P z

Induction along a finite linear order: from the minimum, one immediate successor at a time.

theorem DescriptiveComplexity.exists_gt_of_not_max {A : Type} [LinearOrder A] [Finite A] {z : A} (hz : ¬∀ (a : A), a ≤ z) : ∃ (w : A), z < w ∧ ∀ (a : A), ¬(z < a ∧ a < w)

In a finite linear order, an element that is not a maximum has an immediate successor.

theorem DescriptiveComplexity.order_induction_down {A : Type} [LinearOrder A] [Finite A] {P : A → Prop} (hmax : ∀ (z : A), (∀ (a : A), a ≤ z) → P z) (hstep : ∀ (w z : A), w < z → (∀ (a : A), ¬(w < a ∧ a < z)) → P z → P w) (z : A) : P z

Induction along a finite linear order, downwards: from the maximum, one immediate predecessor at a time. This is the direction a scan is proved correct in – a walk that stops at the greatest element knows about the elements above the one it stands on.

The lexicographic successor of a tuple, coordinatewise

def DescriptiveComplexity.TupSucc {D : ℕ} {A : Type} [LinearOrder A] (t t' : Fin D → A) : Prop

The tuple t' is the immediate successor of t in the lexicographic order (most significant coordinate first), stated coordinatewise: the two tuples agree before some position p, at p the second covers the first, and after p the first is all maxima and the second all minima. This is the condition the guard DescriptiveComplexity.succTupF realizes; DescriptiveComplexity.tupSucc_iff_covBy identifies it with covering in Lex (Fin D → A).

Equations

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

Tuple guards, for the lexicographic order

noncomputable def DescriptiveComplexity.minTupF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The variables sel hold a lexicographically minimal tuple: every coordinate is minimal.

Equations

• DescriptiveComplexity.minTupF sel = DescriptiveComplexity.listInf (List.map (fun (p : Fin D) => DescriptiveComplexity.minF (sel p)) (List.finRange D))

noncomputable def DescriptiveComplexity.maxTupF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The variables sel hold a lexicographically maximal tuple.

Equations

• DescriptiveComplexity.maxTupF sel = DescriptiveComplexity.listInf (List.map (fun (p : Fin D) => DescriptiveComplexity.maxF (sel p)) (List.finRange D))

noncomputable def DescriptiveComplexity.succTupF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel sel' : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The tuple held by sel' is the immediate lexicographic successor of the one held by sel.

Equations

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

@[simp]

theorem DescriptiveComplexity.realize_minTupF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel : Fin D → γ) : (minTupF sel).Realize v ↔ ∀ (p : Fin D) (a : A), v (sel p) ≤ a

@[simp]

theorem DescriptiveComplexity.realize_maxTupF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel : Fin D → γ) : (maxTupF sel).Realize v ↔ ∀ (p : Fin D) (a : A), a ≤ v (sel p)

theorem DescriptiveComplexity.realize_succTupF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel sel' : Fin D → γ) : (succTupF sel sel').Realize v ↔ TupSucc (v ∘ sel) (v ∘ sel')

The bridge to Lex: bottom, top and covering, coordinatewise

The tuple guards above speak coordinatewise; the walk they describe is along the finite linear order Lex (Fin D → A). These lemmas identify the two languages. (Lex is a type synonym, so Finite and Nonempty instances are provided for it here.)

instance DescriptiveComplexity.instFiniteLex_descriptiveComplexity {α : Type u_1} [Finite α] : Finite (Lex α)

instance DescriptiveComplexity.instNonemptyLex_descriptiveComplexity {α : Type u_1} [Nonempty α] : Nonempty (Lex α)

theorem DescriptiveComplexity.lex_lt_iff {D : ℕ} {A : Type} [LinearOrder A] {t t' : Fin D → A} : toLex t < toLex t' ↔ ∃ (p : Fin D), (∀ j < p, t j = t' j) ∧ t p < t' p

theorem DescriptiveComplexity.tup_isBot_iff {D : ℕ} {A : Type} [LinearOrder A] {t : Fin D → A} : (∀ (u : Lex (Fin D → A)), toLex t ≤ u) ↔ ∀ (p : Fin D) (a : A), t p ≤ a

A tuple is a lexicographic bottom iff each coordinate is minimal.

theorem DescriptiveComplexity.tup_isTop_iff {D : ℕ} {A : Type} [LinearOrder A] {t : Fin D → A} : (∀ (u : Lex (Fin D → A)), u ≤ toLex t) ↔ ∀ (p : Fin D) (a : A), a ≤ t p

A tuple is a lexicographic top iff each coordinate is maximal.

theorem DescriptiveComplexity.tupSucc_iff_covBy {D : ℕ} {A : Type} [LinearOrder A] {t t' : Fin D → A} : TupSucc t t' ↔ toLex t ⋖ toLex t'

Coordinatewise successors are lexicographic covers: the condition of the guard DescriptiveComplexity.succTupF says exactly that the second tuple covers the first in Lex (Fin D → A).

The lexicographic product with a static head

theorem DescriptiveComplexity.prodLex_le_iff {J B : Type} [LinearOrder J] [LinearOrder B] {a a' : J} {b b' : B} : toLex (a, b) ≤ toLex (a', b') ↔ a < a' ∨ a = a' ∧ b ≤ b'

theorem DescriptiveComplexity.prodLex_lt_iff {J B : Type} [LinearOrder J] [LinearOrder B] {a a' : J} {b b' : B} : toLex (a, b) < toLex (a', b') ↔ a < a' ∨ a = a' ∧ b < b'

theorem DescriptiveComplexity.prodLex_isBot_iff {J B : Type} [LinearOrder J] [LinearOrder B] {a : J} {b : B} : (∀ (u : Lex (J × B)), toLex (a, b) ≤ u) ↔ (∀ (x : J), a ≤ x) ∧ ∀ (y : B), b ≤ y

theorem DescriptiveComplexity.prodLex_isTop_iff {J B : Type} [LinearOrder J] [LinearOrder B] {a : J} {b : B} : (∀ (u : Lex (J × B)), u ≤ toLex (a, b)) ↔ (∀ (x : J), x ≤ a) ∧ ∀ (y : B), y ≤ b

theorem DescriptiveComplexity.prodLex_covBy_iff {J B : Type} [LinearOrder J] [LinearOrder B] [Nonempty B] {a a' : J} {b b' : B} : toLex (a, b) ⋖ toLex (a', b') ↔ a = a' ∧ b ⋖ b' ∨ a ⋖ a' ∧ (∀ (y : B), y ≤ b) ∧ ∀ (y : B), b' ≤ y

Covering in a lexicographic product: either the heads agree and the tails cover, or the heads cover, the first tail is a top and the second a bottom.

theorem DescriptiveComplexity.finCovBy_iff {n : ℕ} {j j' : Fin n} : j ⋖ j' ↔ ↑j + 1 = ↑j'

Covering in Fin n is incrementing the value.

Deciding the lexicographic order of two tuples

DescriptiveComplexity.succTupF walks the lexicographic order; the two guards below decide it, which is what a reduction defining the order of its image has to do. They are stated at arbitrary selectors sel, sel' into a shared variable type, rather than at the fixed layout Fin 2 × Fin D of DescriptiveComplexity.lexTupleLeF, because their consumers compare tuples sitting at arbitrary positions among the free variables.

noncomputable def DescriptiveComplexity.lexSelLtF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel sel' : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The tuple held by sel is lexicographically strictly below the one held by sel': the two agree before some coordinate, at which the first is strictly smaller.

Equations

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

noncomputable def DescriptiveComplexity.lexSelLeF {D : ℕ} {L : FirstOrder.Language} {γ : Type} (sel sel' : Fin D → γ) : (L.sum FirstOrder.Language.order).Formula γ

The tuple held by sel is lexicographically below or equal to the one held by sel'.

Equations

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

@[simp]

theorem DescriptiveComplexity.realize_lexSelLtF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel sel' : Fin D → γ) : (lexSelLtF sel sel').Realize v ↔ toLex (v ∘ sel) < toLex (v ∘ sel')

@[simp]

theorem DescriptiveComplexity.realize_lexSelLeF {D : ℕ} {L : FirstOrder.Language} {γ A : Type} [L.Structure A] [LinearOrder A] {v : γ → A} (sel sel' : Fin D → γ) : (lexSelLeF sel sel').Realize v ↔ toLex (v ∘ sel) ≤ toLex (v ∘ sel')

Reaching an element from below a cover

theorem DescriptiveComplexity.covBy_le_cases {α : Type u_1} [LinearOrder α] {a b c : α} (h : a ⋖ b) (hc : c ≤ b) : c ≤ a ∨ c = b

Whatever is below a cover is below its base, or is the cover itself.

The rank of an element of a finite linear order

noncomputable def DescriptiveComplexity.orank {A : Type} [LinearOrder A] (z : A) : ℕ

The rank of an element of a finite linear order: the number of its strict predecessors. This converts a walk along covers into arithmetic, matching tuple-indexed fixed-point stages with the ℕ-indexed DescriptiveComplexity.derivesIn.

Equations

• DescriptiveComplexity.orank z = {y : A | y < z}.ncard

theorem DescriptiveComplexity.orank_eq_zero {A : Type} [LinearOrder A] {z : A} (hz : ∀ (a : A), z ≤ a) : orank z = 0

A minimum has rank 0.

theorem DescriptiveComplexity.orank_covBy {A : Type} [LinearOrder A] [Finite A] {w z : A} (h : w ⋖ z) : orank z = orank w + 1

Rank increases by one along a cover.

theorem DescriptiveComplexity.orank_le_orank {A : Type} [LinearOrder A] [Finite A] {x y : A} (h : x ≤ y) : orank x ≤ orank y

Rank is monotone.

theorem DescriptiveComplexity.orank_lt_orank {A : Type} [LinearOrder A] [Finite A] {x y : A} (h : x < y) : orank x < orank y

Rank is strictly monotone.

theorem DescriptiveComplexity.orank_le_iff {A : Type} [LinearOrder A] [Finite A] {x y : A} : orank x ≤ orank y ↔ x ≤ y

Rank reflects the order: it is an order isomorphism onto an initial segment of ℕ, which is what lets a walk along the order be replayed as arithmetic.

theorem DescriptiveComplexity.orank_inj_iff {A : Type} [LinearOrder A] [Finite A] {x y : A} : orank x = orank y ↔ x = y

Rank tells elements apart.

theorem DescriptiveComplexity.orank_inj {A : Type} [LinearOrder A] [Finite A] {x y : A} (h : orank x = orank y) : x = y

The rank determines the element.

theorem DescriptiveComplexity.orank_lt_card {A : Type} [LinearOrder A] [Finite A] (x : A) : orank x < Nat.card A

Rank is below the cardinality.

theorem DescriptiveComplexity.exists_orank_eq {A : Type} [LinearOrder A] [Finite A] {m : ℕ} (h : m < Nat.card A) : ∃ (x : A), orank x = m

Every position below the cardinality is a rank: the ranks exhaust the initial segment, by injectivity between two finite types of the same size.

theorem DescriptiveComplexity.orank_isTop {A : Type} [LinearOrder A] [Finite A] {z : A} (hz : ∀ (a : A), a ≤ z) : orank z = Nat.card A - 1

A maximum has rank Nat.card A - 1.