Documentation

Mathlib.ModelTheory.Arithmetic.Presburger.Basic

Presburger arithmetic #

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

Main Definitions #

TODO #

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

Instances For

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

    Equations
    Instances For
      @[simp]
      @[simp]
      theorem FirstOrder.Language.presburger.natCast_succ {α : Type u_1} (n : ) :
      ↑(n + 1) = n + 1
      @[simp]
      @[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 α) :

      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
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem FirstOrder.Language.presburger.funMap_add {M : Type u_2} [Zero M] [One M] [Add M] {v : Fin 2M} :
        @[simp]
        theorem FirstOrder.Language.presburger.realize_zero {α : Type u_1} {M : Type u_2} {v : αM} [Zero M] [One M] [Add M] :
        @[simp]
        theorem FirstOrder.Language.presburger.realize_one {α : Type u_1} {M : Type u_2} {v : αM} [Zero M] [One M] [Add M] :
        @[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 : } :
        @[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) = is, Term.realize v (f i)