Documentation

Provenance.Semirings.Nat

Counting m-semiring #

This file shows that ℕ (with standard addition and multiplication) is a commutative m-semiring. The monus is truncated subtraction (Nat.sub). Unlike most provenance semirings, ℕ is neither idempotent nor absorptive.

The natural order is the usual order on natural numbers, and monus coincides with Mathlib's Nat.sub.

source
@[implicit_reducible]
instance instSemiringWithMonusNat :
SemiringWithMonus ℕ

ℕ is a commutative m-semiring. The natural order is the usual order on natural numbers, and the monus is truncated subtraction. The δ operator matches ProvSQL's Counting::delta: the support indicator (0 ↦ 0, positive ↦ 1).

Equations
  • One or more equations did not get rendered due to their size.
source
@[implicit_reducible]
instance instCommSemiringWithMonusNat :
CommSemiringWithMonus ℕ
Equations
source
@[implicit_reducible]
instance instHasAltLinearOrderNat :
HasAltLinearOrder ℕ
Equations
source
theorem Nat.mul_sub_left_distributive :
_root_.mul_sub_left_distributive ℕ
source
theorem Nat.not_idempotent :
¬idempotent ℕ
source
theorem Nat.not_absorptive :
¬absorptive ℕ
source
theorem Nat.charP_zero :
CharP ℕ 0

ℕ has characteristic 0: it satisfies CharZero, hence CharP ℕ 0 via CharP.ofCharZero.

source
theorem Nat.no_hom_from_BoolFunc {X : Type} [Inhabited X] :
∃ (ν : X → ℕ), ¬∃ (φ : BoolFunc X →+* ℕ), ∀ (i : X), φ (BoolFunc.var i) = ν i

There is no semiring homomorphism from BoolFunc X to ℕ sending the variables to arbitrary values: ℕ is not absorptive (1 + 1 = 2 ≠ 1), which contradicts var i + 1 = 1 in BoolFunc X.

source
theorem Nat.counterexample_having :
have t₁ := 1; have t₂ := 1; have t₃ := 1; t₁ * t₂ * (1 - t₃) + t₁ * t₃ * (1 - t₂) + t₂ * t₃ * (1 - t₁) ≠ t₁ * t₂ + t₁ * t₃ + t₂ * t₃

Over ℕ, the two natural expansions of HAVING (count = 2) for a three-tuple group, (t₁ ⊗ t₂) ⊗ (𝟙 ⊖ t₃) ⊕ (t₁ ⊗ t₃) ⊗ (𝟙 ⊖ t₂) ⊕ (t₂ ⊗ t₃) ⊗ (𝟙 ⊖ t₁) and (t₁ ⊗ t₂) ⊕ (t₁ ⊗ t₃) ⊕ (t₂ ⊗ t₃), differ. With t₁ = t₂ = t₃ = 1, the first expression evaluates to 0 while the second evaluates to 3.