Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The counting semiring is an m-semiring

Lax392996.CountingSemiring · concepts/Lax392996/CountingSemiring.lean · lax-392996

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The counting semiring (N,+,×,0,1)(\mathbb{N}, +, \times, 0, 1) is an m-semiring: its natural order is the usual order on natural numbers, its monus is truncated subtraction, and its operator δ\delta is the support indicator, 00 on 00 and 11 elsewhere. Unlike most provenance semirings it is neither idempotent nor absorptive. Its usual order also serves as the alternative linear order that lets counts share a column with data values.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.Order.Ring.Defs
    2import Mathlib.Algebra.Order.Ring.Canonical
    3import Mathlib.Algebra.Order.Group.Nat
    4import Mathlib.Algebra.Order.Ring.Nat
    5import Lax392996.SemiringsWithMonus
    6
    7/-!
    8---
    9title: The counting semiring is an m-semiring
    10type: definition
    11---
    12The counting semiring (N,+,×,0,1)(\mathbb{N}, +, \times, 0, 1) is an m-semiring: its
    13natural order is the usual order on natural numbers, its monus is truncated
    14subtraction, and its operator δ\delta is the support indicator, 00 on 00
    15and 11 elsewhere. Unlike most provenance semirings it is neither idempotent
    16nor absorptive. Its usual order also serves as the alternative linear order
    17that lets counts share a column with data values.
    18-/
    19
    20namespace Lax392996.CountingSemiring
    21
    22open Lax392996.SemiringsWithMonus
    23
    24/-- The support indicator: `0 ↦ 0`, positive `↦ 1`. -/
    25def Nat.deltaInd (n : ℕ) : ℕ := if n = 0 then 0 else 1
    26
    27/-- `ℕ` is an m-semiring: the natural order is the usual one, the monus is
    28truncated subtraction, and `δ` is the support indicator. -/
    29instance instSemiringWithMonusNat : SemiringWithMonus ℕ where
    30 monus_spec := by
    31 intro a b c
    32 omega
    33 delta := Nat.deltaInd
    34 delta_zero := rfl
    35 delta_natCast_pos := by
    36 intro n hn
    37 simp [Nat.deltaInd, Nat.pos_iff_ne_zero.mp hn]
    38 delta_absorb := by
    39 intro a b
    40 by_cases ha : a = 0
    41 · simp [ha, Nat.deltaInd]
    42 · simp [Nat.deltaInd, ha]
    43
    44instance instHasAltLinearOrderNat : HasAltLinearOrder ℕ where
    45 altOrder := inferInstance
    46
    47end Lax392996.CountingSemiring
    48
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…