De Morgan and Kleene algebras

This file defines Kleene's law for lattices with an involutive complement. A De Morgan algebra is a bounded distributive lattice with an involutive complement, written [DistribLattice α] [BoundedOrder α] [InvolutiveCompl α] and needing no class of its own. A Kleene algebra adds Kleene's law a ⊓ aᶜ ≤ b ⊔ bᶜ, that contradictions lie below excluded middles; Kalman's "normal" lattices with involution are the distributive lattices satisfying it, with or without bounds. Every Boolean algebra is a Kleene algebra, the law degenerating through ⊥, and the three-element chain SignType is the canonical non-Boolean example.

"Kleene algebra" here is the lattice notion, not the regular-expression star-semiring of mathlib's root KleeneAlgebra. Kalman's construction of Kleene algebras from distributive lattices is in Core/Order/DeMorganAlgebra/Kalman.lean.

Main definitions

• IsKleene: the Kleene law, a Prop mixin over [Lattice α] [InvolutiveCompl α].

Main results

• BooleanAlgebra.toIsKleene: every Boolean algebra is a Kleene algebra.
• Prod and Pi instances of IsKleene.

References

• [Kal58]

class IsKleene (α : Type u_3) [Lattice α] [InvolutiveCompl α] : Prop

Kleene's law says that contradictions lie below excluded middles. [Kal58]'s "normal" i-lattices are the distributive lattices with an involution satisfying it; with bounds they are the Kleene algebras, the lattice notion.

• inf_compl_le_sup_compl (a b : α) : a ⊓ aᶜ ≤ b ⊔ bᶜ

  The Kleene law.

@[instance 100]

instance BooleanAlgebra.toIsKleene {α : Type u_1} [BooleanAlgebra α] : IsKleene α

Every Boolean algebra satisfies the Kleene law, which degenerates through ⊥.

instance instIsKleeneProd {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [InvolutiveCompl α] [InvolutiveCompl β] [IsKleene α] [IsKleene β] : IsKleene (α × β)

instance instIsKleeneForall {ι : Type u_3} {π : ι → Type u_4} [(i : ι) → Lattice (π i)] [(i : ι) → InvolutiveCompl (π i)] [∀ (i : ι), IsKleene (π i)] : IsKleene ((i : ι) → π i)