Arithmetic on numbers given by formulas

A number is given by a formula ν with a distinguished block of ℓ variables, the position: under a valuation of the other variables, ν holds of the positions of the digits 1, a position being an ℓ-tuple of elements and the positions being ordered lexicographically. This file builds, from such formulas, the formulas of

• the sum (DescriptiveComplexity.Digits.addF), by carry lookahead;
• the double (DescriptiveComplexity.Digits.dblF), a shift by one position;
• the number one (DescriptiveComplexity.Digits.oneF);

and identifies what they hold of (DescriptiveComplexity.Digits.AddSet, DescriptiveComplexity.Digits.DblSet) with the digits of the sum and of the double (DescriptiveComplexity.Digits.addSet_tupBits, DescriptiveComplexity.Digits.dblSet_tupBits). The numbers are read modulo 2 ^ (n ^ ℓ), n being the size of the structure, and the operations are exact modulo that.

The vocabulary N of the formulas is arbitrary; it receives the ordered vocabulary through a map ι, along which the order formulas of DescriptiveComplexity.OrderWalk are read.

Sets of positions

def DescriptiveComplexity.Digits.tupBits {A : Type} [LinearOrder A] {ℓ : ℕ} (n : ℕ) (p : Fin ℓ → A) : Prop

The positions of the digits 1 of a number, the positions being the ℓ-tuples in lexicographic order.

Equations

• DescriptiveComplexity.Digits.tupBits n p = DescriptiveComplexity.Digits.bitsOf n (toLex p)

def DescriptiveComplexity.Digits.AddSet {A : Type} [LinearOrder A] {ℓ : ℕ} (X Y : (Fin ℓ → A) → Prop) (p : Fin ℓ → A) : Prop

The sum of two sets of positions, by carry lookahead.

Equations

• DescriptiveComplexity.Digits.AddSet X Y p = Xor (Xor (X p) (Y p)) (∃ (q : Fin ℓ → A), toLex q < toLex p ∧ X q ∧ Y q ∧ ∀ (r : Fin ℓ → A), toLex q < toLex r → toLex r < toLex p → X r ∨ Y r)

def DescriptiveComplexity.Digits.DblSet {A : Type} [LinearOrder A] {ℓ : ℕ} (X : (Fin ℓ → A) → Prop) (p : Fin ℓ → A) : Prop

The double of a set of positions: its shift by one position.

Equations

• DescriptiveComplexity.Digits.DblSet X p = ∃ (q : Fin ℓ → A), toLex q ⋖ toLex p ∧ X q

theorem DescriptiveComplexity.Digits.addSet_tupBits {A : Type} [LinearOrder A] {ℓ : ℕ} [Finite A] (m n : ℕ) : AddSet (tupBits m) (tupBits n) = tupBits (m + n)

theorem DescriptiveComplexity.Digits.dblSet_tupBits {A : Type} [LinearOrder A] {ℓ : ℕ} [Finite A] (n : ℕ) : DblSet (tupBits n) = tupBits (2 * n)

The formulas

def DescriptiveComplexity.Digits.xorF {N : FirstOrder.Language} {γ : Type} (φ ψ : N.Formula γ) : N.Formula γ

The exclusive or of two formulas.

Equations

• DescriptiveComplexity.Digits.xorF φ ψ = φ ⊓ FirstOrder.Language.BoundedFormula.not ψ ⊔ ψ ⊓ FirstOrder.Language.BoundedFormula.not φ

def DescriptiveComplexity.Digits.atQ {N : FirstOrder.Language} {ℓ : ℕ} {γ : Type} (ν : N.Formula (γ ⊕ Fin ℓ)) : N.Formula ((γ ⊕ Fin ℓ) ⊕ Fin ℓ)

A number formula, read at the position bound by one more quantifier block.

Equations

• DescriptiveComplexity.Digits.atQ ν = FirstOrder.Language.Formula.relabel (Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr) ν

def DescriptiveComplexity.Digits.atR {N : FirstOrder.Language} {ℓ : ℕ} {γ : Type} (ν : N.Formula (γ ⊕ Fin ℓ)) : N.Formula (((γ ⊕ Fin ℓ) ⊕ Fin ℓ) ⊕ Fin ℓ)

A number formula, read at the position bound by a second quantifier block.

Equations

• DescriptiveComplexity.Digits.atR ν = FirstOrder.Language.Formula.relabel (Sum.elim (Sum.inl ∘ Sum.inl ∘ Sum.inl) Sum.inr) ν

noncomputable def DescriptiveComplexity.Digits.carryF {K N : FirstOrder.Language} (ι : K.sum FirstOrder.Language.order →ᴸ N) {ℓ : ℕ} {γ : Type} (ν₁ ν₂ : N.Formula (γ ⊕ Fin ℓ)) : N.Formula (γ ⊕ Fin ℓ)

The carry into a position: some lower position generates it, and every position in between propagates it.

Equations

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

noncomputable def DescriptiveComplexity.Digits.addF {K N : FirstOrder.Language} (ι : K.sum FirstOrder.Language.order →ᴸ N) {ℓ : ℕ} {γ : Type} (ν₁ ν₂ : N.Formula (γ ⊕ Fin ℓ)) : N.Formula (γ ⊕ Fin ℓ)

The sum of two numbers.

Equations

• DescriptiveComplexity.Digits.addF ι ν₁ ν₂ = DescriptiveComplexity.Digits.xorF (DescriptiveComplexity.Digits.xorF ν₁ ν₂) (DescriptiveComplexity.Digits.carryF ι ν₁ ν₂)

noncomputable def DescriptiveComplexity.Digits.dblF {K N : FirstOrder.Language} (ι : K.sum FirstOrder.Language.order →ᴸ N) {ℓ : ℕ} {γ : Type} (ν : N.Formula (γ ⊕ Fin ℓ)) : N.Formula (γ ⊕ Fin ℓ)

The double of a number.

Equations

• DescriptiveComplexity.Digits.dblF ι ν = FirstOrder.Language.Formula.iExs (Fin ℓ) (ι.onFormula (DescriptiveComplexity.succTupF Sum.inr (Sum.inl ∘ Sum.inr)) ⊓ DescriptiveComplexity.Digits.atQ ν)

theorem DescriptiveComplexity.Digits.realize_xorF {N : FirstOrder.Language} {γ A : Type} [N.Structure A] (φ ψ : N.Formula γ) (v : γ → A) : (xorF φ ψ).Realize v ↔ Xor (φ.Realize v) (ψ.Realize v)

theorem DescriptiveComplexity.Digits.realize_atQ {N : FirstOrder.Language} {ℓ : ℕ} {γ A : Type} [N.Structure A] (ν : N.Formula (γ ⊕ Fin ℓ)) (g : γ → A) (p q : Fin ℓ → A) : (atQ ν).Realize (Sum.elim (Sum.elim g p) q) ↔ ν.Realize (Sum.elim g q)

theorem DescriptiveComplexity.Digits.realize_atR {N : FirstOrder.Language} {ℓ : ℕ} {γ A : Type} [N.Structure A] (ν : N.Formula (γ ⊕ Fin ℓ)) (g : γ → A) (p q r : Fin ℓ → A) : (atR ν).Realize (Sum.elim (Sum.elim (Sum.elim g p) q) r) ↔ ν.Realize (Sum.elim g r)

A quantifier block before the position

noncomputable def DescriptiveComplexity.Digits.exMid {N : FirstOrder.Language} {γ : Type} {ℓ m : ℕ} (ξ : N.Formula ((γ ⊕ Fin m) ⊕ Fin ℓ)) : N.Formula (γ ⊕ Fin ℓ)

Existential quantification over a block of variables that is not the last one: the position stays last.

Equations

• DescriptiveComplexity.Digits.exMid ξ = FirstOrder.Language.Formula.iExs (Fin m) (FirstOrder.Language.Formula.relabel (Sum.elim (Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr) (Sum.inl ∘ Sum.inr)) ξ)

def DescriptiveComplexity.Digits.weaken {N : FirstOrder.Language} {γ : Type} {ℓ m : ℕ} (ν : N.Formula (γ ⊕ Fin ℓ)) : N.Formula ((γ ⊕ Fin m) ⊕ Fin ℓ)

A formula that does not mention a block of variables.

Equations

• DescriptiveComplexity.Digits.weaken ν = FirstOrder.Language.Formula.relabel (Sum.map Sum.inl id) ν