structure Why (α : Type) : Type

• carrier : Set (Set α)

theorem Why.ext_iff {α : Type} {x y : Why α} : x = y ↔ x.carrier = y.carrier

theorem Why.ext {α : Type} {x y : Why α} (carrier : x.carrier = y.carrier) : x = y

instance instCoeWhySet {α : Type} : Coe (Why α) (Set (Set α))

Equations

• instCoeWhySet = { coe := Why.carrier }

instance instZeroWhy {α : Type} : Zero (Why α)

Equations

• instZeroWhy = { zero := { carrier := ∅ } }

instance instAddWhy {α : Type} : Add (Why α)

Equations

• instAddWhy = { add := fun (a b : Why α) => { carrier := a.carrier ∪ b.carrier } }

def why_mul {α : Type} (a b : Why α) : Why α

Equations

• why_mul a b = { carrier := {z : Set α | ∃ (x : Set α) (y : Set α), x ∈ a.carrier ∧ y ∈ b.carrier ∧ z = x ∪ y} }

instance instCommSemiringWhy {α : Type} : CommSemiring (Why α)

Equations

• One or more equations did not get rendered due to their size.

instance instSemiringWithMonusWhy {α : Type} : SemiringWithMonus (Why α)

Equations

• One or more equations did not get rendered due to their size.

theorem Why.idempotent {α : Type} : _root_.idempotent (Why α)

theorem Why.not_absorptive {α : Type} (hNotEmpty : ∃ (x : α), ⊤) : ¬absorptive (Why α)

theorem Why.not_mul_sub_left_distributive {α : Type} [Inhabited α] : ¬mul_sub_left_distributive (Why α)

In Why[X], as long as X is non-empty, times is not distributive over monus. Note that this contradicts Amsterdamer, Deutch & Tannen, On the limitations of provenance for queries with differences, table page 4, which claims this semiring satisfies axiom A13.