(Generalized) Boolean algebras #
A Boolean algebra is a bounded distributive lattice with a complement operator. Boolean algebras generalize the (classical) logic of propositions and the lattice of subsets of a set.
Generalized Boolean algebras may be less familiar, but they are essentially Boolean algebras which
do not necessarily have a top element (⊤
) (and hence not all elements may have complements). One
example in mathlib is Finset α
, the type of all finite subsets of an arbitrary
(not-necessarily-finite) type α
.
GeneralizedBooleanAlgebra α
is defined to be a distributive lattice with bottom (⊥
) admitting
a relative complement operator, written using "set difference" notation as x \ y
(sdiff x y
).
For convenience, the BooleanAlgebra
type class is defined to extend GeneralizedBooleanAlgebra
so that it is also bundled with a \
operator.
(A terminological point: x \ y
is the complement of y
relative to the interval [⊥, x]
. We do
not yet have relative complements for arbitrary intervals, as we do not even have lattice
intervals.)
Main declarations #
GeneralizedBooleanAlgebra
: a type class for generalized Boolean algebrasBooleanAlgebra
: a type class for Boolean algebras.Prop.booleanAlgebra
: the Boolean algebra instance onProp
Implementation notes #
The sup_inf_sdiff
and inf_inf_sdiff
axioms for the relative complement operator in
GeneralizedBooleanAlgebra
are taken from
Wikipedia.
Stone's paper introducing generalized Boolean algebras does not define a relative
complement operator a \ b
for all a
, b
. Instead, the postulates there amount to an assumption
that for all a, b : α
where a ≤ b
, the equations x ⊔ a = b
and x ⊓ a = ⊥
have a solution
x
. Disjoint.sdiff_unique
proves that this x
is in fact b \ a
.
References #
- https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations
- Postulates for Boolean Algebras and Generalized Boolean Algebras, M.H. Stone
- Lattice Theory: Foundation, George Grätzer
Tags #
generalized Boolean algebras, Boolean algebras, lattices, sdiff, compl
Generalized Boolean algebras #
Some of the lemmas in this section are from:
A generalized Boolean algebra is a distributive lattice with ⊥
and a relative complement
operation \
(called sdiff
, after "set difference") satisfying (a ⊓ b) ⊔ (a \ b) = a
and
(a ⊓ b) ⊓ (a \ b) = ⊥
, i.e. a \ b
is the complement of b
in a
.
This is a generalization of Boolean algebras which applies to Finset α
for arbitrary
(not-necessarily-Fintype
) α
.
Instances
For any a
, b
, (a ⊓ b) ⊔ (a / b) = a
For any a
, b
, (a ⊓ b) ⊓ (a / b) = ⊥
Equations
- GeneralizedBooleanAlgebra.toOrderBot = OrderBot.mk ⋯
Equations
- GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra = GeneralizedCoheytingAlgebra.mk ⋯
Equations
- Prod.instGeneralizedBooleanAlgebra = GeneralizedBooleanAlgebra.mk ⋯ ⋯
Equations
- Pi.instGeneralizedBooleanAlgebra = GeneralizedBooleanAlgebra.mk ⋯ ⋯
Boolean algebras #
A Boolean algebra is a bounded distributive lattice with a complement operator ᶜ
such that
x ⊓ xᶜ = ⊥
and x ⊔ xᶜ = ⊤
. For convenience, it must also provide a set difference operation \
and a Heyting implication ⇨
satisfying x \ y = x ⊓ yᶜ
and x ⇨ y = y ⊔ xᶜ
.
This is a generalization of (classical) logic of propositions, or the powerset lattice.
Since BoundedOrder
, OrderBot
, and OrderTop
are mixins that require LE
to be present at define-time, the extends
mechanism does not work with them.
Instead, we extend using the underlying Bot
and Top
data typeclasses, and replicate the
order axioms of those classes here. A "forgetful" instance back to BoundedOrder
is provided.
Instances
The infimum of x
and xᶜ
is at most ⊥
The supremum of x
and xᶜ
is at least ⊤
⊤
is the greatest element
⊥
is the least element
x \ y
is equal to x ⊓ yᶜ
x ⇨ y
is equal to y ⊔ xᶜ
Equations
- BooleanAlgebra.toBoundedOrder = BoundedOrder.mk
A bounded generalized boolean algebra is a boolean algebra.
Equations
- GeneralizedBooleanAlgebra.toBooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
Equations
- ⋯ = ⋯
Equations
- BooleanAlgebra.toGeneralizedBooleanAlgebra = GeneralizedBooleanAlgebra.mk ⋯ ⋯
Equations
- BooleanAlgebra.toBiheytingAlgebra = BiheytingAlgebra.mk ⋯ ⋯
Equations
- OrderDual.instBooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- Prod.instBooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Pi.instBooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Pullback a GeneralizedBooleanAlgebra
along an injection.
Equations
- Function.Injective.generalizedBooleanAlgebra f hf map_sup map_inf map_bot map_sdiff = GeneralizedBooleanAlgebra.mk ⋯ ⋯
Instances For
Pullback a BooleanAlgebra
along an injection.
Equations
- Function.Injective.booleanAlgebra f hf map_sup map_inf map_top map_bot map_compl map_sdiff map_himp = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
An alternative constructor for boolean algebras: a distributive lattice that is complemented is a boolean algebra.
This is not an instance, because it creates data using choice.
Equations
- DistribLattice.booleanAlgebraOfComplemented α = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯