Presburger arithmetic

This file defines the first-order language of Presburger arithmetic as (0,1,+).

Main Definitions

• FirstOrder.Language.presburger: the language of Presburger arithmetic.

TODO

• Generalize presburger.sum (maybe also NatCast and SMul) for classes like FirstOrder.Language.IsOrdered.
• Define the theory of Presburger arithmetic and prove its properties (quantifier elimination, completeness, etc).

inductive FirstOrder.presburgerFunc : ℕ → Type

The type of Presburger arithmetic functions, defined as (0, 1, +).

• zero : presburgerFunc 0
• one : presburgerFunc 0
• add : presburgerFunc 2

@[implicit_reducible]

instance FirstOrder.instDecidableEqPresburgerFunc {a✝ : ℕ} : DecidableEq (presburgerFunc a✝)

def FirstOrder.instDecidableEqPresburgerFunc.decEq {a✝ : ℕ} (x✝ x✝¹ : presburgerFunc a✝) : Decidable (x✝ = x✝¹)

def FirstOrder.Language.presburger : Language

The language of Presburger arithmetic, defined as (0, 1, +).

@[implicit_reducible]

instance FirstOrder.Language.instIsAlgebraicPresburger : presburger.IsAlgebraic

@[implicit_reducible]

instance FirstOrder.Language.presburger.instZeroTerm {α : Type u_1} : Zero (presburger.Term α)

@[implicit_reducible]

instance FirstOrder.Language.presburger.instOneTerm {α : Type u_1} : One (presburger.Term α)

@[implicit_reducible]

instance FirstOrder.Language.presburger.instAddTerm {α : Type u_1} : Add (presburger.Term α)

@[implicit_reducible]

instance FirstOrder.Language.presburger.instNatCastTerm {α : Type u_1} : NatCast (presburger.Term α)

@[simp]

theorem FirstOrder.Language.presburger.natCast_zero {α : Type u_1} : ↑0 = 0

@[simp]

theorem FirstOrder.Language.presburger.natCast_succ {α : Type u_1} (n : ℕ) : ↑(n + 1) = ↑n + 1

@[implicit_reducible]

instance FirstOrder.Language.presburger.instSMulNatTerm {α : Type u_1} : SMul ℕ (presburger.Term α)

@[simp]

theorem FirstOrder.Language.presburger.zero_nsmul {α : Type u_1} {t : presburger.Term α} : 0 • t = 0

@[simp]

theorem FirstOrder.Language.presburger.succ_nsmul {α : Type u_1} {t : presburger.Term α} {n : ℕ} : (n + 1) • t = n • t + t

noncomputable def FirstOrder.Language.presburger.sum {α : Type u_1} {β : Type u_2} (s : Finset β) (f : β → presburger.Term α) : presburger.Term α

Summation over a finite set of terms in Presburger arithmetic.

It is defined via choice, so the result only makes sense when the structure satisfies commutativity (see realize_sum).

@[implicit_reducible]

instance FirstOrder.Language.presburger.instStructure {M : Type u_2} [Zero M] [One M] [Add M] : presburger.Structure M

@[simp]

theorem FirstOrder.Language.presburger.funMap_zero {M : Type u_2} [Zero M] [One M] [Add M] {v : Fin 0 → M} : Structure.funMap presburgerFunc.zero v = 0

@[simp]

theorem FirstOrder.Language.presburger.funMap_one {M : Type u_2} [Zero M] [One M] [Add M] {v : Fin 0 → M} : Structure.funMap presburgerFunc.one v = 1

@[simp]

theorem FirstOrder.Language.presburger.funMap_add {M : Type u_2} [Zero M] [One M] [Add M] {v : Fin 2 → M} : Structure.funMap presburgerFunc.add v = v 0 + v 1

@[simp]

theorem FirstOrder.Language.presburger.realize_zero {α : Type u_1} {M : Type u_2} {v : α → M} [Zero M] [One M] [Add M] : Term.realize v 0 = 0

@[simp]

theorem FirstOrder.Language.presburger.realize_one {α : Type u_1} {M : Type u_2} {v : α → M} [Zero M] [One M] [Add M] : Term.realize v 1 = 1

@[simp]

theorem FirstOrder.Language.presburger.realize_add {α : Type u_1} {t₁ t₂ : presburger.Term α} {M : Type u_2} {v : α → M} [Zero M] [One M] [Add M] : Term.realize v (t₁ + t₂) = Term.realize v t₁ + Term.realize v t₂

@[simp]

theorem FirstOrder.Language.presburger.realize_natCast {α : Type u_1} {M : Type u_2} {v : α → M} [AddMonoidWithOne M] {n : ℕ} : Term.realize v ↑n = ↑n

@[simp]

theorem FirstOrder.Language.presburger.realize_nsmul {α : Type u_1} {t : presburger.Term α} {M : Type u_2} {v : α → M} [AddMonoidWithOne M] {n : ℕ} : Term.realize v (n • t) = n • Term.realize v t

@[simp]

theorem FirstOrder.Language.presburger.realize_sum {α : Type u_1} {M : Type u_2} {v : α → M} [AddCommMonoidWithOne M] {β : Type u_3} {s : Finset β} {f : β → presburger.Term α} : Term.realize v (sum s f) = ∑ i ∈ s, Term.realize v (f i)