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 alsoNatCast
andSMul
) for classes likeFirstOrder.Language.IsOrdered
. - Define the theory of Presburger arithmetic and prove its properties (quantifier elimination, completeness, etc).
The type of Presburger arithmetic functions, defined as (0, 1, +).
- zero : presburgerFunc 0
- one : presburgerFunc 0
- add : presburgerFunc 2
Instances For
The language of Presburger arithmetic, defined as (0, 1, +).
Equations
- FirstOrder.Language.presburger = { Functions := FirstOrder.presburgerFunc, Relations := fun (x : ℕ) => Empty }
Instances For
Equations
Equations
Equations
@[simp]
noncomputable def
FirstOrder.Language.presburger.sum
{α : Type u_1}
{β : Type u_2}
(s : Finset β)
(f : β → 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
).
Equations
- FirstOrder.Language.presburger.sum s f = (List.map f s.toList).sum
Instances For
Equations
- One or more equations did not get rendered due to their size.
@[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]
:
@[simp]
theorem
FirstOrder.Language.presburger.realize_natCast
{α : Type u_1}
{M : Type u_2}
{v : α → M}
[AddMonoidWithOne M]
{n : ℕ}
:
@[simp]
theorem
FirstOrder.Language.presburger.realize_nsmul
{α : Type u_1}
{t : presburger.Term α}
{M : Type u_2}
{v : α → M}
[AddMonoidWithOne M]
{n : ℕ}
:
@[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 α}
: