Documentation

CslibFrontier.Logics.FirstOrder.Ordered.Division

Bounds, quotients and remainders by fixed literals #

Formulas comparing with a fixed numeral and taking quotient and remainder by a fixed literal divisor, built from the native addition formula and scaleEq. As with natEq, the literal need not be an element of the universe: ltNat L k x holds exactly when the value of x is below k, and the quotient and remainder formulas use only witnesses bounded by their dividend, so they have exact natural-number semantics in every canonical universe.

Main definitions #

Main results #

source
noncomputable def Cslib.Logic.FO.Ordered.ltNat (L : FirstOrder.Language) (k : ℕ) {α : Type u_1} (x : (language L).Term α) :
(language L).Formula α

The value is below a fixed numeral, which need not be an element of the universe.

Instances For
    source
    noncomputable def Cslib.Logic.FO.Ordered.scaleAddEq (L : FirstOrder.Language) (d : ℕ) {α : Type u_1} (x y z : (language L).Term α) :
    (language L).Formula α

    The equation d * x + y = z for a fixed literal d.

    Instances For
      source
      noncomputable def Cslib.Logic.FO.Ordered.divNatEq (L : FirstOrder.Language) (d : ℕ) {α : Type u_1} (x y : (language L).Term α) :
      (language L).Formula α

      y is the quotient of x by the fixed literal d.

      Instances For
        source
        noncomputable def Cslib.Logic.FO.Ordered.modNatEq (L : FirstOrder.Language) (d : ℕ) {α : Type u_1} (x y : (language L).Term α) :
        (language L).Formula α

        y is the remainder of x by the fixed literal d.

        Instances For
          source
          @[simp]
          theorem Cslib.Logic.FO.Ordered.realize_ltNat {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (k : ℕ) (x : (language L).Term α) (v : α → Fin n) :
          (ltNat L k x).Realize v ↔ ↑(FirstOrder.Language.Term.realize v x) < k

          ltNat L k x holds exactly when x denotes a number below k.

          source
          @[simp]
          theorem Cslib.Logic.FO.Ordered.realize_scaleAddEq {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (d : ℕ) (x y z : (language L).Term α) (v : α → Fin n) :
          (scaleAddEq L d x y z).Realize v ↔ d * ↑(FirstOrder.Language.Term.realize v x) + ↑(FirstOrder.Language.Term.realize v y) = ↑(FirstOrder.Language.Term.realize v z)

          scaleAddEq L d x y z holds exactly when d * x + y = z.

          source
          @[simp]
          theorem Cslib.Logic.FO.Ordered.realize_divNatEq {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (hd : 0 < d) (x y : (language L).Term α) (v : α → Fin n) :
          (divNatEq L d x y).Realize v ↔ ↑(FirstOrder.Language.Term.realize v y) = ↑(FirstOrder.Language.Term.realize v x) / d

          divNatEq L d x y holds exactly when y = x / d, for a positive literal d.

          source
          @[simp]
          theorem Cslib.Logic.FO.Ordered.realize_modNatEq {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} {d : ℕ} (hd : 0 < d) (x y : (language L).Term α) (v : α → Fin n) :
          (modNatEq L d x y).Realize v ↔ ↑(FirstOrder.Language.Term.realize v y) = ↑(FirstOrder.Language.Term.realize v x) % d

          modNatEq L d x y holds exactly when y = x % d, for a positive literal d.