Notation classes for lattice operations #
In this file we introduce typeclasses and definitions for lattice operations.
Main definitions #
HasCompl
: type class for theᶜ
notationTop
: type class for the⊤
notationBot
: type class for the⊥
notation
Notations #
xᶜ
: complement in a lattice;x ⊔ y
: supremum/join, which is notation formax x y
;x ⊓ y
: infimum/meet, which is notation formin x y
;
We implement a delaborator that pretty prints max x y
/min x y
as x ⊔ y
/x ⊓ y
if and only if the order on α
does not have a LinearOrder α
instance (where x y : α
).
This is so that in a lattice we can use the same underlying constants max
/min
as in linear orders, while using the more idiomatic notation x ⊔ y
/x ⊓ y
.
Lemmas about the operators ⊔
and ⊓
should use the names sup
and inf
respectively.
The supremum/join operation: x ⊔ y
. It is notation for max x y
and should be used when the type is not a linear order.
Equations
Instances For
The infimum/meet operation: x ⊓ y
. It is notation for min x y
and should be used when the type is not a linear order.
Equations
Instances For
Delaborate max x y
into x ⊔ y
if the type is not a linear order.
Equations
Instances For
Delaborate min x y
into x ⊓ y
if the type is not a linear order.
Equations
Instances For
Syntax typeclass for Heyting negation ¬
.
The difference between HasCompl
and HNot
is that the former belongs to Heyting algebras,
while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but compl
underestimates while HNot
overestimates. In boolean algebras, they are equal.
See hnot_eq_compl
.
- hnot : α → α
Heyting negation
¬