Documentation

Provenance.Semirings.Bool

Boolean m-semiring #

This file shows that Bool (with || as addition and && as multiplication) is a commutative m-semiring. It is the simplest m-semiring and serves as the target of the natural homomorphism from BoolFunc X.

The semiring is absorptive (true || a = true), idempotent, and satisfies left-distributivity of multiplication over monus.

source
@[instance_reducible]
instance instZeroBool_provenance :
Zero Bool
Equations
Dependency graph
source
@[instance_reducible]
instance instAddBool_provenance :
Add Bool
Equations
Dependency graph
source
@[instance_reducible]
instance instOneBool_provenance :
One Bool
Equations
Dependency graph
source
@[instance_reducible]
instance instMulBool_provenance :
Mul Bool
Equations
Dependency graph
source
@[instance_reducible]
instance instSubBool_provenance :
Sub Bool
Equations
Dependency graph
source
@[instance_reducible]
instance instCommSemiringBool_provenance :
CommSemiring Bool
Equations
  • One or more equations did not get rendered due to their size.
Dependency graph
source
@[instance_reducible]
instance instSemiringWithMonusBool :
SemiringWithMonus Bool

The Boolean semiring (Bool, ||, &&) is an m-semiring. The natural order is the usual Boolean order (false ≤ true), and the monus is a && !b. The δ operator matches ProvSQL's Boolean::delta: it is the identity.

Equations
  • One or more equations did not get rendered due to their size.
Dependency graph
source
theorem Bool.isDelta_id :
IsDelta id

On 𝔹 the identity is an admissible δ, so it is the one used – the positive half of the choice recorded by the not_isDelta_id theorems of the indicator semirings.

Dependency graph
source
@[instance_reducible]
instance instCommSemiringWithMonusBool :
CommSemiringWithMonus Bool
Equations
Dependency graph
source
theorem Bool.absorptive :
_root_.absorptive Bool
Dependency graph
source
theorem Bool.idempotent :
_root_.idempotent Bool
Dependency graph
source
theorem Bool.mul_sub_left_distributive :
_root_.mul_sub_left_distributive Bool
Dependency graph
source
instance Bool.instCharPZero :
CharP Bool 0

Bool has characteristic 0 in the CharP sense: it is idempotent and nontrivial (true ≠ false), so every positive natural-number cast equals 1 = true. It is not CharZero since the cast ℕ → Bool is not injective.

Dependency graph
source
theorem Bool.homomorphism_from_BoolFunc {X : Type} :
∃ (ν : SemiringWithMonusHom Bool (BoolFunc X)), Function.Injective fun (x : Bool) => ν.toRingHom x

Injective m-semiring homomorphism from Bool to Bool[X]

Dependency graph
source
theorem Bool.homomorphism_to_BoolFunc {X : Type} (ν : X → Bool) :
∃ (h : SemiringWithMonusHom (BoolFunc X) Bool), ∀ (i : X), (fun (x : BoolFunc X) => h.toRingHom x) (BoolFunc.var i) = ν i

For any assignment ν : X → Bool of Boolean variables to Booleans, the evaluation map f ↦ f ν is an m-semiring homomorphism BoolFunc X → Bool sending each variable BoolFunc.var i to ν i.

Dependency graph