Documentation

Complexity.Logics.FirstOrder.Ordered.BitArithmetic

Native numeral and shift formulas #

Exact binary shifts are definable from BIT and the native addition formula. A separate no-lost-bit condition rejects overflow; matching only the visible output bits would instead define a truncated shift. Numeral formulas work even when their numeral is outside the universe: they then have no satisfying value.

Main definitions #

Main results #

References #

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

Apply the native PLUS formula to three terms.

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

    Equality to a fixed natural numeral, without requiring that numeral to exist.

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

      Multiplication by a fixed literal, expanded as a fixed chain of additions.

      Instances For
        source
        noncomputable def Cslib.Logic.FO.Ordered.powerOfTwo (L : FirstOrder.Language) {α : Type u_1} (p e : (language L).Term α) :
        (language L).Formula α

        Exactly one set bit, at the specified exponent.

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

          The highest set bit of a nonzero numeral.

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

            Exact left shift, with every source set bit required to remain representable.

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

              addEq L x y z holds under v if and only if (x.realize v).val + (y.realize v).val = (z.realize v).val.

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

              natEq L k x holds exactly when x denotes k.

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

              scaleEq L k x z holds under v iff k * (x.realize v).val = (z.realize v).val.

              source
              @[simp]
              theorem Cslib.Logic.FO.Ordered.realize_highestBit {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (x h : (language L).Term α) (v : α → Fin n) :
              (highestBit L x h).Realize v ↔ 2 ^ ↑(FirstOrder.Language.Term.realize v h) ≤ ↑(FirstOrder.Language.Term.realize v x) ∧ ↑(FirstOrder.Language.Term.realize v x) < 2 ^ (↑(FirstOrder.Language.Term.realize v h) + 1)

              highestBit L x h holds under v iff 2 ^ (h.realize v).val ≤ (x.realize v).val and (x.realize v).val < 2 ^ ((h.realize v).val + 1).

              source
              @[simp]
              theorem Cslib.Logic.FO.Ordered.realize_powerOfTwo {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (p e : (language L).Term α) (v : α → Fin n) :
              (powerOfTwo L p e).Realize v ↔ ↑(FirstOrder.Language.Term.realize v p) = 2 ^ ↑(FirstOrder.Language.Term.realize v e)

              powerOfTwo L p e holds exactly when p = 2 ^ e.

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

              shiftLeft L x e z holds exactly when x * 2 ^ e = z; the product is not reduced modulo the universe size.